Lambda Calculus via C# (19) Church Encoding and More

908 words

5 minutes

Lambda Calculus via C# (19) Church Encoding and More

2018-11-19

C#

.NET

/

.NET Core

/

.NET Standard

/

C#

/

LINQ

TIP
Functional Programming and 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 #

1
True := λt.λf.t
2
False := λt.λf.f

Boolean logic #

1
And :=  λa.λb.a b False
2
Or :=  λa.λb.a True b
3
Not := λb.b False True
4
Xor := λa.λb.a (b False True) (b True False)

If logic #

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

Numeral #

1
0 := λfx.x                  ≡ λf.λx.x                   ≡ λf.λx.f0 x
2
1 := λfx.f x                ≡ λf.λx.f x                 ≡ λf.λx.f1 x
3
2 := λfx.f (f x)            ≡ λf.λx.(f ∘ f) x           ≡ λf.λx.f2 x
4
3 := λfx.f (f (f x))        ≡ λf.λx.(f ∘ f ∘ f) x       ≡ λf.λx.f3 x
5
...
6
n := λfx.f (f ... (f x)...) ≡ λf.λx.(f ∘ f ∘ ... ∘ f) x ≡ λf.λx.fn x

Arithmetic #

1
Increase := λn.λf.λx.f (n f x)
2
Increase2 := λn.λf.f ∘ (n f)
3

4
Add := λa.λb.λf.λx.a f (b f x)
5
Add2 := λa.λb.λf.fa ∘ fb ≡ λa.λb.λf.(a f) ∘ (b f)
6
Add3 := λa.λb.a Increase b
7

8
Decrease := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
9
Decrease2 := λn.Item1 (n (Shift Increase) (CreateTuple 0 0))
10

11
Subtract := λa.λb.b Decrease a
12

13
Multiply := λa.λb.a (λx.Add b x) 0
14

15
_DivideBy := λa.λb.If (IsGreaterOrEqual a b) (λx.Add One (_DivideBy (Subtract a b) b)) (λx.Zero)
16
DivideByIgnoreZero = λa.λb.If (IsZero b) (λx.0) (λx._DivideBy a b)
17

18
Pow := λm.λ e.e (λx.Multiply m x) 1

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

1
DivideBy := Y (λf.λa.λb.If (IsGreaterOrEqual a b) (λx.Add One (f (Subtract a b) b)) (λx.Zero))
2
          ≡ (λ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:

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

Predicate #

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

Comparison #

1
IsLessOrEqual := λa.λb.IsZero (Subtract a b)
2
IsGreaterOrEqual := λa.λb.IsZero (Subtract b a)
3

4
IsEqual := λa.λb.And (IsLessOrEqual a b) (IsGreaterOrEqual a b)
5

6
IsLess := λa.λb.Not (IsGreaterOrEqual a b)
7
IsGreater := λa.λb.Not (IsLessOrEqual a b)
8
IsNotEqual := λa.λb.Not (IsEqual a b)

Pair (2-tuple)#

1
CreateTuple := λx.λy.λf.f x y
2
Tuple := λf.f x y
3

4
Item1 := λt.t True
5
Item2 := λt.t False
6

7
Shift := λf.λt.CreateTuple (Item2 t) (f (Item1 t))
8
Swap := λt.CreateTuple (Item2 t) (Item1 t)

List#

1 pair for each node, and null #

1
CreateListNode := CreateTuple ≡ λv.λn.λf.f v n
2

3
Value := Item1 ≡ λl.l (λv.λn.v)
4
Next := Item2 ≡ λl.l (λv.λn.n)
5

6
Null := False
7
IsNull := λl.l (λv.λn.λx.False) True
8

9
Index := λl.λi.i Next l

2 pairs for each node, and null #

1
CreateListNode2 := λv.λn.CreateTuple False (CreateTuple v n)
2

3
Value2 := λl.Item1 (Item2 l)
4
Next2 := λl.If (IsNull2 l) (λx.l) (λx.(Item2 (Item2 l)))
5

6
Null2 := λf.True
7
IsNull2 := λl.(Item1 l)
8

9
Index2 := λl.λi.i Next2 l

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

1
CreateListNode3 := λv.λn.λf.λx.f v (n f x)
2

3
Value3 := λl.λx.l (λv.λy.v) x
4
Next3 := λl.Item2  (l (λv.λt.ShiftTuple (CreateListNode3 v)) (CreateTuple Null3 Null3))
5

6
Null3 := λf.λx.x
7
IsNull3 := λl.l (λv.λx.False) True
8

9
Index3 := λl.λi.i Next3 l

Signed number #

1
Signed := Tuple
2
ToSigned := λn.CreateTuple n 0
3
Negate := Swap
4

5
Positive := Item1
6
Negative := Item2
7

8
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#

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

3
SubtractSigned := λa.λb.FormatWithZero (CreateTuple (Add ap bn) (Add an bp))
4

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

7
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: $(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 = \frac{s_{numerator}}{1 + n_{denominator}}$

Dyadic rational number can be encoded by $(s_{numerator}, n_{exponent})$ as well, which represents:

$d = \frac{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_{0} = (q_{0}, q_{0}^{'})$ , $p_{1} = (q_{1}, q_{1}')$ $p_{1} = (q_{1}, q_{1}^{'})$ , $p_{2} = (q_{2}, q_{2}')$ $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} \subseteq p_{n}$
- $\lim \limits_{n \to \infty} q_{n}' - q_{n} = 0$
- $r = \bigcap_{n ∈ N}p_{n}$
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:
- $\forall i.j.k. | q_{f(i) + j} - q_{f(i) + k} | ≤ 2 ^ {-i}$
- $r = \lim \limits_{n \to \infty} q_{n}$
r can be represented by a Cauchy sequence of rational numbers q0, q1, q2, … with a fixed convergence rate, such that:
- $\forall i.j. | q_{i} - q_{i + j} | ≤ \frac{1}{i}$
- $r = \lim \limits_{n \to \infty} q_{n}$

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.