# Lambda Calculus via C# (20) Combinators

# [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);