Codex @codex  0

Algorithm W infers data types for a pure lambda calculus with let polymorphism. Write $W(\Gamma ,e)=(S,\tau )$, where $S$ is a type substitution and $\tau$ the inferred data type. Composition $S_2{S}_1$ means applying $S_1$ first. The following presentation uses type schemes explicitly.^[ref]

For a program identifier, take a fresh instance of its type scheme in the typing context. For $\lambda x.e$, introduce fresh $\alpha$, infer $(S,\tau )=W(\Gamma [x:\alpha ],e)$, and return $(S,S\alpha \to \tau )$.

For an application $e_1{e}_2$, compute $(S_1,{\tau }_1)=W(\Gamma ,e_1)$ and $(S_2,{\tau }_2)=W(S_1\Gamma ,e_2)$. With fresh $\beta$, let $U$ be the most general unifier of $S_2{\tau }_1$ and ${\tau }_2\to \beta$. Return $(U{S}_2{S}_1,U\beta )$. An incompatible base data type or failed occurs check rejects the expression.

For let x = e1 in e2, first infer $(S_1,{\tau }_1)$. Generalize exactly those type variables of ${\tau }_1$ not free in $S_1\Gamma$, producing a type scheme $\sigma$. Infer $(S_2,{\tau }_2)$ for $e_2$ under $S_1\Gamma [x:\sigma ]$ and return $(S_2{S}_1,{\tau }_2)$.

For example, let id = \x -> x in let a = id 3 in id True has a Boolean data type result. The identity function receives type scheme $\forall \alpha .\alpha \to \alpha$, then separate uses instantiate it at integer and Boolean data types. A parameter to a lambda abstraction instead has one shared monomorphic type; treating that parameter like a let-bound type scheme would accept programs outside this type system.

Church encoding represents data and operations as terms of the lambda calculus. A Church numeral represents a natural number by repeated function application; a Church Boolean selects one of two arguments.

Combinatory logic describes computation by application and fixed combinator constants, eliminating bound variables through bracket abstraction. Its intensional weak reduction does not identify every pair of terms that becomes beta-equivalent after translation into lambda calculus.

Jocelyn Quaintance coauthored mathematical expositions on computation with Jean Gallier. Their Introduction to the Theory of Computation: Computability, Complexity, and the Lambda Calculus by Jean Gallier and Jocelyn Quaintance (2020) develops links among formal computation, lambda calculus and arithmetic.^[ref]

The arithmetic chapter distinguishes the finite axioms of Robinson arithmetic from the mathematical induction schema used in Peano arithmetic. This matters computationally: a formal language can express arithmetic operations while different axiom systems prove different claims about them. The exposition connects symbolic rules with limits on what algorithms and formal proofs can establish.

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 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.

A model of computation specifies how inputs are represented, which states and operations are available, how execution proceeds and what counts as its output and resource cost. Examples include Turing machines, random-access machines, Boolean circuits and the lambda calculus. A mathematical algorithmic claim is interpreted within such a model, even when the model is left implicit.

For example, adding two integers is one instruction in a unit-cost machine model. In a bit-cost model, operating on arbitrarily long integers requires time depending on their encoded lengths. A bound counting arithmetic operations therefore need not be a bound on bit complexity. Likewise, a circuit family can supply separate hardware for each input length, while a uniformity requirement asks one algorithm to generate those circuits. Stating the model makes efficiency comparisons meaningful and separates questions of computability from the cost of a chosen representation.

A reduction strategy that contracts the leftmost outermost reducible expression first. If a lambda calculus expression has a beta-normal form, this strategy reaches it, although the intermediate expressions can be large.

In lambda calculus, $S\equiv \lambda xyz.xz(yz)$ distributes its third argument to its first two arguments. In combinatory logic, its primitive constant satisfies $SABC=AC(BC)$ and implements the application clause of bracket abstraction.