# Lambda Calculus via C# (19) Church Encoding, And More

# [LINQ via C# series]

# [Lambda Calculus via C# series]

So far a ton has been encoded. Here is a summary.

# Summary of church encoding

## Boolean

```
True := λt.λf.t
False := λt.λf.f
```

### Boolean logic

```
And := λa.λb.a b False
Or := λa.λb.a True b
Not := λb.b False True
Xor := λa.λb.a (b False True) (b True False)
```

### If logic

`If := λc.λt.λf.c t f (λx.x)`

## Numeral

`0 := λfx.x ≡ λf.λx.x ≡ λf.λx.f`^{0} x
1 := λfx.f x ≡ λf.λx.f x ≡ λf.λx.f^{1} x
2 := λfx.f (f x) ≡ λf.λx.(f ∘ f) x ≡ λf.λx.f^{2} x
3 := λfx.f (f (f x)) ≡ λf.λx.(f ∘ f ∘ f) x ≡ λf.λx.f^{3} x
...
n := λfx.f (f ... (f x)...) ≡ λf.λx.(f ∘ f ∘ ... ∘ f) x ≡ λf.λx.f^{n} x

### Arithmetic

```
Increase := λn.λf.λx.f (n f x)
Increase2 := λn.λf.f ∘ (n f)
Add := λa.λb.λf.λx.a f (b f x)
Add2 := λa.λb.λf.fa ∘ fb ≡ λa.λb.λf.(a f) ∘ (b f)
Add3 := λa.λb.a Increase b
Decrease := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
Decrease2 := λn.Item1 (n (Shift Increase) (CreateTuple 0 0))
Subtract := λa.λb.b Decrease a
Multiply := λa.λb.a (λx.Add b x) 0
_DivideBy := λa.λb.If (IsGreaterOrEqual a b) (λx.Add One (_DivideBy (Subtract a b) b)) (λx.Zero)
DivideByIgnoreZero = λa.λb.If (IsZero b) (λx.0) (λx._DivideBy a b)
Pow := λm.λ e.e (λx.Multiply m x) 1
```

A better DivideBy will be re-implemented after introducing Y combinator:

```
DivideBy := Y (λf.λa.λb.If (IsGreaterOrEqual a b) (λx.Add One (f (Subtract a b) b)) (λx.Zero))
≡ (λf.(λx.f (x x)) (λx.f (x x))) (λf.λa.λb.If (IsGreaterOrEqual a b) (λx.Add One (f (Subtract a b) b)) (λx.Zero))
```

So DivideByIgnoreZero can by redefined using DivideBy instead of _DivideBy:

`DivideByIgnoreZero = λa.λb.If (IsZero b) (λx.0) (λx.DivideBy a b)`

## Predicate

`IsZero := λn.n (λx.False) True`

### Compari_{}son

```
IsLessOrEqual := λa.λb.IsZero (Subtract a b)
IsGreaterOrEqual := λa.λb.IsZero (Subtract b a)
IsEqual := λa.λb.And (IsLessOrEqual a b) (IsGreaterOrEqual a b)
IsLess := λa.λb.Not (IsGreaterOrEqual a b)
IsGreater := λa.λb.Not (IsLessOrEqual a b)
IsNotEqual := λa.λb.Not (IsEqual a b)
```

## Pair (2-tuple)

```
CreateTuple := λx.λy.λf.f x y
Tuple := λf.f x y
Item1 := λt.t True
Item2 := λt.t False
Shift := λf.λt.CreateTuple (Item2 t) (f (Item1 t))
Swap := λt.CreateTuple (Item2 t) (Item1 t)
```

## List

### 1 pair for each node, and null

```
CreateListNode := CreateTuple ≡ λv.λn.λf.f v n
Value := Item1 ≡ λl.l (λv.λn.v)
Next := Item2 ≡ λl.l (λv.λn.n)
Null := False
IsNull := λl.l (λv.λn.λx.False) True
Index := λl.λi.i Next l
```

### 2 pairs for each node, and null

```
CreateListNode2 := λv.λn.CreateTuple False (CreateTuple v n)
Value2 := λl.Item1 (Item2 l)
Next2 := λl.If (IsNull2 l) (λx.l) (λx.(Item2 (Item2 l)))
Null2 := λf.True
IsNull2 := λl.(Item1 l)
Index2 := λl.λi.i Next2 l
```

