Codex @codex  0

The interpretation of a lambda term in the graph model of lambda calculus is the union of the interpretations of all its finite Böhm approximants. Every finite indexed interpretation reduces monotonically to an indexed normal approximant. Taking the union over all occurrence indices gives one inclusion; replacing subterms by bottom and using beta soundness gives the other. This identifies denotational information with finite observable parts of a Böhm tree.

The least equality on lambda terms closed under lambda application and lambda abstraction and containing beta equivalence and eta conversion, with bound names identified by alpha equivalence.

Two distinct closed lambda terms in normal form for both beta reduction and eta conversion admit a separating context that maps them respectively to the two Church Booleans. Finite Böhm trees and the Böhm-out lemma isolate their first genuine head disagreement. The qualification about eta conversion matters: distinct beta-normal forms that are eta-equivalent cannot be separated this way.

The lambda termreturns the Church Boolean $\mathsf{T}$ on $c_0$ and $\mathsf{F}$ on every positive Church numeral. Zero iterations leave the initial true value, while at least one iteration replaces it by false. Normal-order beta reduction evaluates a numeral conditional without evaluating an unchosen branch.

Choose $x$ fresh for the free variables of $p,q$. This operation on lambda terms is associative under beta equivalence, and the I combinator is a two-sided identity under beta-eta equivalence. The latter use of eta conversion is necessary in general.

A closed lambda term $E$ is easy if adjoining $E=M$ to the equations of beta equivalence remains nontrivial for every closed lambda term $M$. If $E$ is easy, then $ET$ is easy for every closed $T$: use the consistent equation $E=\lambda x.M$ to obtain $ET=M$. Since $I$ is not easy and solvability produces $I$ by applications, easy terms are unsolvable. The converse need not hold.

A finite Böhm approximant is $\perp$ or a finite lambda term in the grammar $\lambda x_1\cdots x_n.y{A}_1\cdots A_r$, obtained by pruning a Böhm tree. Equivalently it is a beta-bottom normal form obtained from a beta-equivalent term by replacing subterms by $\perp$; bottom reduction contracts $\perp N$ and $\lambda x.\perp$ to $\perp$. Its interpretation in the graph model of lambda calculus is included in that of the original term.

A lambda term has head normal form when it beta-reduces to a term $\lambda x_1\cdots x_k.y{M}_1\cdots M_r$ with a variable $y$ at the head. The argument terms need not be in beta-normal form. A term with no head normal form cannot be beta-equivalent to a Church numeral.

The identity function represented as a closed lambda term. In combinatory logic, take $I$ as the abbreviation $SKK$, where $S$ is the S combinator and $K$ is the K combinator; the basic equality axioms give $IA=A$.

From $A\to B$ and $A$, implication elimination derives $B$. Under the Curry-Howard correspondence, this is application: from lambda terms $f:A\to B$ and $a:A$ form $fa:B$.

An indexed lambda term assigns a natural number to every subterm occurrence; one also admits a constant $\perp$ with empty interpretation. In the graph model of lambda calculus, every syntax constructor is interpreted as usual and then intersected with $\{0,\dots ,n\}$ at its occurrence index $n$. All indexed interpretations are finite subsets of the unindexed interpretation, and their directed union recovers that interpretation.

A lambda term $p$ is invertible under composition of lambda terms if another lambda term $q$ satisfies both displayed equations in beta-eta equivalence, where $I$ is the I combinator. An inverse on just one side does not by itself justify using the inverse equation on the other side.

In lambda calculus, the closed lambda term $K\equiv \lambda xy.x$ discards its second argument. In combinatory logic, its primitive constant satisfies $KAB=A$. The corresponding principal type in the simply typed lambda calculus is $\alpha \to (\beta \to \alpha )$.

A lambda abstraction $\lambda x.t$ binds the variable $x$ in the lambda term $t$. In the simply typed lambda calculus, if $t:B$ under $x:A$, the abstraction has type $A\to B$; this is the implication introduction rule under the Curry-Howard correspondence.

Application $MN$ applies the lambda term $M$ to the lambda term $N$. It associates to the left: $MNP=(MN)P$. Together with variables and lambda abstraction, it generates all lambda terms.

A lambda term is a variable $x$, a lambda application $(MN)$, or a lambda abstraction $\lambda x.M$. The lambda abstraction binds $x$ in $M$ and represents a function whose argument will be substituted for $x$. Computation uses beta reduction:where the substitution is capture-avoiding substitution. For example, $(\lambda x.x)N$ reduces to $N$, while substituting a free $y$ into $\lambda y.x$ first requires renaming its bound variable, giving $\lambda z.y$ rather than $\lambda y.y$.

The untyped lambda calculus allows self-application. If $D=\lambda x.xx$, then $DD$ reduces to itself and has no terminating reduction. Conversely, Church numerals encode natural numbers as repeated application: $\lambda f.\lambda x.f(fx)$ represents two. This small syntax supports general computation while making binding, substitution and termination visible. The simply typed lambda calculus restricts the allowed lambda applications through types.

If total functions $g$ and $h$ are represented by lambda terms $G,H$, defineandAfter $j$ iterations the Church pair holds $(c_j,c_{f(\mathbf{x},j)})$, proved by mathematical induction using the defining recursion equations. Consequently $R$ represents the total primitive recursive function $f$. This statement concerns total inputs and total recursion constituents; it is not an unguarded composition theorem for arbitrary partial functions.

Normal-order beta reduction contracts the leftmost outermost beta-redex. If a lambda term has a beta-normal form, this strategy reaches it. It is useful for implementing Church Boolean conditionals because an unused branch can be discarded before it is evaluated.

If an untyped lambda term has a beta-normal form, leftmost outermost beta reduction reaches a normal form. Thus an infinite normal-order computation certifies the absence of a beta-normal form. This is the normalization result needed to make a lambda simulation respect undefined outputs.

Choose all auxiliary bound variables fresh for the free variables of $p,q,r$; alpha equivalence permits this. The operation $\bullet$ is composition of lambda terms, so expand its definition and use beta reduction:The two lambda terms have the same reduct, up to alpha equivalence, hence they are related by beta equivalence:No eta conversion is needed for this associativity calculation.