Fact-checked by Grok 2 weeks ago

Church encoding

Church encoding is a method developed by Alonzo Church for representing various data types and structures, such as natural numbers, booleans, and pairs, purely as lambda terms within the untyped lambda calculus, enabling computation without relying on any built-in primitives beyond function abstraction and application.^[1] Introduced at the end of Church's 1933 paper "A Set of Postulates for the Foundation of Logic (Second Paper)," this encoding demonstrates the expressive power of lambda calculus by allowing arithmetic, logic, and data manipulation to be defined via beta-reduction alone.^[2]^[1] The most prominent example of Church encoding is the representation of natural numbers, known as Church numerals, where the number n is encoded as the lambda term \lambda f x. f^n x, a function that applies its first argument f exactly n times to its second argument x.^[3] For instance:

Zero: $0 \triangleq \lambda f x. x
One: $1 \triangleq \lambda f x. f x
Two: $2 \triangleq \lambda f x. f (f x)

This encoding supports basic arithmetic operations through additional lambda terms; the successor function, for example, is \mathsf{succ} \triangleq \lambda n f x. f (n f x), which increments a numeral by one application.^[3] Similarly, addition is defined as \mathsf{plus} \triangleq \lambda m n f x. m f (n f x), composing the applications of two numerals.^[1] Beyond numerals, Church encoding extends to booleans, where \mathsf{true} \triangleq \lambda x y. x and \mathsf{false} \triangleq \lambda x y. y, functioning as selectors that return one of two arguments based on a condition.^[3] Logical operations follow naturally: negation is \mathsf{not} \triangleq \lambda b. b\ \mathsf{false}\ \mathsf{true}, and conjunction is \mathsf{and} \triangleq \lambda b_1 b_2. b_1\ b_2\ \mathsf{false}.^[3] Pairs are encoded as \mathsf{pair} \triangleq \lambda a b f. f a b, with projections using booleans: \mathsf{fst} \triangleq \lambda p. p\ \mathsf{true} and \mathsf{snd} \triangleq \lambda p. p\ \mathsf{false}.^[3] Church encoding underscores the universality of lambda calculus, as formalized in Church's lambda calculus system, which Church presented more fully in his 1941 book The Calculi of Lambda-Conversion and used to establish foundational results in computability, including the equivalence of lambda-definable functions to recursive functions.^[4] While powerful for theoretical foundations, such encodings highlight the untyped nature of the original lambda calculus, where ill-formed applications can lead to non-termination or unexpected reductions, influencing later developments in typed variants.^[3]

Introduction

Definition and Motivation

Church encoding is a technique in untyped lambda calculus for representing data structures and operations solely through lambda terms, without relying on any primitive types or built-in operations beyond function abstraction and application.^[1] In this system, all data—such as booleans, pairs, and natural numbers—and all functions manipulating them are expressed as lambda abstractions, demonstrating the foundational principle that computation can be reduced to the application of anonymous functions. The core syntax of lambda terms includes abstractions of the form \lambda x.M, where x is a variable and M is a lambda term denoting the body of the function, and applications of the form (M N), where M and N are lambda terms representing a function applied to an argument.^[1] Computation proceeds via beta-reduction, the rule that substitutes the argument N for all free occurrences of x in M when reducing (\lambda x.M) N, subject to variable capture avoidance. The primary motivation for Church encoding stems from Alonzo Church's development of lambda calculus in the early 1930s as a formal system for the foundations of logic and mathematics, where encodings were introduced to illustrate the calculus's ability to model recursive functions and data without external primitives.^[1] By encoding structures like natural numbers (known as Church numerals), booleans, and pairs purely in lambda terms, Church aimed to prove that lambda calculus could express all effectively computable functions, thereby establishing its equivalence to other models of computation and supporting the Church-Turing thesis on the limits of mechanical calculation.^[5] This approach highlights the Turing-completeness of lambda calculus, as the encodings enable the definition of arithmetic, logic, and control structures through higher-order functions alone.^[1] A simple illustrative example is the encoding of the identity function as \lambda x.x, which takes any lambda term N and returns it unchanged upon application ((\lambda x.x) N), reducing via beta-reduction to N. Church encodings were originally developed in Church's 1933 paper and elaborated in his 1941 monograph to rigorously demonstrate the expressive power of lambda calculus in relation to recursive function theory and other foundational systems.^[2]

