notebook/notes/lambda-calculus/alpha-conversion.md

title	TARGET DECK	FILE TAGS	tags
α-conversion	Obsidian::STEM	λ-calculus	λ-calculus

Overview

Let \lambda-term P contain an occurrence of \lambda x. M, and let y \not\in FV(M). The act of replacing this occurrence of \lambda x. M with \lambda y. [y/x]M is called a change of bound variable or an \alpha-conversion in P.

If P can be changed to \lambda-term Q by a finite series of changes of bound variables, we shall say P is congruent to Q, or P \alpha-converts to Q, or P \equiv_\alpha Q.

%%ANKI Basic If P \equiv Q, does P \equiv_\alpha Q? Back: Yes. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Cloze P \equiv Q is to {equivalent} whereas P \equiv_\alpha Q is to {congruent}. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What two ways can we pronounce P \equiv_\alpha Q? Back: "P is congruent to Q" and "P \alpha-converts to Q". Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If P \equiv_\alpha Q, does P \equiv Q? Back: Not necessarily. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What does an \alpha-conversion refer to? Back: The act of replacing an occurrence of (\lambda x. M) with \lambda y. [y/x]M. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What distinguishes terms "\alpha-conversion" and "\alpha-converts"? Back: The latter refers to 0 or more applications of the former. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic \alpha-conversion is most related to what kind of \lambda-term? Back: Abstractions. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What property must y satisfy for \lambda x. M \equiv_\alpha \lambda y. [y/x]M? Back: y \not\in FV(M) Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Cloze "\alpha-{conversion}" refers to exactly one change of bound variable. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Cloze "\alpha-{converts}" refers to zero or more change of bound variables. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What kind of conversion is a change of bound variable? Back: An \alpha-conversion. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Given \lambda-terms P and Q, what does it mean for P to be congruent to Q? Back: P \equiv_\alpha Q Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Given \lambda-terms P and Q, P \equiv_\alpha Q if and only if what? Back: P can be changed to Q with a finite number of changes of bound variables. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Is the following identity true? \lambda x y. x(xy) \equiv \lambda x. (\lambda y. x(xy)) Back: Yes. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Is the following identity true? \lambda x y. x(xy) \equiv_\alpha \lambda x. (\lambda y. x(xy)) Back: Yes. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Is the following identity true? \lambda x y. x(xy) \equiv \lambda u v. u(uv)) Back: No. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Is the following identity true? \lambda x y. x(xy) \equiv_\alpha \lambda u v. u(uv)) Back: Yes. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Cloze \alpha-conversion is known as a change of {bound variable}. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What greek-prefixed term is a change of bound variable known as? Back: An \alpha-conversion. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If P \equiv_\alpha Q, what can be said about the free variables of P and Q? Back: FV(P) = FV(Q) Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What does it mean for \equiv_\alpha to be reflexive? Back: P \equiv_\alpha P Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What does it mean for \equiv_\alpha to be symmetric? Back: P \equiv_\alpha Q \Rightarrow Q \equiv_\alpha P Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What does it mean for \equiv_\alpha to be transitive? Back: P \equiv_\alpha Q \land Q \equiv_\alpha R \Rightarrow P \equiv_\alpha R Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What three properties make \equiv_\alpha an equivalence relation? Back: \equiv_\alpha is reflexive, symmetric, and transitive. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

Let x, y, and v be distinct variables. Then

