notebook/notes/lambda-calculus/index.md

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

Overview

Assume that there is given an infinite sequence of expressions called variables and a finite or infinite sequence of expressions called atomic constants, different from the variables. The set of expressions called \lambda-terms is defined inductively as follows:

• all variables and atomic constants are \lambda-terms (called atoms);
• if M and N are \lambda-terms, then (MN) is a \lambda-term (called application);
• if M is a \lambda-term and x is a variable, then (\lambda x. M) is a \lambda-term (called abstraction).

If the sequence of atomic constants is empty, the system is called pure. Otherwise it is called applied.

%%ANKI Basic Who is usually attributed the creation of \lambda-calculus? Back: Alonzo Church. 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 a "higher-order function" refer to? Back: A function that acts on other functions. 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 f(x) = x - y written using \lambda-calculus? Back: \lambda x. x - y 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 f(x, y) = x - y written using (uncurried) \lambda-calculus? Back: \lambda x y. x - y 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 do you curry expression \lambda x y. x - y? Back: \lambda x. \lambda y. x - y 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 do you uncurry expression \lambda x. \lambda y. x - y? Back: \lambda x y. x - y 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 (\lambda x. x - y)(0) evaluate to? Back: 0 - y 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 many variables exist in a \lambda-calculus formal system? Back: An infinite number. 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 many atomic constants exist in a \lambda-calculus formal system? Back: Zero or more. 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 variables and atomic constants? Back: The latter is meant to refer to constants outside the formal system. 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 classes of expressions does an "atom" potentially refer to? Back: Variables and atomic constants. 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 general term describes both variables and atomic constants? Back: Atoms. 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 Why are variables and atomic constants called "atoms"? Back: They are not composed of smaller \lambda-terms. 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 When is a \lambda-calculus considered pure? Back: When there exist no atomic constants in the system. 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 When is a \lambda-calculus considered applied? Back: When there exists at least one atomic constant in the system. 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 A \lambda-calculus is either {pure} or {applied}. 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 term refers to the base case of the \lambda-term definition? Back: The atoms. 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 terms refer to the inductive cases of the \lambda-term definition? Back: Application and abstraction. 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 Given \lambda-terms M and N, {(MN)} is referred to as {application}. 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 Given \lambda-term M and variable x, {(\lambda x. M)} is referred to as {abstraction}. 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 Consider term (\lambda x. x)(0). Is our \lambda-calculus pure or applied? Back: Applied. 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 Consider term (\lambda x. x)(y). Is our \lambda-calculus pure or applied? Back: Indeterminate. 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 terms categorize all \lambda-terms? Back: Atoms, applications, and 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 How is a constant function returning y denoted in \lambda-calculus? Back: \lambda x. y 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 By convention, parentheses in \lambda-calculus are {left}-associative. 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 expression \lambda x. \lambda y. MN written with parentheses reintroduced? Back: (\lambda x. (\lambda y. (MN))) 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 are parentheses conventionally reintroduced to \lambda-term MN? Back: (MN) 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 are parentheses conventionally reintroduced to \lambda-term MNPQ? Back: (((MN)P)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 How are parentheses conventionally reintroduced to \lambda-term \lambda x. PQ? Back: (\lambda x. (PQ)) 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 (MN) is interpreted as applying {1:M} to {1:N}. 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%%

Syntactic Identity

Syntactic identity of terms is denoted by "\equiv".

%%ANKI Basic What does it mean for two terms to be syntactically identical? Back: The terms are written out using the exact same sequence of characters. 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 form of Lean equality corresponds to \lambda-calculus's \equiv operator? Back: Syntactic equality. 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. Tags: lean

END%%

%%ANKI Basic How does Hindley et al. denote syntactic identity of \lambda-terms M and N? Back: M \equiv N 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 syntactic identities are assumed when MN \equiv PQ? Back: M \equiv P and N \equiv 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 syntactic identities are assumed when \lambda x. M \equiv \lambda y. P? Back: x \equiv y and M \equiv 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%%

Length

The length of a \lambda-term (denoted lgh) is equal to the number of atoms in the term:

• lgh(a) = 1 for all atoms a;
• lgh(MN) = lgh(M) + lgh(N);
• lgh(\lambda x. M) = 1 + lgh(M).

%%ANKI Basic What is the base case of the recursive definition of the "length of a \lambda-term"? Back: lgh(a) = 1 for all atoms a. 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 the length of a \lambda-term measure? Back: The number of atoms in the term. 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 For atom a, what does lgh(a) equal? Back: 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%%

%%ANKI Basic What is the recursive definition of the "length of application"? Back: For \lambda-terms M and N, lgh(MN) = lgh(M) + lgh(N). 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 For \lambda-terms M and N, what does lgh(MN) equal? Back: lgh(M) + lgh(N) 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 is the recursive definition of the "length of abstraction"? Back: For \lambda-term M, lgh(\lambda x. M) = 1 + lgh(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 For \lambda-term M, what does lgh(\lambda x. M) equal? Back: 1 + lgh(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 lgh(x(\lambda y. yux)) equal? Back: 5 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 The phrase "{induction on M}" is shorthand for phrase "{induction on lgh(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%%

Occurrence

For \lambda-terms P and Q, the relation P occurs in Q is defined by induction on Q as:

• P occurs in P;
• if P occurs in M or in N, then P occurs in (MN);
• if P occurs in M or P is x, then P occurs in (\lambda x. M).

%%ANKI Basic What is the base case of recursive definition "P occurs in Q"? Back: P occurs in 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 intuition does the "occurs in" relation aim to capture? Back: Whether a \lambda-term appears somewhere in another \lambda-term. 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 If P occurs in {1:M} or {1:N}, then P occurs in (MN). 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 If P occurs in {1:M} or P {1:is x}, then P occurs in (\lambda 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 "occurs in" recursively defined for application? Back: P occurs in (MN) if P occurs in M or P occurs in N. 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 "occurs in" recursively defined for abstraction? Back: P occurs in (\lambda x. M) if P occurs in M or P is 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 Basic How many occurences of x are in ((xy)(\lambda x. (xy)))? Back: 3 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 preprocessing step does Hindley et al. recommend when counting occurrences of \lambda-terms? Back: Reintroduce parentheses. 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 a particular occurrence of \lambda x. M in a term P, the occurrence of M is called the scope of the occurrence of \lambda x.

%%ANKI Cloze Given term \lambda x. M, the occurrence of {1:M} is called the {2:scope} of the occurrence of {1:\lambda 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 Basic The concept of scope is relevant 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 is the scope of the leftmost \lambda y in the following term? (\lambda y. yx(\lambda x. y(\lambda y.z)x))vw$$ Back: yx(\lambda x. y(\lambda y. z)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 Basic What is the scope of \lambda x in the following term? (\lambda y. yx(\lambda x. y(\lambda y.z)x))vw$$ Back: y(\lambda y. z)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 Basic What is the scope of the rightmost \lambda y in the following term? (\lambda y. yx(\lambda x. y(\lambda y.z)x))vw$$ Back: z 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 is wrong with asking "what is the scope of x in \lambda-term P"? Back: We should be asking about a \lambda 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%%

Free and Bound Variables

An occurrence of a variable x in a term P is called

• bound if it is in the scope of a \lambda x in P;
• bound and binding iff it is the x in \lambda x;
• free otherwise.

FV(P) denotes the set of all free variables of P. A closed term is a term without any free variables.

%%ANKI Basic What kind of \lambda-terms can be classified as bound and/or free? Back: 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 When is variable x in term P said to be "bound"? Back: When it is in the scope of a \lambda x in 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 When is variable x in term P said to be "bound and binding"? Back: If and only if it is the x in some occurrence of \lambda 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 Basic When is variable x in term P said to be "free"? Back: When it is not bound. 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 When is variable x in term P said to be "free and binding"? Back: N/A. 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 When is variable x in term P said to be "bound" and "free"? Back: When one occurrence is bound and another occurrence is free. 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 When is variable x called a "bound variable of P"? Back: When x has at least one binding occurrence in 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 When is variable x called a "free variable of P"? Back: When x has at least one free occurrence in 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 Cloze {FV(P)} denotes the {set of all free variables} of 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 When is a \lambda-term considered "closed"? Back: When the term has no free 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 term describes \lambda-term P satisfying FV(P) = \varnothing? Back: Closed. 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 Using FV, when is \lambda-term P closed? Back: When FV(P) = \varnothing. 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 \lambda x. y a closed term? Why or why not? Back: No. y is a free 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 Is \lambda x. x a closed term? Why or why not? Back: Yes. The term has no free 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 Which specific occurrences are bound in \lambda x. x(\lambda y. yz)? Back: Both $x$s and both $y$s. 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 Which specific occurrences are free in \lambda x. x(\lambda y. yz)? Back: The only z. 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 Which specific occurrences are bound and binding in \lambda x. x(\lambda y. yz)? Back: The first x and the first y. 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 expression FV(\lambda x. xyz) evaluate to? Back: \{y, z\} 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-term P, what kind of mathematic object is FV(P)? Back: A set. 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%%

Substitution

For any M, N, and x, define [N/x]M to be the result of substituting N for every free occurrence of x in M, and changing bound variables to avoid clashes.

%%ANKI Basic How is E_e^x equivalently written in \lambda-calculus? Back: [e/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 How is [N/x]M equivalently written in equivalence transformation? Back: M_N^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 Basic How does substitution, say [N/x]M, affect free variables? Back: Every free occurrence of x is substituted with N. 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 does substitution, say [N/x]M, affect bound variables? Back: Bound variables are renamed to avoid name clashes. 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 [N/x]M is the result of substituting {1:N} for every free occurrence of {1:x} in {1: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 {M^x_e} is to equivalence transformation whereas {[e/x]M} is to \lambda-calculus. 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 is the result of [N/x]x? Back: N 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 is the result of [N/x]a, for some atom a \not\equiv x? Back: a 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 is the result of [N/x]a, for some atom a \equiv x? Back: N 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 is the result of [N/x](PQ)? Back: ([N/x]P)([N/x]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 is the result of [N/x](\lambda x. P)? Back: \lambda x. 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 If x \in FV(P) and y \in FV(N), what is the result of [N/x](\lambda y. P)? Back: \lambda z. [N/x][z/y]P where z \not\in FV(NP). 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 x \not\in FV(P) and y \in FV(N), what is the result of [N/x](\lambda y. P)? Back: \lambda y. 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 If x \in FV(P) and y \not\in FV(N), what is the result of [N/x](\lambda y. P)? Back: \lambda y. [N/x]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 If x \not\in FV(P) and y \not\in FV(N), what is the result of [N/x](\lambda y. P)? Back: \lambda y. 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 Is (\lambda x. xy)N \equiv Ny? 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 [N/x]xy \equiv Ny? 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%%

For all \lambda-terms M, N, and variables x:

• [x/x]M \equiv M
• x \not\in FV(M) \Rightarrow [N/x]M \equiv M
• x \in FV(M) \Rightarrow FV([N/x]M) = FV(N) \cup (FV(M) - \{x\})
• lgh([y/x]M) = lgh(M)

%%ANKI Basic What is the result of [x/x]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 If x \not\in FV(M), what is the result of [N/x]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 Suppose x \in FV(M). How is FV([N/x]M) equivalently written without substitution? Back: FV(N) \cup (FV(M) - \{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 Basic Suppose x \in FV(M). How is FV(N) \cup (FV(M) - \{x\}) more simply written using substitution? Back: FV([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 is the result of lgh([y/x]M)? Back: lgh(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%%

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.