Lambda Calculus via C# (15) Encoding Church List with Church Pair, And Null

This part will demonstrate how to use lambda expressions to encode another data structure - list (Church list in lambda calculus or LinkedList in .NET).

It is straightforward to represent a Church list node (or LinkedListNode in .NET) with Church pair (2-tuple)

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.

Church pair as a Church list node#

Remember Church pair (called tuple here in order to align with .NET):

1
CreateTuple := λx.λy.λf.f x y
2
Tuple := λf.f x y
3
Item1 := λt.t (λx.λy.x)
4
Item2 := λt.t (λx.λy.y)

Directly for Church list node:

1
CreateListNode := CreateTuple ≡ λv.λn.λf.f v n
2
ListNode := Tuple ≡ λf.f v n
3
Value := Item1 ≡ λl.l (λv.λn.v)
4
Next := Item2 ≡ λl.l (λv.λn.n)

The C# code will be direct applications of the tuple’s functions:

1
// ListNode<T> is alias of Tuple<T, ListNode<T>>
2
public delegate object ListNode<out T>(Boolean<T, ListNode<T>> f);
3

4
public static class ChurchList
5
{
6
    // Create = value => next => ChurchTuple.Create(value)(next)
7
    public static Func<ListNode<T>, ListNode<T>> Create<T>
8
        (T value) => next => new ListNode<T>(ChurchTuple.Create<T, ListNode<T>>(value)(next));
9

10
    // Value = node => node.Item1()
11
    public static T Value<T>
12
        (this ListNode<T> node) => new Tuple<T, ListNode<T>>(node).Item1();
13

14
    // Next = node => node.Item2()
15
    public static ListNode<T> Next<T>
16
        (this ListNode<T> node) => new Tuple<T, ListNode<T>>(node).Item2();
17
}

Encoding Null, and IsNull predicate#

If a list has a end node, what’s its Next node, or as a tuple what’s its Item2? In C#/.NET, a LinkedListNode’s Next property can be null to indicate the current node is the last element (Last) of the LinkedList. In lambda calculus, Null and IsNull predicate for list node can be defined as:

1
Null := λf.λx.x
2
IsNull := λl.l (λv.λn.λx.False) True

When IsNull is applied with a null node:

1
IsNull Null
2
≡ (λl.l (λv.λn.λx.False) True) (λf.λx.x)
3
≡ (λf.λx.x) (λv.λn.λx.False) True
4
≡ (λx.x) True
5
≡ True

And when IsNull is applied with a non-null node:

1
IsNull (CreateListNode 0 Null)
2
≡ IsNull (λf.f 0 Null)
3
≡ (λl.l (λv.λn.λx.False) True) (λf.f 0 Null)
4
≡ (λf.f 0 Null) (λv.λn.λx.False) True
5
≡ (λv.λn.λx.False) 0 Null True
6
≡ (λn.λx.False) Null True
7
≡ (λx.False) True
8
≡ False

The C# implementation is noisy because a lot of type information has to be provided. This is Null:

1
// Null = f => _ => _;
2
public static object Null<T>
3
    (Boolean<T, ListNode<T>> f) => new Func<Boolean, Boolean>(_ => _);

and IsNull:

1
// IsNull = node(value => next => _ => ChurchBoolean.False)(ChurchBoolean.True)
2
public static Boolean IsNull<T>
3
    (this ListNode<T> node) =>
4
        ((Func<Boolean, Boolean>)node(value => next =>
5
            new Func<Boolean, Boolean>(_ => ChurchBoolean.False)))(ChurchBoolean.True);

Church Boolean as Null#

Actually, the definition of Null (λf.λx.x) is exactly the same as False (λf.λx.x) according to alpha-conversion, so it can be redefined as:

1
Null := False

C# will be:

1
// Null = ChurchBoolean.False;
2
public static ListNode<T> GetNull<T>
3
    () => ChurchBoolean.False<Boolean<T, ListNode<T>>, Boolean>;

Here a function GetNull has to be created, because C# does not support generic property.

And IsNull needs to be refactored too:

