[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.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)
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

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

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

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: (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₀ = (q₀, q₀’), p₁ = (q₁, q₁’), p₂ = (q₂, q₂’), …, 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
• r can be represented by a Cauchy sequence of rational numbers q₀, q₁, q₂, …, 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
• r can be represented by a Cauchy sequence of rational numbers q₀, q₁, q₂, … with a fixed convergence rate, such that:
  • ∀i.j. | q_i - q_{i + j} | ≤ 1 / i
  • r = lim_{n → ∞} 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.