Historical Context

Alonzo Church introduced lambda calculus in the early 1930s as part of his efforts to address foundational issues in logic and mathematics, particularly in relation to the Entscheidungsproblem posed by David Hilbert, which sought an algorithm to determine the truth of mathematical statements in first-order logic.^[1] His initial formulation appeared in the 1932 paper "A Set of Postulates for the Foundation of Logic," where lambda calculus served as a system for functional abstraction and application, initially within a typed framework to avoid paradoxes. This work laid the groundwork for using lambda terms to model computation, evolving from Church's broader investigations into the limits of formal systems during the 1930s. Although the 1933 encoding was presented in Church's simple theory of types, it laid the groundwork for representations in the untyped lambda calculus formalized in 1936.^[6] Church first introduced the encoding of natural numbers in his 1933 paper "A Set of Postulates for the Foundation of Logic (Second Paper)". In his 1936 paper "An Unsolvable Problem of Elementary Number Theory," he formalized lambda-definability using the untyped lambda calculus and this encoding to demonstrate the undecidability of certain problems in number theory.^[7] In this context, Church shifted to an untyped lambda calculus, eliminating restrictive typing from earlier versions to enhance expressive power for defining effective calculability.^[1] The encoding allowed him to prove that lambda-definable functions capture intuitive notions of computability, forming the basis of Church's thesis, which posits lambda calculus as a universal model of computation, independently paralleling Alan Turing's 1936 machine model.^[5] The adoption of Church encoding played a key role in establishing the Turing completeness of lambda calculus, as subsequent proofs showed equivalence between lambda-definable functions and Turing-computable ones.^[5] It influenced early developments in recursion theory, notably Stephen Kleene's 1938 recursion theorem, which extended Church's ideas on self-referential computable functions using similar lambda-based notations.^[8] Although Church encoding predates Turing machines by several months in its formalization, its core concepts saw no significant revisions after the 1940s, yet it retains foundational relevance in theoretical computer science for illustrating pure functional computation.^[9]

Fundamental Encodings

Church Booleans

In Church encoding within the lambda calculus, boolean values are represented as higher-order functions that select one of two arguments based on a truth value, treating booleans uniformly as functional selectors rather than primitive constants. The encoding for true selects the first argument and is defined as the lambda term \true \triangleq \lambda t. \lambda f. t.^[3] Conversely, false selects the second argument and is encoded as \false \triangleq \lambda t. \lambda f. f.^[3] This selector-based representation, originally proposed by Alonzo Church, enables the implementation of control flow and logical structures purely through lambda abstraction and application, without relying on built-in data types.^[3] Building on these encodings, the conditional operation (if-then-else) is defined as \if \triangleq \lambda p. \lambda a. \lambda b. p \, a \, b, where the boolean p determines whether to return a (the "then" branch) or b (the "else" branch) via selection.^[3] Standard logical operations follow similarly: negation (not) inverts the boolean by swapping the branches, given by \not \triangleq \lambda p. p \, \false \, \true; conjunction (and) evaluates the second operand only if the first is true, as \and \triangleq \lambda p. \lambda q. p \, q \, \false; and disjunction (or) short-circuits to true if the first operand is true, defined as \or \triangleq \lambda p. \lambda q. p \, \true \, q.^[3] These compositions exploit the inherent selector mechanism of Church booleans to replicate classical boolean algebra in lambda terms. For example, applying and to true and false yields false through beta-reduction: \and \, \true \, \false \beta-reduces to \true \, \false \, \false, which further reduces to \false since true selects its first argument.^[10] This reduction sequence highlights how Church booleans facilitate precise, step-by-step evaluation of logical expressions solely via functional application. These foundational encodings underpin extensions to predicates, which test properties using boolean outcomes.^[3]

Church Pairs

