Dixin's Blog
Dixin is a UI designer and knows a little bit about programming.

Lambda Calculus via C# (24) Undecidability of Equivalence
[LINQ via C#]  [Lambda Calculus]
All the previous parts were demonstrating what lambda calculus can do  like abstracting functions, applying functions, encoding data types and data structures…. Yes, lambda calculus is powerful, and it’s Turing complete. So it is also interesting what cannot be done with lambda expressions  predict if 2 lambda expressions are equivalent.

Lambda Calculus via C# (23) Y Combinator, And Divide
[LINQ via C#]  [Lambda Calculus]
Fix point
p is the fixed point of function F if and only if:
p ≡ F p
The following picture is stolen from Wikipedia:
A simple example:
F := 0  x
has a fixed point 0:
0 ≡ F 0

Lambda Calculus via C# (22) Iota Combinator
[LINQ via C#]  [Lambda Calculus]
Language with 1 element
Iota is an esoteric programming language with minimum elements but still Turingcomplete. Iota's universal combinator is:
ι := λf.f S K ≡ λf.f (λx.λy.λz.x z (y z)) (λx.λy.x)
That’s the whole language.

Lambda Calculus via C# (21) SKI Combinator Calculus
[LINQ via C#]  [Lambda Calculus]
The previous part shows SKI calculus is untyped and strongly typed C# implementation does not work. So here comes the SKI in untyped C#:
public static partial class SkiCombinators { public static Func<dynamic, Func<dynamic, Func<dynamic, dynamic>>> S = x => y => z => x(z)(y(z)); public static Func<dynamic, Func<dynamic, dynamic>> K = x => _ => x; public static Func<dynamic, dynamic> I = x => x; }
Notice closed types (Func<dynamic, …>) are used instead of open type (Func<T, …>) in previous part. So S, K and I do not have to be in the form of C# methods.

Lambda Calculus via C# (20) Combinators
[LINQ via C#]  [Lambda Calculus]
As mentioned in a fundamental part, combinator is a special kind of lambda expression without free variables. So combinatory logic (introduced by Moses Schönfinkel and Haskell Curry) can be viewed as a variant of lambda calculus.

Lambda Calculus via C# (19) Church Encoding, And More
[LINQ via C#]  [Lambda Calculus]
So far a ton has been encoded. Here is a summary.
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)

Lambda Calculus via C# (18) Encoding Signed Number
[LINQ via C#]  [Lambda Calculus]
In lambda calculus, a signed number (integer) can be represented by a Church pair (2tuple) of Church numerals (natural numbers):
 the first Church number represents the positive part
 the second Church number represents the negative part
Signed := Tuple
So a signed number (n_{positive}, n_{egative}) ≡ Subtract n_{positive} n_{negative}.

Lambda Calculus via C# (17) Encoding Church List with Fold (Aggregate) Function
[LINQ via C#]  [Lambda Calculus]
A third way to encode Church list, is to use fold function (also called aggregate in C#/.NET):
CreateListNode3 = λv.λn.λf.λx.f v (n f x) Null3 = λf.λx.x IsNull3 = λl.l (λv.λx.False) True Value3 = λl.λx.l (λv.λy.v) x Next3 = λl.Item2 (l (λv.λt.Shift (CreateListNode3 v)) (CreateTuple Null3 Null3)) Index3 = λl.λi.i Next3 l

Lambda Calculus via C# (16) Encoding Church List with 2 Church Pairs as a Node
[LINQ via C#]  [Lambda Calculus]
Previous part encoded Church list with one Church pair (2tuple) as a list node. An alternative way is to use 2 tuples as a node, one wrapping the other.
 Outer tuple’s Item1 will be the null flag (a Church Boolean value to indicate this node is null or not)
 Outer tuple’s Item2 is the inner tuple:
 Inner tuple’s Item1 is the value of this node
 Inner tuple’s Item2 is the next node

Lambda Calculus via C# (15) Encoding Church List with Church Pair, And Null
[LINQ via C#]  [Lambda Calculus]
This part will demonstrate how to use lambda expressions to encode another data structure  list (Church list in lambda calculus or LinkedList<T> in .NET).
It is straightforward to represent a Church list node (or LinkedListNode<T> in .NET) with Church pair (2tuple)
 tuple’s Item1 will be the value of current node
 tuple’s Item2 will be the next node, which is also another tuple of course.

Lambda Calculus via C# (14) Church Pair (2Tuple) and Church Numeral Decrease
[LINQ via C#]  [Lambda Calculus]
In the Church numeral arithmetic part, the Decrease was defined as:
Decrease := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
This is complex. Now with Church pair (called tuple here to align to C# terms), Decrease can be defined in a easier way.

Lambda Calculus via C# (13) Encoding Church Pairs (2Tuples) and Generic Church Booleans
[LINQ via C#]  [Lambda Calculus]
Church pair is the Church encoding of the pair type, aka 2tuple. Unlike the Tuple<T1, T2> class in .NET, in lambda calculus Church pair will be represented by lambda expression. To avoid 2 naming systems, here in all the code, Church pair will be called tuple.

Lambda Calculus via C# (12) Church Numeral Comparison Operators
[LINQ via C#]  [Lambda Calculus]
Church Numeral Comparison Operators
With the predicates defined in previous part, operators can be defined in _Numeral class. Once again, class does not exist in lambda calculus, but C# class provides a place to define operators, which greatly improve the readability.

Lambda Calculus via C# (11) Predicates, And Divide
[LINQ via C#]  [Lambda Calculus]
A predicate is a function that returns a Boolean value. In Church encoding of lambda calculus, a predicate is a lambda expression that returns a Church Boolean.
Predicates
The is the most fundamental predicate:
IsZero := λn.n (λx.False) True
When it is applied, it will do (λx.False) n times based on True:
 When n is 0, it will “apply (λx.False)” 0 time and just returns True
 When n is not 0, it will “apply (λx.False)” 1 or more times, so returns False

Lambda Calculus via C# (10) Church Numeral Arithmetic Operators
[LINQ via C#]  [Lambda Calculus]
Operators
Another benefits of introducing (cheating with) _Numeral class into lambda calculus is  it provides a place to define custom operators.

Lambda Calculus via C# (9) Wrapping Church Numerals And Arithmetic
[LINQ via C#]  [Lambda Calculus]
In previous part, the Decrease function was a Func<Numeral<Func<Func<T, T>, T>>, Numeral<T>>:
// Decrease = n => f => x => n(g => h => h(g(f)))(_ => x)(_ => _) public static Numeral<T> Decrease<T>(this Numeral<Func<Func<T, T>, T>> numeral) { … }
This is ok because in the definition of Numeral<T>:
public delegate Func<T, T> Numeral<T>(Func<T, T> f);
T can be anything. But on another hand Decrease is expected to be more useful if its parameter and return value are exactly the same type. This can be done if in the definition of Numeral<T>, the type parameter can be hidden, so that Decrease can be something like a Func<Numeral, Numeral>.

Lambda Calculus via C# (8) Church Numeral Arithmetic
[LINQ via C#]  [Lambda Calculus]
The previous part defined Church numerals in lambda calculus and implemented 0, 1, 2, 3 in 2 different ways. By observing the definition and code, there are some patterns when the Church numeral increases from 0 to 3.

Lambda Calculus via C# (7) Encoding Church Numerals
[LINQ via C#]  [Lambda Calculus]
Previous parts showed that Boolean values, Boolean logic, and if logic can all be encoded by lambda expressions. This and next few articles will focus on natural numbers. Signed number will be encoded after introducing Church pairs (2tuples).

Lambda Calculus via C# (6) If Logic, And Reduction Strategies
[LINQ via C#]  [Lambda Calculus]
The if logic is already built in Church Booleans.
The first If
So naturedly, This is the direct implementation of if:
public static partial class ChurchBoolean { // If = condition => then => @else => @condition(then, @else) public static Func<T, Func<T, T>> If<T>(Boolean condition) { return then => @else => (T)condition (then) (@else); } }
Straightforward:
 When condition is True, if returns then
 When condition is False, If returns @else.

Lambda Calculus via C# (5) Boolean Logic
[LINQ via C#]  [Lambda Calculus]
After defining Boolean values True and False with functions, now the Boolean logics can be encoded, by functions too.
And
And can be defined by the following lambda:
And := λab.a b False
This is easy to understand. It is a function take 2 parameters a and b and return a result:
 When a is True, (True b False) returns True’s first argument b. This is correct, since in Boolean logic (And True b) ≡ b
 When a is False, (False b False) returns False’s second argument False, This is also correct, since in Boolean logic, (And False b) ≡ False