[LINQ via C# series]

[Lambda Calculus via C# series]

Latest version: https://weblogs.asp.net/dixin/lambda-calculus-via-csharp-6-combinatory-logic

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:

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:

B := λx.λy.λz.x (y z)
C := λx.λy.λz.x z y
K := λx.λy.   x
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:

public static class BckwCombinators
{
    // B = x => => z => x(y(z))
    public static Func<Func<T1, T2>, Func<T1, TResult>> B<T1, T2, TResult>
        (Func<T2, TResult> x) => y => z => x(y(z));

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

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

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

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

ω combinator

ω is the self application combinator:

ω := λx.x x

And Ω is to apply ω to itself:

Ω := ω ω

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

  ω ω
≡ (λx.x x) (λx.x x)
≡ (λx.x x) (λx.x x)
...

C#:

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

public static class OmegaCombinators
{
    // ω = x => x(x)
    public static T ω<T>
        (ω<T> x) => x(x);

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

Apparently, applying Ω will throw an exception:

System.StackOverflowException was unhandled.

SKI combinators

The more interested combinators are:

S := λx.λy.λz.x z (y z)
K := λx.λy.   x
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:

public static partial class SkiCombinators
{
    // S = x => y => z = x(z)(y(z))
    public static Func<Func<T1, T2>, Func<T1, TResult>> S<T1, T2, TResult>
        (Func<T1, Func<T2, TResult>> x) => y => z => x(z)(y(z));

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

    // I = x => x
    public static T I<T>
        (T x) => x;
}

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:

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

Here with SKI:

  K t f
≡ t

  S K t f
≡ K f (t f) 
≡ f

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

True := K
False := S K

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

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

// Cannot be compiled.
// False = S(K)
public static Func<object, object> False
    (object /* Func<object, object> */ @true) => @false => 
        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:

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

So, dynamic is the (untyped) way to go.