Lambda Calculus via C# (21) SKI Combinator Calculus

1
public static partial class SkiCombinators
2
{
3
    public static Func<dynamic, Func<dynamic, Func<dynamic, dynamic>>>
4
        S = x => y => z => x(z)(y(z));
5

6
    public static Func<dynamic, Func<dynamic, dynamic>>
7
        K = x => _ => x;
8

9
    public static Func<dynamic, dynamic>
10
        I = x => x;
11
}

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.

I Combinator#

Actually I can be defined with S and K:

1
S K K x
2
≡ K x (K x)
3
≡ x
4

5
  S K S x
6
≡ K x (S x)
7
≡ x

So I is merely syntactic sugar:

1
I2 := S K K
2
I3 := S K S

And C#:

1
public static partial class SkiCombinators
2
{
3
    public static Func<dynamic, dynamic>
4
        I2 = S(K)(K);
5

6
    public static Func<dynamic, dynamic>
7
        I3 = S(K)(S);
8
}

BCKW combinators#

BCKW and SKI can define each other:

1
B := S (K S) K
2
C := S (S (K (S (K S) K)) S) (K K)
3
K := K
4
W := S S (S K)
5

6
S := B (B (B W) C) (B B) ≡ B (B W) (B B C)
7
K := K
8
I := W K

ω combinator#

In SKI, the self application combinator ω is:

1
ω := S I I

This is easy to understand:

1
S I I x
2
≡ I x (I x)
3
≡ x x

Then

1
Ω := S I I (S I I)
2
   ≡ I (S I I) (I (S I I))
3
   ≡ (S I I) (S I I)
4
   ≡ S I I (S I I)
5
   ...

C#:

1
public static partial class SkiCombinators
2
{
3
    public static Func<dynamic, dynamic>
4
        ω = S(I)(I);
5

6
    public static Func<dynamic, dynamic>
7
        Ω = _ => ω(ω); // Ω = ω(ω) throws exception.
8
}

Function composition#

Remember function composition:

1
(f2 ∘ f1) x := f2 (f1 x)

In SKI:

1
S (K S) K f1 f2 x
2
≡ (K S) f1 (K f1) f2 x
3
≡ S (K f1) f2 x
4
≡ (K f1) x (f2 x)
5
≡ f1 (f2 x)

So:

1
Compose := S (K S) K

In C#:

1
public static partial class SkiCombinators
2
{
3
    public static Func<dynamic, dynamic>
4
        Compose = S(K(S))(K);
5
}

Booleans#

From previous part:

1
True := K
2
False := S K

So:

1
public static partial class SkiCombinators
2
{
3
    public static Boolean
4
        True = new Boolean(K);
5

6
    public static Boolean
7
        False = new Boolean(S(K));
8
}

Numerals#

Remember:

1
0 := λf.λx.x
2
1 := λf.λx.f x
3
2 := λf.λx.f (f x)
4
3 := λf.λx.f (f (f x))
5
...

In SKI:

1
K I f x
2
≡ I x
3
≡ x
4

5
  I f x
6
≡ f x
7

8
  S Compose I f x
9
≡ Compose f (I f) x
10
≡ Compose f f x
11
≡ f (f x)
12

13
  S Compose (S Compose I) f x
14
≡ Compose f (S Compose I f) x
15
≡ Compose f (Compose f f) x
16
≡ f (f (f x))
17

18
...

So:

1
0 := K I                     ≡ K I
2
1 := I                       ≡ I
3
2 := S Compose I             ≡ S (S (K S) K) I
4
3 := S Compose (S Compose I) ≡ S (S (K S) K) (S (S (K S) K) I)
5
...

In C#:

1
public static partial class SkiCombinators
2
{
3
    public static Func<dynamic, dynamic>
4
        Zero = K(I);
5

6
    public static Func<dynamic, dynamic>
7
        One = I;
8

9
    public static Func<dynamic, dynamic>
10
        Two = S(Compose)(I);
11

12
    public static Func<dynamic, dynamic>
13
        Three = S(Compose)(S(Compose)(I));
14
}

And generally:

1
Increase := S Compose ≡ S (S (K S) K)

C#:

1
public static partial class SkiCombinators
2
{
3
    public static Func<dynamic, Func<dynamic, dynamic>>
4
        Increase = S(Compose);
5
}

The encoding can keep going, but this post stops here. Actually, S and K can be composed to combinators that are extensionally equal to any lambda term. The proof can be found here - Completeness of the S-K basis.

Unit tests#

1
[TestClass]
2
public class SkiCombinatorsTests
3
{
4
    [TestMethod]
5
    public void SkiTests()
6
    {
7
        Func<int, Func<int, int>> x1 = a => b => a + b;
8
        Func<int, int> y1 = a => a + 1;
9
        int z1 = 1;
10
        Assert.AreEqual(x1(z1)(y1(z1)), (int)SkiCombinators.S(x1)(y1)(z1));
11
        Assert.AreEqual(x1, (Func<int, Func<int, int>>)SkiCombinators.K(x1)(y1));
12
        Assert.AreEqual(x1, (Func<int, Func<int, int>>)SkiCombinators.I(x1));
13
        Assert.AreEqual(y1, (Func<int, int>)SkiCombinators.I(y1));
14
        Assert.AreEqual(z1, (int)SkiCombinators.I(z1));
15

16
        string x2 = "a";
17
        int y2 = 1;
18
        Assert.AreEqual(x2, (string)SkiCombinators.K(x2)(y2));
19
        Assert.AreEqual(x2, (string)SkiCombinators.I(x2));
20
        Assert.AreEqual(y2, (int)SkiCombinators.I(y2));
21
    }
22

23
    [TestMethod]
24
    public void BooleanTests()
25
    {
26
        Assert.AreEqual(true, (bool)SkiCombinators.True(true)(false));
27
        Assert.AreEqual(false, (bool)SkiCombinators.False(new Func<dynamic, dynamic>(_ => true))(false));
28
    }
29

30
    [TestMethod]
31
    public void NumeralTests()
32
    {
33
        Assert.AreEqual(0U, SkiCombinators._UnchurchNumeral(SkiCombinators.Zero));
34
        Assert.AreEqual(1U, SkiCombinators._UnchurchNumeral(SkiCombinators.One));
35
        Assert.AreEqual(2U, SkiCombinators._UnchurchNumeral(SkiCombinators.Two));
36
        Assert.AreEqual(3U, SkiCombinators._UnchurchNumeral(SkiCombinators.Three));
37
        Assert.AreEqual(4U, SkiCombinators._UnchurchNumeral(SkiCombinators.Increase(SkiCombinators.Three)));
38
    }
39
}