[LINQ via C# series]

[Lambda Calculus via C# series]

Latest version: https://weblogs.asp.net/dixin/lambda-calculus-via-csharp-5-list

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

CreateTuple := λx.λy.λf.f x y
Tuple := λf.f x y
Item1 := λt.t (λx.λy.x)
Item2 := λt.t (λx.λy.y)

Directly for Church list node:

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

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

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

public static class ChurchList
{
    // Create = value => next => ChurchTuple.Create(value)(next)
    public static Func<ListNode<T>, ListNode<T>> Create<T>
        (T value) => next => new ListNode<T>(ChurchTuple.Create<T, ListNode<T>>(value)(next));

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

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

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:

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

When IsNull is applied with a null node:

  IsNull Null
≡ (λl.l (λv.λn.λx.False) True) (λf.λx.x)
≡ (λf.λx.x) (λv.λn.λx.False) True
≡ (λx.x) True
≡ True

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

  IsNull (CreateListNode 0 Null)
≡ IsNull (λf.f 0 Null)
≡ (λl.l (λv.λn.λx.False) True) (λf.f 0 Null)
≡ (λf.f 0 Null) (λv.λn.λx.False) True
≡ (λv.λn.λx.False) 0 Null True
≡ (λn.λx.False) Null True
≡ (λx.False) True
≡ False

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

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

and IsNull:

// IsNull = node(value => next => _ => ChurchBoolean.False)(ChurchBoolean.True)
public static Boolean IsNull<T>
    (this ListNode<T> node) =>
        ((Func<Boolean, Boolean>)node(value => next =>
            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:

Null := False

C# will be:

// Null = ChurchBoolean.False;
public static ListNode<T> GetNull<T>
    () => 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:

// IsNull = node => node(value => next => _ => ChurchBoolean.False)(ChurchBoolean.True)
public static Boolean IsNull<T>
    (this ListNode<T> node) => 
        (Boolean)((Func<Boolean, object>)node(value => next => 
            new Func<Boolean, object>(_ => 
                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:

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

Refactored C#:

// Next = node => If(node.IsNull())(_ => Null)(_ => node.Item2())
public static ListNode<T> Next<T>
    (this ListNode<T> node) =>
        ChurchBoolean.If<ListNode<T>>(node.IsNull())
            (_ => node)
            (_ => 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:

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

// Index = start => index => index(Next)(start)
public static ListNode<T> Index<T>
    (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:

[TestClass()]
public class ChurchListTests
{
    [TestMethod()]
    public void CreateValueNextTest()
    {
        ListNode<int> node1 = ChurchList.Create(1)(ChurchList.Null);
        ListNode<int> node2 = ChurchList.Create(2)(node1);
        ListNode<int> node3 = ChurchList.Create(3)(node2);
        Assert.AreEqual(1, node1.Value());
        Assert.AreEqual(ChurchList.Null, node1.Next());
        Assert.AreEqual(2, node2.Value());
        Assert.AreEqual(node1, node2.Next());
        Assert.AreEqual(3, node3.Value());
        Assert.AreEqual(node2, node3.Next());
        Assert.IsTrue(ChurchList.GetNull<object>().Next().IsNull()._Unchurch());
    }

    [TestMethod()]
    public void NullIsNullTest()
    {
        ListNode<int> node = ChurchList.Create(1)(ChurchList.Null);
        Assert.IsTrue(ChurchList.IsNull<object>(ChurchList.Null)._Unchurch());
        Assert.IsTrue(ChurchList.GetNull<object>().IsNull()._Unchurch());
        Assert.IsTrue(new ListNode<object>(ChurchBoolean.False<Boolean<object, ListNode<object>>, Boolean>).IsNull()._Unchurch());
        Assert.IsFalse(node.IsNull()._Unchurch());
    }

    [TestMethod()]
    public void IndexTest()
    {
        ListNode<int> node1 = ChurchList.Create(1)(ChurchList.Null);
        ListNode<int> node2 = ChurchList.Create(2)(node1);
        ListNode<int> node3 = ChurchList.Create(3)(node2);
        Assert.AreEqual(node3, node3.Index(0U._Church()));
        Assert.AreEqual(node2, node3.Index(1U._Church()));
        Assert.AreEqual(node1, node3.Index(2U._Church()));
        Assert.IsTrue(node3.Index(3U._Church()).IsNull()._Unchurch());
        Assert.IsTrue(node3.Index(4U._Church()).IsNull()._Unchurch());
        Assert.IsTrue(node3.Index(5U._Church()).IsNull()._Unchurch());
    }
}