In the lambda calculus, ordered pairs are encoded using higher-order functions that allow selective access to their components without relying on primitive data types. The pair constructor, denoted as PAIR, is defined as \lambda x. \lambda y. \lambda z. z\, x\, y, which takes two elements x and y along with a selector function z and applies z to x and y.^[11] This encoding represents the pair as a function that defers the choice of operation on its components until a projector is provided.^[12] To extract the components, two projection functions are used. The first projection, FST, is \lambda p. p\, (\lambda x. \lambda y. x), which applies the pair p to a function that selects the first argument, yielding x. Similarly, the second projection, SND, is \lambda p. p\, (\lambda x. \lambda y. y), which selects the second argument y. These projections ensure that pairs behave as composable units, enabling the encoding to support functional manipulation of structured data.^[11]^[12] For instance, to encode the pair of Church numerals 3 and 4, first form the pair as PAIR applied to the numeral for 3 (\lambda f. \lambda x. f\, (f\, (f\, x))) and the numeral for 4 (\lambda f. \lambda x. f\, (f\, (f\, (f\, x)))). Applying FST to this pair reduces to the numeral for 3, while SND yields the numeral for 4, demonstrating how the encoding preserves the distinct identities of the components through beta reduction.^[12] This pair encoding can be extended to represent longer tuples by nesting pairs, such as encoding a triple as a pair of one element and another pair. Such constructions form the basis for recursive data definitions in lambda calculus, serving as a foundational building block for more complex structures like lists and trees.^[13] Pairs also play a role in implementing operations like the predecessor function by storing intermediate values during computation.^[11]

Predicates

In Church encoding, predicates are higher-order functions that take encoded data, such as numerals, and return Church booleans to test specific properties, enabling conditional behavior in pure lambda calculus without built-in primitives.^[14] The IsZero predicate determines whether a Church numeral represents zero. It is defined as \lambda n. n\, (\lambda x. \mathsf{False})\, \mathsf{True}, where applying the numeral n to the constant function (\lambda x. \mathsf{False}) n times yields \mathsf{False} if n > 0, but returns \mathsf{True} directly if n = 0. This leverages the iterative nature of Church numerals to fold the test over the encoded count.^[14]^[15] Predicates for parity, such as IsOdd and IsEven, rely on a modulo operation adapted to Church numerals, which itself requires recursion via a fixed-point combinator. For instance, IsOdd can be expressed as \lambda n. \mathsf{IsZero}\, (\mathsf{Mod}\, n\, 2), where Mod computes the remainder through repeated subtraction until the divisor is reached. IsEven follows symmetrically as the negation of IsOdd. These definitions highlight the recursive structure needed for non-iterative tests in lambda calculus.^[15] Equality testing for Church numerals compares two values m and n by checking if their difference is zero in both directions: \lambda m. \lambda n. \mathsf{AND}\, (\mathsf{IsZero}\, (\mathsf{Sub}\, m\, n))\, (\mathsf{IsZero}\, (\mathsf{Sub}\, n\, m)). This bidirectional subtraction ensures symmetry, returning \mathsf{True} only if m = n.^[16] These predicates uniquely facilitate branching in lambda calculus computations, as Church booleans themselves act as selectors in conditionals, such as \mathsf{IF}\, (\mathsf{IsZero}\, n)\, \mathsf{then}\, \mathsf{else}. For example, to compute the factorial of a numeral n, one might use IsZero to base-case return 1 when n = 0, recursing otherwise on the predecessor.^[14]^[16]

Numerical Encodings

Church Numerals

Church numerals provide a way to encode the natural numbers within the untyped lambda calculus, representing each nonnegative integer n through a higher-order function that performs iteration. Specifically, the Church numeral \overline{n} is defined as the lambda term \lambda f. \lambda x. f^n x, where f^n x denotes the application of the function f exactly n times to the argument x. This encoding was introduced by Alonzo Church at the end of his 1933 paper "A Set of Postulates for the Foundation of Logic (Part II)," where it serves as a basis for representing arithmetic in pure lambda terms.^[1] To illustrate, the numeral for zero, \overline{0}, is \lambda f. \lambda x. x, which applies f zero times and thus returns x unchanged. For one, \overline{1} = \lambda f. \lambda x. f x, applying f once. The numeral for two is \overline{2} = \lambda f. \lambda x. f (f x), and for three, \overline{3} = \lambda f. \lambda x. f (f (f x)). These examples demonstrate how the structure grows by nesting applications of f, directly embedding the count n into the term's form without relying on external data types. Conceptually, a Church numeral \overline{n} acts as an iterator: given any function f (interpreted as a successor or step operation) and a base value x, it computes the result of iterating f over x precisely n times, thereby capturing the iterative essence of natural numbers. This interpretation aligns with the intuitive notion of numbers as repeated applications, allowing lambda calculus to model counting and succession purely functionally. The encoding implicitly realizes the successor operation from Peano arithmetic, where each numeral builds upon the previous by adding one more application of f, providing a foundation for numerical reasoning in lambda terms. Furthermore, Church numerals relate to fixed-point combinators in enabling recursive definitions over numbers, as iteration can be extended to recursion via such combinators for more complex computations.^[17]