1
// IsNull = node => node(value => next => _ => ChurchBoolean.False)(ChurchBoolean.True)
2
public static Boolean IsNull<T>
3
    (this ListNode<T> node) =>
4
        (Boolean)((Func<Boolean, object>)node(value => next =>
5
            new Func<Boolean, object>(_ =>
6
                new Boolean(ChurchBoolean.False))))(ChurchBoolean.True);

Here object in the code does not mean that System.Object is introduced to implement IsNull. It is just used to satisfy c# compiler. So with the help of Church pair and Church Boolean, the Church list has been encoded with functions in lambda calculus, as well as null and IsNull predicate.

The improved Next#

Since Null is introduced, Next need to be redefined, so that a Null node’s next node will still be itself:

1
ListNodeNext := λl.If (IsNull l) (λx.l) (λx.(Item2 l))

Refactored C#:

1
// Next = node => If(node.IsNull())(_ => Null)(_ => node.Item2())
2
public static ListNode<T> Next<T>
3
    (this ListNode<T> node) =>
4
        ChurchBoolean.If<ListNode<T>>(node.IsNull())
5
            (_ => node)
6
            (_ => new Tuple<T, ListNode<T>>(node).Item2());

This is the same way as Church numerals, Decrease 0 is still 0.

Index#

With the improved Next, the Index function can be defined as:

1
Index = λl.λi.i Next l

To get the node of index I, just means to do “Next” I times, starting with the specified node.

C#:

1
// Index = start => index => index(Next)(start)
2
public static ListNode<T> Index<T>
3
    (this ListNode<T> start, _Numeral index) => index.Numeral<ListNode<T>>()(Next)(start);

Unit tests#

The following unit tests also shows how to use Church list:

1
[TestClass()]
2
public class ChurchListTests
3
{
4
    [TestMethod()]
5
    public void CreateValueNextTest()
6
    {
7
        ListNode<int> node1 = ChurchList.Create(1)(ChurchList.Null);
8
        ListNode<int> node2 = ChurchList.Create(2)(node1);
9
        ListNode<int> node3 = ChurchList.Create(3)(node2);
10
        Assert.AreEqual(1, node1.Value());
11
        Assert.AreEqual(ChurchList.Null, node1.Next());
12
        Assert.AreEqual(2, node2.Value());
13
        Assert.AreEqual(node1, node2.Next());
14
        Assert.AreEqual(3, node3.Value());
15
        Assert.AreEqual(node2, node3.Next());
16
        Assert.IsTrue(ChurchList.GetNull<object>().Next().IsNull()._Unchurch());
17
    }
18

19
    [TestMethod()]
20
    public void NullIsNullTest()
21
    {
22
        ListNode<int> node = ChurchList.Create(1)(ChurchList.Null);
23
        Assert.IsTrue(ChurchList.IsNull<object>(ChurchList.Null)._Unchurch());
24
        Assert.IsTrue(ChurchList.GetNull<object>().IsNull()._Unchurch());
25
        Assert.IsTrue(new ListNode<object>(ChurchBoolean.False<Boolean<object, ListNode<object>>, Boolean>).IsNull()._Unchurch());
26
        Assert.IsFalse(node.IsNull()._Unchurch());
27
    }
28

29
    [TestMethod()]
30
    public void IndexTest()
31
    {
32
        ListNode<int> node1 = ChurchList.Create(1)(ChurchList.Null);
33
        ListNode<int> node2 = ChurchList.Create(2)(node1);
34
        ListNode<int> node3 = ChurchList.Create(3)(node2);
35
        Assert.AreEqual(node3, node3.Index(0U._Church()));
36
        Assert.AreEqual(node2, node3.Index(1U._Church()));
37
        Assert.AreEqual(node1, node3.Index(2U._Church()));
38
        Assert.IsTrue(node3.Index(3U._Church()).IsNull()._Unchurch());
39
        Assert.IsTrue(node3.Index(4U._Church()).IsNull()._Unchurch());
40
        Assert.IsTrue(node3.Index(5U._Church()).IsNull()._Unchurch());
41
    }
42
}