2
$\begingroup$

I'm doing some simple exercise about Lambda Calculus but i have doubt about this beta-reduction.

Let $$<u,v>= \lambda p((p)u)v$$ a pair in Lambda Calculus.

Prove that for every lambda term M you have that: $$ (<M,u>) <M,v> \simeq_{\beta} (((M)M)v)u$$

$\endgroup$
4
  • $\begingroup$ There's nothing wrong here. The only glaring issue I see is that your first step is not a $\beta$-reduction, even though you've marked it as such. $\endgroup$ Commented Jan 26, 2020 at 14:02
  • $\begingroup$ Oh thank you , I will correct now! So I will also change the question in an answer $\endgroup$ Commented Jan 26, 2020 at 14:17
  • $\begingroup$ Note that on the first step you are implicitly using an $\alpha$-reduction as well as substituting values in, if you'd want to mark that. $\endgroup$ Commented Jan 26, 2020 at 14:19
  • $\begingroup$ Ok thank you again, I pretty new in the lambda calculus world... $\endgroup$ Commented Jan 26, 2020 at 14:31

1 Answer 1

Reset to default
2
$\begingroup$

To prove that you can follow this steps: $$(<M,u>) <M,v> \simeq_{\alpha} (\lambda p((p)M)u) \space \lambda q((q)M)v \\ \simeq_{\beta} ((\lambda q((q)M)v)M)u\\ \simeq_{\beta} ((M)M)v)u$$

Q.E.D.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.