Arithmetic Operations

Arithmetic operations on Church numerals are defined purely through higher-order functions in the lambda calculus, leveraging the iterative nature of the numerals to compose applications of a function f without requiring explicit loops or primitive recursion. This approach demonstrates the expressive power of lambda terms, where numbers themselves act as iterators.^[3] Addition of two Church numerals m and n, denoted as \mathsf{plus} = \lambda m.\lambda n.\lambda f.\lambda x. m f (n f x), works by applying f a total of m + n times to x: first n times via the inner application, then m more times to that result.^[18] Specifically, n f x computes the n-fold application, and m f then iterates f m times over that intermediate value, yielding the sum.^[19] Multiplication, defined as \mathsf{mult} = \lambda m.\lambda n.\lambda f.\lambda x. m (n f) x, treats the n-fold application of f as a single composite function n f, which is then applied m times to x, effectively composing m \times n applications of f. This encodes the distributive property of multiplication over iterated function application.^[3] Exponentiation follows similarly with \mathsf{exp} = \lambda m.\lambda n. n m, where n acts as an iterator that applies the function m (itself a numeral encoding repeated application) exactly n times to an implicit base, resulting in m^n iterations.^[19] Here, the base numeral m is elevated to serve as the function being iterated, showcasing the higher-order manipulation central to Church encoding. To illustrate, consider the beta-reduction of \mathsf{plus}\ \ulcorner 2 \urcorner\ \ulcorner 3 \urcorner\ f\ x, where \ulcorner 2 \urcorner = \lambda f.\lambda x. f (f x) and \ulcorner 3 \urcorner = \lambda f.\lambda x. f (f (f x)). Substituting yields \ulcorner 2 \urcorner\ f\ (\ulcorner 3 \urcorner\ f\ x) = f (f (\ulcorner 3 \urcorner\ f\ x)), and \ulcorner 3 \urcorner\ f\ x = f (f (f x)), so f (f (f (f (f x)))), which is precisely \ulcorner 5 \urcorner\ f\ x. This step-by-step reduction confirms the operation without auxiliary constructs.^[18]

Successor and Predecessor Functions

The successor function for Church numerals, denoted as \mathsf{succ}, increments a numeral n by applying its function one additional time. It is defined as \mathsf{succ} = \lambda n . \lambda f . \lambda x . f (n f x), which effectively inserts one more application of f to the base value x encoded by n.^[20] This construction preserves the iterative nature of Church numerals, where \mathsf{succ}\ n represents the numeral for n+1.^[3] Defining a predecessor function, denoted \mathsf{pred}, presents significant challenges in the untyped lambda calculus because Church numerals lack a direct mechanism for decrementing; instead, numerical values are built through repeated function application, requiring indirect simulation via iteration to "count down."^[21] To overcome this, \mathsf{pred} leverages Church pairs to track intermediate values during iteration, encoding the process such that applying the numeral n times to an initial pair yields a final pair whose second component is n and first is n-1. Specifically, \mathsf{pred} = \lambda n . \mathsf{first} (n\ \mathsf{next}\ (\mathsf{pair}\ \mathsf{zero}\ \mathsf{zero})), where \mathsf{next} = \lambda p . \mathsf{pair}\ (\mathsf{second}\ p)\ (\mathsf{succ}\ (\mathsf{second}\ p)), \mathsf{pair} = \lambda x . \lambda y . \lambda z . z\ x\ y, \mathsf{first} = \lambda p . p\ \mathsf{true}, and \mathsf{second} = \lambda p . p\ \mathsf{false}.^[21] This approach uses pairs, previously defined in Church encoding, to maintain a running predecessor while incrementing a counter.^[21] For example, applying \mathsf{pred} to the Church numeral $2 = \lambda f . \lambda x . f (f x) begins with the pair (\mathsf{zero}, \mathsf{zero}). The first iteration yields (\mathsf{zero}, \mathsf{one}), and the second yields (\mathsf{one}, 2); extracting the first component returns \mathsf{one}.^[21] For n = 0, the result is \mathsf{zero}, ensuring consistency.

