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

770 words

4 minutes

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

2018-11-15

C#

.NET

/

.NET Core

/

.NET Standard

/

C#

/

LINQ

TIP
Functional Programming and LINQ via C# Series
Lambda Calculus via C# Series
This post is updated, here is the latest version.

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 (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<T>’s Next property can be null to indicate the current node is the last element (Last) of the LinkedList<T>. 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
}