### Fold (aggregate) function for each node, and null

```
CreateListNode3 := λv.λn.λf.λx.f v (n f x)
Value3 := λl.λx.l (λv.λy.v) x
Next3 := λl.Item2 (l (λv.λt.ShiftTuple (CreateListNode3 v)) (CreateTuple Null3 Null3))
Null3 := λf.λx.x
IsNull3 := λl.l (λv.λx.False) True
Index3 := λl.λi.i Next3 l
```

## Signed number

```
Signed := Tuple
ToSigned := λn.CreateTuple n 0
Negate := Swap
Positive := Item1
Negative := Item2
FormatWithZero := λs.If (IsEqual s
```_{p} s_{n}) (λx.ToSigned 0) (λx.If (IsGreater s_{p} s_{n}) (λy.ToSigned (Subtract s_{p} s_{n})) (λy.Negate (ToSigned (Subtract s_{n} s_{p}))))

### Arithmetic

`AddSigned := λa.λb.FormatWithZero (CreateTuple (Add a`_{p} b_{p}) (Add a_{n} b_{n}))
SubtractSigned := λa.λb.FormatWithZero (CreateTuple (Add a_{p} b_{n}) (Add a_{n} b_{p}))
MultiplySigned := λa.λb.FormatWithZero (CreateTuple (Add (Multiply a_{p} b_{p}) (Multiply a_{n} b_{n})) (Add (Multiply a_{p} b_{n}) (Multiply a_{n} b_{p})))
DivideBySigned := λa.λb.FormatWithZero (CreateTuple (Add (DivideByIgnoreZero a_{p} b_{p}) + (DivideByIgnoreZero a_{n} b_{n})) (Add (DivideByIgnoreZero a_{p} b_{n}) (DivideByIgnoreZero a_{n} b_{p}))))

# Encode, encode, and encode

## From signed number to complex integer and rational number

With signed number, complex integer can be encoded by a Church pair of signed numbers: (s_{real}, s_{imaginary}), which represents complex integer z = s_{real} + s_{imaginary} * i.

With signed number, rational number can also be encoded by a Church pair of a signed number and a Church numeral: (s_{numerator}, n_{denominator}), which represents rational number q = s_{numerator} / (1 + n_{denominator}).

Dyadic rational number can be encoded by (s_{numerator}, n_{exponent}) as well, which represents d = s_{numerator} / (2 ^ n_{exponent}).

## From rational number to real number and complex number

Then with rational number, a real number r can be encoded in many different ways:

- r can be represented by a sequence of Church pair of 2 rational numbers p
_{0}= (q_{0}, q_{0}’), p_{1}= (q_{1}, q_{1}’), p_{2}= (q_{2}, q_{2}’), …, such that:- p
_{n}represents a rational interval, since q_{n}and q_{n}’ are both rational numbers. - p
_{n + 1}⊆ p_{n} - lim
_{n → ∞ }q_{n}’ − q_{n}= 0 - r = ∩
_{n ∈ N }p_{n}

- p
- r can be represented by a Cauchy sequence of rational numbers q
_{0}, q_{1}, q_{2}, …, and a function f of type Func<_Numeral, _Numeral>, defining the convergence rate of the Cauchy sequence such that:- ∀i.j.k. | q
_{f(i) + j}- q_{f(i) + k}| ≤ 2^{-i} - r = lim
_{n → ∞ }q_{n}

- ∀i.j.k. | q
- r can be represented by a Cauchy sequence of rational numbers q
_{0}, q_{1}, q_{2}, … with a fixed convergence rate, such that:- ∀i.j. | q
_{i}- q_{i + j}| ≤ 1 / i - r = lim
_{n → ∞ }q_{n}

- ∀i.j. | q

etc.. An example in Haskell can be found on Github.

With real number, complex number can be naturally encoded by a Church pair of 2 real numbers (r_{real}, r_{imaginary}), which represents complex number z = r_{real} + r_{imaginary} * i.

## And much more

Church pair can encode more complex data structures, like tree.

Church List can encode string.

Church Tuple and Church List can encode more complex algebra types.

…

Don’t worry. The encoding stops here. All the above data types and functions demonstrate that any data type or calculation may be encoded in lambda calculus. This is the Church-Turing thesis.