Advanced Numerical Representations

Signed Numbers

Signed integers in Church encoding are represented as pairs consisting of a Church boolean indicating the sign and a Church numeral representing the absolute value or magnitude. The true boolean, defined as \lambda t.\lambda f. t, denotes a positive sign, while the false boolean, \lambda t.\lambda f. f, denotes a negative sign. For instance, the positive integer +3 is encoded as the pair (true, 3), where 3 is the Church numeral \lambda f.\lambda x. f (f (f x)), and -3 as (false, 3). This pair-based approach leverages the existing encodings of booleans and numerals to handle negatives purely within the lambda calculus, without introducing primitive integer operations.^[22] The absolute value of a signed integer s is obtained by projecting the second component of the pair, effectively discarding the sign: \lambda s. \text{second } s. To negate a signed integer, the sign boolean is flipped using a negation function on booleans, such as \text{Neg} = \lambda b. b\ \mathsf{false}\ \mathsf{true}, yielding \lambda s. \text{pair } (\text{Neg } (\text{first } s)) (\text{second } s). For example, applying negation to +3 produces (false, 3), or -3. This enables basic manipulations of signed representations while preserving the functional nature of Church encodings. Comparisons between signed integers, such as determining if one is greater than another, account for both signs and magnitudes. The greater-than function can be defined by first comparing signs: if both are positive or both negative, compare magnitudes using unsigned comparison; if signs differ, the positive one is greater unless its magnitude is zero. This adapts the unsigned comparison from natural number arithmetic to the signed domain by conditioning on the sign booleans. A key advantage of this encoding is its ability to support full integer arithmetic, including operations on negatives, solely through lambda terms. For addition, magnitudes are adjusted conditionally based on signs: if signs match, add the magnitudes and retain the sign; if they differ, subtract the smaller magnitude from the larger and assign the sign of the larger. For example, adding +2, encoded as (true, 2), and -1, as (false, 1), involves subtracting 1 from 2 (yielding magnitude 1) and assigning the positive sign, resulting in +1. Such operations build on magnitude computations from unsigned arithmetic, extended via sign handling.

Rational and Real Numbers

In Church encoding, rational numbers are represented as pairs of Church numerals for the numerator and denominator, assuming positive denominators and allowing signed numerators to handle negative values as defined in signed number encodings.^[23] This encoding leverages the Church pair construction, where a rational \frac{p}{q} is the term \lambda z. z \, p \, q, with p and q as Church numerals.^[23] Arithmetic operations on rationals are defined by composing the encoded integer operations. For addition, the sum of \frac{r_1}{s_1} and \frac{r_2}{s_2} is encoded as \lambda r_1. \lambda s_1. \lambda r_2. \lambda s_2. pair (\mathsf{Add} \, (\mathsf{Mul} \, r_1 \, s_2) \, (\mathsf{Mul} \, r_2 \, s_1)) \, (\mathsf{Mul} \, s_1 \, s_2), where \mathsf{Add} and \mathsf{Mul} are the Church-encoded addition and multiplication on numerals.^[23] Similar compositions define multiplication as \lambda r_1. \lambda s_1. \lambda r_2. \lambda s_2. pair (\mathsf{Mul} \, r_1 \, r_2) \, (\mathsf{Mul} \, s_1 \, s_2) and other operations. To normalize a fraction \frac{p}{q} to lowest terms, compute the greatest common divisor g = \gcd(|p|, q) using a recursively defined Euclidean algorithm encoded via the fixed-point combinator in lambda calculus, then divide both by g.^[23] For example, the rational \frac{1}{2} is the pair of Church numerals 1 and 2. Adding \frac{1}{3}, represented as the pair of 1 and 3, yields the pair of 5 and 6 before normalization, or \frac{5}{6} after applying the GCD (which is 1).^[23] Real numbers in Church encoding are more complex due to their continuity and require representations that capture infinite precision, often linking to computable reals. One approach uses Dedekind cuts, encoding a real as a pair of lower and upper sets of rationals: the lower set L contains all rationals strictly less than the real, and the upper set U contains all rationals strictly greater, with L and U disjoint, nonempty, and satisfying the Dedekind properties (no maximum in L, no minimum in U).^[24] These sets are represented as lambda terms acting as predicates on rationals: the lower cut \delta is \lambda d. \, d < a (returning a Church boolean true if rational d is in L), and the upper cut \upsilon is \lambda u. \, a < u, forming the pair (\delta, \upsilon).^[24] This encoding ensures exact representation through the lambda terms' computational content, as explored in Abstract Stone Duality (ASD), where reals form a subspace of pairs of rational predicates with infinite precision for arithmetic operations extended continuously from rationals.^[24] Computable reals arise when the predicates are computable functions, aligning with Bauer's framework for exact real computation in lambda-based models, avoiding approximation errors inherent in finite representations.^[24] Alternatively, reals can be encoded via Cauchy sequences of rationals, represented as infinite streams (encoded recursively) converging to the real within specified error bounds, though this requires handling limits through fixed-point recursion.^[24]

