# Lambda Calculus via C# (21) SKI Combinator Calculus

The previous part shows SKI calculus is untyped and strongly typed C# implementation does not work. So here comes the SKI in untyped C#:

```public static partial class SkiCombinators
{
public static Func<dynamic, Func<dynamic, Func<dynamic, dynamic>>>
S = x => y => z => x(z)(y(z));

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

public static Func<dynamic, dynamic>
I = x => x;
}```

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:

```  S K K x
≡ K x (K x)
≡ x

S K S x
≡ K x (S x)
≡ x```

So I is merely syntactic sugar:

```I2 := S K K
I3 := S K S```

And C#:

```public static partial class SkiCombinators
{
public static Func<dynamic, dynamic>
I2 = S(K)(K);

public static Func<dynamic, dynamic>
I3 = S(K)(S);
}```

# BCKW combinators

BCKW and SKI can define each other:

```B := S (K S) K
C := S (S (K (S (K S) K)) S) (K K)
K := K
W := S S (S K)

S := B (B (B W) C) (B B) ≡ B (B W) (B B C)
K := K
I := W K```

# ω combinator

In SKI, the self application combinator ω is:

`ω := S I I`

This is easy to understand:

```  S I I x
≡ I x (I x)
≡ x x```

Then

```Ω := S I I (S I I)
≡ I (S I I) (I (S I I))
≡ (S I I) (S I I)
≡ S I I (S I I)
...```

C#:

```public static partial class SkiCombinators
{
public static Func<dynamic, dynamic>
ω = S(I)(I);

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

A lot more combinators can be found here, as well as their SKI implementation.

# Function composition

Remember function composition:

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

In SKI:

```  S (K S) K f1 f2 x
≡ (K S) f1 (K f1) f2 x
≡ S (K f1) f2 x
≡ (K f1) x (f2 x)
≡ f1 (f2 x)```

So:

`Compose := S (K S) K`

In C#:

```public static partial class SkiCombinators
{
public static Func<dynamic, dynamic>
Compose = S(K(S))(K);
}```

# Booleans

From previous part:

```True := K
False := S K```

So:

```public static partial class SkiCombinators
{
public static Boolean
True = new Boolean(K);

public static Boolean
False = new Boolean(S(K));
}```

# Numerals

Remember:

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

In SKI:

```  K I f x
≡ I x
≡ x

I f x
≡ f x

S Compose I f x
≡ Compose f (I f) x
≡ Compose f f x
≡ f (f x)

S Compose (S Compose I) f x
≡ Compose f (S Compose I f) x
≡ Compose f (Compose f f) x
≡ f (f (f x))

...```

So:

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

In C#:

```public static partial class SkiCombinators
{
public static Func<dynamic, dynamic>
Zero = K(I);

public static Func<dynamic, dynamic>
One = I;

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

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

And generally:

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

C#:

```public static partial class SkiCombinators
{
public static Func<dynamic, Func<dynamic, dynamic>>
Increase = S(Compose);
}```

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

```[TestClass]
public class SkiCombinatorsTests
{
[TestMethod]
public void SkiTests()
{
Func<int, Func<int, int>> x1 = a => b => a + b;
Func<int, int> y1 = a => a + 1;
int z1 = 1;
Assert.AreEqual(x1(z1)(y1(z1)), (int)SkiCombinators.S(x1)(y1)(z1));
Assert.AreEqual(x1, (Func<int, Func<int, int>>)SkiCombinators.K(x1)(y1));
Assert.AreEqual(x1, (Func<int, Func<int, int>>)SkiCombinators.I(x1));
Assert.AreEqual(y1, (Func<int, int>)SkiCombinators.I(y1));
Assert.AreEqual(z1, (int)SkiCombinators.I(z1));

string x2 = "a";
int y2 = 1;
Assert.AreEqual(x2, (string)SkiCombinators.K(x2)(y2));
Assert.AreEqual(x2, (string)SkiCombinators.I(x2));
Assert.AreEqual(y2, (int)SkiCombinators.I(y2));
}

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

[TestMethod]
public void NumeralTests()
{
Assert.AreEqual(0U, SkiCombinators._UnchurchNumeral(SkiCombinators.Zero));
Assert.AreEqual(1U, SkiCombinators._UnchurchNumeral(SkiCombinators.One));
Assert.AreEqual(2U, SkiCombinators._UnchurchNumeral(SkiCombinators.Two));
Assert.AreEqual(3U, SkiCombinators._UnchurchNumeral(SkiCombinators.Three));
Assert.AreEqual(4U, SkiCombinators._UnchurchNumeral(SkiCombinators.Increase(SkiCombinators.Three)));
}
}```