Church Encoding

lambda-calculus

Definition

Church Encoding

Church encodings are a way to represent data structures as functions that act on other functions.

Boolean Logic

$$\begin{array}{rl}\mathbf{T}& =\lambda xy.x\\ \mathbf{F}& =\lambda xy.x\\ \mathbf{ITE}& =\lambda pxy.pxy\\ & \\ \mathbf{and}& =\lambda pq.pqp\\ \mathbf{or}& =\lambda pq.ppp\\ \mathbf{not}& =\lambda pab.pba\end{array}$$

Note that $\mathbf{ITE}$ is the ITE function.

Example

$$\begin{array}{rl}\mathbf{ITE}\mathbf{T}ab& =(\lambda pxy.pxy)\mathbf{T}ab\\ & {\to }_{\beta }(\lambda xy.\mathbf{T}xy)ab\\ & {\to }_{\beta }(\lambda y.\mathbf{T}ay)b\\ & {\to }_{\beta }\mathbf{T}ab\\ & {\to }_{\beta }(\lambda xy.x)ab\\ & {\to }_{\beta }(\lambda y.a)b\\ & {\to }_{\beta }a\end{array}$$

todo

K Combinator

Definition

K Combinator

The K combinator is a combinator used in Church encoding to represent true (boolean value).

$$\mathbf{T}=\lambda xy.x$$

Link to original

Numerals

Definition

Church Numeral

Church numerals are a type of Church encoding for natural numbers.

The general form for a Church numeral $n\in \mathbb{N}$ is:

$$n\equiv \lambda f.\lambda x.f^{n}x$$

where $f^{n}x$ is a shorthand for applying $f$ repeatedly $n$ times.

$$\begin{array}{rl}0& \equiv \lambda f.\lambda x.x\\ 1& \equiv \lambda f.\lambda x.fx\\ 2& \equiv \lambda f.\lambda x.ffx\\ 3& \equiv \lambda f.\lambda x.fffx\\ & ⋮\end{array}$$

Link to original

Arithmetic Functions

$$\begin{array}{rl}\mathbf{succ}& =\lambda nfx.f(nfx)\\ \mathbf{add}& =\lambda mnfx.mf(nfx)\\ \mathbf{mul}& =\lambda mnf.m(nf)\end{array}$$