Translations to Other Representations

Church encodings of natural numbers can be translated to other numeral systems to facilitate interoperability with different computational paradigms or to leverage alternative representations for efficiency or expressiveness. One common translation maps Church numerals to binary representations, where individual bits are encoded as Church booleans (true for 1 and false for 0), and the numeral itself is represented as a list of these bits constructed via iterated cons operations on pairs. For instance, the Church numeral for 3, which applies its function three times, can be converted to the binary representation 11 by building a bit list as the pair of true and the pair of true and false, effectively encoding the value through the structure of the list rather than repeated application. This approach allows for more compact storage in systems supporting binary operations, as demonstrated in left-associated binary numeral systems within lambda calculus. Another mapping exists from Peano numerals, defined inductively with zero and a successor function, to Church numerals, where the Peano successor directly corresponds to the Church successor that increments by wrapping an additional function application. This translation preserves the iterative structure of natural numbers, linking the inductive definition in Peano arithmetic to the functional iteration in lambda terms, and enables proofs of equivalence between the two systems through fold operations on data types.^[25] Church numerals also align closely with von Neumann ordinals from set theory, where the numeral n is represented as \lambda f. \lambda x. f^n x, mirroring the von Neumann construction of ordinals as transitive sets containing all smaller ordinals, but adapted to functional form with explicit recursion over applications rather than set membership. This similarity highlights the expressive power of lambda calculus in modeling set-theoretic constructs without primitive sets. These translations underscore the universality of Church encodings, as they can be converted to alternative forms like Scott numerals—where numbers are case analyzers distinguishing zero from successors—using fixed-point combinators to bridge the iterative Church style with the eliminative Scott approach, enabling seamless operations across encodings.^[26] For binary lists, such conversions may reference list encodings briefly to handle the cons-based structure.

Data Structure Encodings

List Encodings

In Church encoding, lists are represented functionally using higher-order terms that capture their recursive structure through iteration or folding, allowing operations to be defined uniformly without primitive data types. The empty list, denoted as nil, is encoded as the lambda term \lambda c. \lambda n. n, which selects the neutral element n when applied to a continuation c and neutral n, effectively acting like the Church boolean false in selection but enabling an empty-list check to behave as true via \lambda l. l (\lambda h. \lambda t. \text{false}) \text{true}. The constructor cons, which prepends an element h (head) to a list t (tail), is defined as \lambda h. \lambda t. \lambda c. \lambda n. c\, h\, (t\, c\, n). This encoding represents the list as a right fold, where applying the list to a combining function c and neutral n iterates c over each head element, starting from the rightmost (building right-associatively), thus processing the list in a functional manner without explicit recursion. For example, the list consisting of elements a followed by b followed by nil would apply c\, a\, (c\, b\, n). The head operation extracts the first element of a non-empty list and is encoded as \lambda l. l\, (\lambda h. \lambda t. h)\, \bot, where \bot is an error term or default value invoked on nil (e.g., yielding an undefined or exceptional result). Similarly, the tail operation returns the rest of the list and is given by \lambda l. l\, (\lambda h. \lambda t. t)\, \bot, again using \bot for the empty case. These definitions leverage the fold structure: for a list l = \text{cons}\, h\, t, head reduces to h by selecting the head in the cons case, while tail reduces to t. An alternative pair-based encoding composes lists from nested Church pairs, where cons h\, t forms a pair (h, t), resulting in right-nested structures like ((a, (b, \text{nil}))) for a list [a, b], with head and tail as the pair's first and second projections, respectively. This builds on Church pairs as foundational combinators but emphasizes functional processing in the primary fold-based approach.

Scott Encoding for Lists

