# [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.f0 x
1 := λfx.f x                ≡ λf.λx.f x                 ≡ λf.λx.f1 x
2 := λfx.f (f x)            ≡ λf.λx.(f ∘ f) x           ≡ λf.λx.f2 x
3 := λfx.f (f (f x))        ≡ λf.λx.(f ∘ f ∘ f) x       ≡ λf.λx.f3 x
...
n := λfx.f (f ... (f x)...) ≡ λf.λx.(f ∘ f ∘ ... ∘ f) x ≡ λf.λx.fn 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)

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

### Comparison

```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 sp  sn) (λx.ToSigned 0) (λx.If (IsGreater sp sn) (λy.ToSigned (Subtract sp sn)) (λy.Negate (ToSigned (Subtract sn sp))))```

### Arithmetic

```AddSigned := λa.λb.FormatWithZero (CreateTuple (Add ap bp) (Add an bn))

MultiplySigned := λa.λb.FormatWithZero (CreateTuple (Add (Multiply ap bp) (Multiply an bn)) (Add (Multiply ap bn) (Multiply an bp)))

DivideBySigned := λa.λb.FormatWithZero (CreateTuple (Add (DivideByIgnoreZero ap bp) + (DivideByIgnoreZero an bn)) (Add (DivideByIgnoreZero ap bn) (DivideByIgnoreZero an bp))))
```

# 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: (sreal, simaginary), which represents complex integer z = sreal + simaginary * i.

With signed number, rational number can also be encoded by a Church pair of a signed number and a Church numeral: (snumerator, ndenominator), which represents rational number q = snumerator / (1 + ndenominator).

Dyadic rational number can be encoded by (snumerator, nexponent) as well, which represents d = snumerator / (2 ^ nexponent).

## 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 p0 = (q0, q0’), p1 = (q1, q1’), p2 = (q2, q2’), …, such that:
• pn represents a rational interval, since qn and qn’ are both rational numbers.
• pn + 1 ⊆ pn
• limn → ∞ qn’ − qn = 0
• r = ∩n ∈ N pn
• r can be represented by a Cauchy sequence of rational numbers q0, q1, q2, …, and a function f of type Func<_Numeral, _Numeral>, defining the convergence rate of the Cauchy sequence such that:
• ∀i.j.k. | qf(i) + j - qf(i) + k | ≤ 2-i
• r = limn → ∞ qn
• r can be represented by a Cauchy sequence of rational numbers q0, q1, q2, … with a fixed convergence rate, such that:
• ∀i.j. | qi - qi + j | ≤ 1 / i
• r = limn → ∞ qn

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 (rreal, rimaginary), which represents complex number z = rreal + rimaginary * 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.