 # [Lambda Calculus via C# series]

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
• 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.