Scott encoding provides an alternative representation of lists in the untyped lambda calculus that directly mirrors the structure of algebraic data types, enabling pattern matching through higher-order functions rather than relying on pairs for cons cells.^[27] In this encoding, a list is treated as a function that accepts two arguments: a cons case handler c (of type head × tail → result) and a nil case handler n (of type result), applying the appropriate one based on the list's structure. This approach is isomorphic to the inductive type for lists, \text{List } A = 1 + A \times \text{List } A, where the empty list corresponds to the unit and non-empty lists to the product.^[27] The empty list, nil, is encoded as \lambda c. \lambda n. n, which selects the nil handler when applied. A non-empty list cons h t (with head h and tail t) is encoded as \lambda c. \lambda n. c \, h \, t, invoking the cons handler with the head and tail. This functional representation facilitates direct recursion over the data structure, as the list itself drives the case analysis without needing additional projectors or deconstructors.^[27] Common operations on Scott-encoded lists leverage this pattern-matching capability. The right fold, foldr, which accumulates a value from the end of the list using a binary function f (of type A \times B \to B) and initial value z (of type B), is defined as \lambda l. \lambda z. \lambda f. l \, f \, z. For the empty list, this reduces to z; for a non-empty list, it applies f to the head and the fold over the tail. Similarly, the map function, which applies a unary function f (of type A \to A) to each element, is \lambda l. \lambda f. l \, (\lambda h. \lambda t. \text{cons} \, (f \, h) \, t) \, \text{nil}, reconstructing the list by transforming each head while preserving the structure. These definitions exploit the Scott encoding's inherent recursion support, making it more straightforward for structural induction compared to pair-based encodings.^[27] For instance, consider a list encoding the numerals [1, 2], represented as \text{cons} \, \mathbf{1} \, (\text{cons} \, \mathbf{2} \, \text{nil}), where \mathbf{1} and \mathbf{2} are Church numerals. Applying map with the successor function \text{succ} (defined as \lambda n. n \, \text{add} \, \mathbf{1}, where add is addition) yields \text{cons} \, \mathbf{2} \, (\text{cons} \, \mathbf{3} \, \text{nil}), corresponding to [2, 3], through successive beta-reductions that transform each element.^[27]

References

