0
$\begingroup$

I want to prove that if $$(\lambda x. P)Q=(\lambda y. M)N$$ then $$P[x:=Q]= M[y:=N]$$ which means that the contraction of a given redex yields a unique result (so we don't have beta equivalence, but alpha equivalence).

I would go for a proof by contradiction but I think it should be prooved by a variation of structural induction, as it seems quite a hasty conclusion that an occurence of x (or y) hasn't been substituted and that's why contractum's differ.

Though I have neither seen any variation of induction used somewhere, nor I can use it without proof.

So could anyone help?

I am studying from "Lectures on the Curry"-Howard isomorphism-Sorensen, Urzyczyn (2006)

$\endgroup$
2
  • 2
    $\begingroup$ I'm not sure to understand your question. If $(\lambda x.P)Q = (\lambda y. M)N$ ($=$ is always in the sense of $\alpha$-equivalence here), then $\lambda x.P = \lambda y.M$ and $Q = N$, from that it follows that $P[x:=Q] = M[y:=N]$ because substitution is compatible with $\alpha$-equivalence.. $\endgroup$ May 9, 2023 at 9:32
  • $\begingroup$ Ohh... it was that simple? $\endgroup$ May 9, 2023 at 11:40

1 Answer 1

0
$\begingroup$

Transferring here the answer in the comments so that the question won't be left in the unanswered posts forever.

I'm not sure to understand your question. If $(𝜆𝑥.𝑃)𝑄=(𝜆𝑦.𝑀)𝑁$ (= is always in the sense of $𝛼$-equivalence here), then $𝜆𝑥.𝑃=𝜆𝑦.𝑀$ and $𝑄=𝑁$, from that it follows that $𝑃[𝑥:=𝑄]=𝑀[𝑦:=𝑁]$ because substitution is compatible with $𝛼$-equivalence..

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .