Lambda Calculus via C# (20) Combinators

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.

I combinator#

The following simplest lambda expression:

1
I := λx.x

is an example of combinator. In combinatory logic, λx.x is called I (Id), because it just returns the parameter itself.

BCKW combinators#

Also:

1
B := λx.λy.λz.x (y z)
2
C := λx.λy.λz.x z y
3
K := λx.λy.   x
4
W := λx.λy.   x y y

where:

B composes x and y
C swaps y and z
K discards y
W duplicates y

Only bound variables appear in the body of the lambda expressions. So apparently these are combinators.

C# version:

1
public static class BckwCombinators
2
{
3
    // B = x => => z => x(y(z))
4
    public static Func<Func<T1, T2>, Func<T1, TResult>> B<T1, T2, TResult>
5
        (Func<T2, TResult> x) => y => z => x(y(z));
6

7
    // C = f => x => y => f(y)(z)
8
    public static Func<T2, Func<T1, TResult>> C<T1, T2, TResult>
9
        (Func<T1, Func<T2, TResult>> x) => y => z => x(z)(y);
10

11
    // K = x => _ => x
12
    public static Func<T2, T1> K<T1, T2>
13
        (T1 x) => _ => x;
14

15
    // W = x => y => x(y)(y)
16
    public static Func<T, TResult> W<T, TResult>
17
        (Func<T, Func<T, TResult>> x) => y => x(y)(y);
18
}

The BCKW system is a variant of combinatory logic that takes the BCKW combinators as primitives.

ω combinator#

ω is the self application combinator:

1
ω := λx.x x

And Ω is to apply ω to itself:

1
Ω := ω ω

The interesting property of Ω is - it’s irreducible:

1
ω ω
2
≡ (λx.x x) (λx.x x)
3
≡ (λx.x x) (λx.x x)
4
...

C#:

1
public delegate T ω<T>(ω<T> ω);
2

3
public static class OmegaCombinators
4
{
5
    // ω = x => x(x)
6
    public static T ω<T>
7
        (ω<T> x) => x(x);
8

9
    // Ω = ω(ω)
10
    public static T Ω<T>
11
        () => ω<T>(ω); // Ω<T> = ω<T>(ω) throws exception.
12
}

Apparently, applying Ω will throw an exception:

System.StackOverflowException was unhandled.

SKI combinators#

The more interested combinators are:

1
S := λx.λy.λz.x z (y z)
2
K := λx.λy.   x
3
I := λx.      x

where:

S (Slider) slides z to between x and y (In most materials S is called Substitution, but in Dana Scott’s presentation he called it Slider)
K (Killer) discards y (The same K in BCKW)
I (Id) returns x

Naturally, this is the C#, strongly typed:

1
public static partial class SkiCombinators
2
{
3
    // S = x => y => z = x(z)(y(z))
4
    public static Func<Func<T1, T2>, Func<T1, TResult>> S<T1, T2, TResult>
5
        (Func<T1, Func<T2, TResult>> x) => y => z => x(z)(y(z));
6

7
    // K = x => _ => x
8
    public static Func<T2, T1> K<T1, T2>
9
        (T1 x) => _ => x;
10

11
    // I = x => x
12
    public static T I<T>
13
        (T x) => x;
14
}

Just like above BCKW system, the SKI combinator calculus takes the SKI combinators as primitives. It can be viewed as a reduced version of untyped lambda calculus, and an extremely simple Turing complete language.

Boolean in SKI, and type issue#

The same as lambda calculus, Boolean would be the simplest thing to try first. Remember in lambda calculus:

1
True := λt.λf.t
2
False := λt.λf.f

Here with SKI:

1
K t f
2
≡ t
3

4
  S K t f
5
≡ K f (t f)
6
≡ f

So in SKI calculus, True and False can be defined as:

1
True := K
2
False := S K

If above C# SKI is used to implement True and False:

1
// True = K
2
public static Func<object, object> True
3
    (object @true) => K<object, object>(@true);
4

5
// Cannot be compiled.
6
// False = S(K)
7
public static Func<object, object> False
8
    (object /* Func<object, object> */ @true) => @false =>
9
        S<object, object, object>(K<object, object>)(/* Func<object, object> */ @true)(@false);

False does not compile. Because in the strongly typed implementation, @true is expected to be a Func<object, object>, so that it can be applied to S as S’s second argument.

Again, as fore mentioned, SKI calculus is untyped. To “make” the above code compile, something is needed to have C# compiler forget @true’s type:

1
// False = S(K)
2
public static Func<object, object> False
3
    (dynamic @true) => @false => S<object, object, object>(K<object, object>)(@true)(@false);