[1]
Lambda Calculi | Internet Encyclopedia of Philosophy
Alonzo Church first introduced the λ -calculus as “A set of postulates for the foundation of logic” in two papers of that title published in 1932 and 1933.The Untyped Lambda Calculus · Expressiveness · Philosophical Importance
[2]
A Set of Postulates For the Foundation of Logic - jstor
BY ALONZO CHURCH. 1. Revision of the list of formal postulates. In a recent paper' the author proposed a set of postulates which, it was believed, would ...
[3]
[PDF] CS 6110 S18 Lecture 3 λ-Calculus Encodings
The Church numeral for the number n ∈ N is denoted n. It is the λ-term λfx.fn x, where fn denotes the n-fold composition of f with itself: 0 ≜ λfx.
[4]
Alonzo Church - Stanford Encyclopedia of Philosophy
Oct 21, 2021 · 1933, “A Set of Postulates For the Foundation of Logic (2)”, The Annals of Mathematics, 34(4): 839–864. Reprinted in BE: 68–87. doi:10.2307 ...
[5]
The Church-Turing Thesis (Stanford Encyclopedia of Philosophy)
Jan 8, 1997 · The Church-Turing thesis concerns the concept of an effective or systematic or mechanical method, as used in logic, mathematics and computer science.
[6]
[PDF] An Unsolvable Problem of Elementary Number Theory Alonzo ...
Mar 3, 2008 · The purpose of the present paper is to propose a definition of effective calculability which is thought to correspond satisfactorily to the ...
[7]
Recursive Functions - Stanford Encyclopedia of Philosophy
Apr 23, 2020 · Such a demonstration was given by Church (1936b)—and in greater detail by Kleene 1936b—providing the first of several extensional equivalence ...
[8]
Lambda calculus
Lambda calculus is historically significant. Alonzo Church was Alan Turing's doctoral advisor, and his lambda calculus predates Turing machines.
[9]
3.8. Church Numerals and Booleans - OpenDSA
To turn the λ calculus into a “real” programming language, we need to be able to manipulate: Boolean constants (true, false). logical operators (and, or, not).
[10]
[PDF] Lambda Calculus
pair x y z = z x y fst x y = x snd x y = y pair = λx.λy.λz. z x y fst = λx.λy.x snd = λx.λy.y pair True False first = (λx.λy.λz. z x y) (λx.λy.x) (λx.λy.y) (λx.
[11]
[PDF] Lecture 7 — Lambda Calculus - Washington
Is it weird that the encodings of Booleans and pairs both used λx. λy. x and ... ▷ Simple Lambda encodings (it is Turing complete!) (done). ▷ Other ...
[12]
[PDF] Encoding Data in Lambda Calculus: An Introduction
Sep 26, 2017 · If we have type, then pair : A → B → A × B, p1 : A × B → A, p2 : A × B → B. Definition 7 (Church numerals). Zero Z := λz.λs.z. Successor S ...Missing: original | Show results with:original
[13]
[PDF] Lambda Calculus Encodings | CMSC 330 - UMD Computer Science
Church's encoding of mathematical logic. • true = λx.λy.x. • false = λx.λy.y ... IsZero? • iszero = λz.z (λy.false) true. This is equivalent to λz.((z (λy ...
[14]
[PDF] Lambda calculus encodings and Recursion; Definitional translations ...
Feb 25, 2016 · (d) In class we made use of a combinator ISZERO, which takes a Church encoding of a natural number ... if it is applied to a lambda term that is ...
[15]
[PDF] Programming Languages and Lambda Calculi
due to Church, and the encoded numbers are therefore called Church numerals. ... To generalize iszero to number equality, we need subtraction. In the same ...
[16]
[PDF] THE CALCULI OF LAMBDA-CONVERSION
The Calculi of Lambda-Conversion, by ALONZO CHURCH. 7 Finite Dimensional Vector Spaces, by PAUL R. HALMOS. 10. Topics in Topology, by SOLOMON LEFSCHETZ. 11 ...Missing: encoding | Show results with:encoding
[17]
[PDF] 1 Booleans 2 Natural Numbers - Ethan Cecchetti
There are many reasonable encodings for numerous datatypes. We will explore Church encodings, named for Alonzo Church who first proposed them. 1 Booleans.
[18]
[PDF] Lambda Calculus - CMU School of Computer Science
Jan 30, 2020 · But we'll stop here. Page 45. Predecessor. Predecessor using pairs: SUBTRACT := λm.λn.n PRED m. PRED := λn. FIRST (n NEXT (PAIR 0 0)). To ...
[19]
[PDF] Introduction to Lambda Calculus Henk Barendregt Erik Barendsen ...
(1) Church (1936) invented a formal system called the lambda calculus and defined the notion of computable function via this system. (2) Turing (1936/7) ...
[20]
Dixin's Blog - Lambda Calculus via C# (4) Tuple and Signed Numeral
Nov 10, 2024 · Signed numeral. With tuple, a signed numeral (integer) can be modeled by a pair ... Church numeral represents natural number. So Converting ...
[21]
[PDF] Church Numerals - People @EECS
The study of how to do this is "lambda calculus," a branch of mathematics invented by Alonzo Church. ("Lambda" is what the non-Snap! world calls gray rings. In ...Missing: encoding | Show results with:encoding
[22]
[PDF] The Dedekind Reals in Abstract Stone Duality
Jul 3, 2005 · Since rational numbers are easily encoded,. e.g. as pairs of integers, real numbers can therefore be represented as pairs of λ-terms. Remark ...
[23]
[PDF] An Adequate Left-Associated Binary Numeral System in the λ-Calculus
Mar 14, 1996 · In this paper, we present an adequate binary numeral system for the λ- calculus, where the successor function, the predecessor function, and the ...
[24]
(PDF) Theoretical pearl - Church numerals, twice! - ResearchGate
Aug 7, 2025 · This pearl explains Church numerals, twice. The first explanation links Church numerals to Peano numerals via the well-known encoding of data ...Missing: literature | Show results with:literature
[25]
Programming in the λ-Calculus: From Church to Scott and Back
The transformation is based on using the Scott-encoding for Algebraic Data Types instead of the more common Church encoding. In this way we not only obtain ...Missing: translation | Show results with:translation
[26]
[PDF] The Church-Scott representation of inductive and coinductive data
Data in the lambda calculus is usually represented using the "Church encoding", which gives closed terms for the constructors and which naturally allows to ...