• v \not\in FV(M) \Rightarrow [P/v][v/x]M \equiv_\alpha [P/x]M
• v \not\in FV(M) \Rightarrow [x/v][v/x]M \equiv_\alpha M
• y \not\in FV(P) \Rightarrow [P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M
• x \not\in FV(Q) \land y \not\in FV(P) \Rightarrow [P/x][Q/y]M \equiv_\alpha [Q/y][P/x]M
• [P/x][Q/x]M \equiv_\alpha [([P/x]Q)/x]M

%%ANKI Basic [N/x]M corresponds to which equivalence-transformation inference rule? Back: Substitution. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic [P/v][v/x]M \equiv [P/x]M corresponds to which equivalence-transformation inference rule? Back: Transitivity. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Rewrite (E_u^x)_v^x using \lambda-calculus syntax. Back: [v/x][u/x]E Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Rewrite [x/v][v/x]M using equivalence-transformation syntax. Back: (M^x_v)^v_x Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Cloze {v \not\in FV(M)} \Rightarrow [P/v][v/x]M \equiv_\alpha [P/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What happens if the antecedent is false in v \not\in FV(M) \Rightarrow [P/v][v/x]M \equiv_\alpha [P/x]M? Back: The LHS of the identity has more occurrences of P than the right. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If v \in FV(M) and x \not\in FV(M), does [P/v][v/x]M \equiv_\alpha [P/x]M? Back: No. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If v \not\in FV(M) and x \in FV(M), does [P/v][v/x]M \equiv_\alpha [P/x]M? Back: Yes. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If v \not\in FV(M), what simpler term is [P/v][v/x]M congruent to? Back: [P/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If v \not\in FV(M) and x \in FV(M), does [x/v][v/x]M \equiv_\alpha M? Back: Yes. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If v \not\in FV(M) and x \in FV(M), does [v/x][x/v]M \equiv_\alpha M? Back: No. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If v \in FV(M) and x \not\in FV(M), does [v/x][x/v]M \equiv_\alpha M? Back: Yes. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If v \in FV(M) and x \not\in FV(M), does [x/v][v/x]M \equiv_\alpha M? Back: No. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic If y \not\in FV(P), "commuting" substitution in [P/x][Q/y]M yields what congruent term? Back: [([P/x]Q)/y][P/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Cloze {y \not\in FV(P)} \Rightarrow [P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Cloze {x \not\in FV(Q) \land y \not\in FV(P)} \Rightarrow [P/x][Q/y]M \equiv_\alpha [Q/y][P/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic [P/x][Q/y]M \equiv_\alpha [Q/y][P/x]M is a specialization of what more general congruence? Back: [P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Cloze {T} \Rightarrow [P/x][Q/x]M \equiv_\alpha [([P/x]Q)/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What expression containing nested substitutions is congruent to [P/x][Q/x]M? Back: [([P/x]Q)/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What expression containing adjacent substitutions is congruent to [([P/x]Q)/x]M? Back: [P/x][Q/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What happens if the antecedent of the following lemma is false? $y \not\in FV(P) \Rightarrow [P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M$ Back: y is subbed in M on the LHS but subbed in both P and M on the RHS. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Free occurrences of x are substituted in which \lambda-terms of [P/x][Q/y]M? Back: Q and M. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Free occurrences of y are substituted in which \lambda-terms of [P/x][Q/y]M? Back: M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Free occurrences of x are substituted in which \lambda-terms of [([P/x]Q)/y][P/x]M? Back: Q and M. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Free occurrences of y are substituted in which \lambda-terms of [([P/x]Q)/y][P/x]M? Back: P and M. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

For \lambda-terms M, M', N, and N', and variable x, $M \equiv_\alpha M' \land N \equiv_\alpha N' \Rightarrow [N/x]M \equiv_\alpha [N'/x]M'$

%%ANKI Basic The proof of which implication shows "substitution is well-behaved w.r.t. \alpha-conversion"? Back: P \equiv_\alpha P' \land M \equiv_\alpha M' \Rightarrow [P/x]M \equiv_\alpha [P'/x]M' Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What does Hindley et al. mean by "substitution is well-behaved w.r.t. \alpha-conversion"? Back: \alpha-converting substitution inputs yields congruent outputs. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Cloze {M \equiv_\alpha M' \land N \equiv_\alpha N'} \Rightarrow [N/x]M \equiv_\alpha [N'/x]M' Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic What does Hindley et al. say the following implication says about substitution? $M \equiv_\alpha M' \land N \equiv_\alpha N' \Rightarrow [N/x]M \equiv_\alpha [N'/x]M'$ Back: It is well-defined with respect to \alpha-conversion. Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

Simultaneous Substitution

Substitution can be generalized in the natural way to define simultaneous substitution [N_1/x_1, N_2/x_2, \ldots, N_n/x_n]M$ for $n \geq 2. As in equiv-trans#Substitution, simultaneous substitution is different from sequential substitution.

%%ANKI Basic How is simultaneous substitution of N_1 for x_1 and N_2 for x_2 in M denoted? Back: [N_1/x_1, N_2/x]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic How is [N_1/x_1, N_2/x_2]M denoted in the equivalence-transformation system? Back: M_{N_1, N_2}^{x_1, x_2} Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic How is M_{N_1, N_2}^{x_1, x_2} denoted in \lambda-calculus? Back: [N_1/x_1, N_2/x_2]M Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Suppose M \equiv x_1x_2. What is the result of [u/x_1]([x_1/x_2]M)? Back: uu Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

%%ANKI Basic Suppose M \equiv x_1x_2. What is the result of [u/x_1, x_1/x_2]M? Back: ux_1 Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.

END%%

Bibliography

• Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf.