# Lambda Calculus via C# (8) Church Numeral Arithmetic

# [LINQ via C# series]

# [Lambda Calculus via C# series]

**Latest version: https://weblogs.asp.net/dixin/lambda-calculus-via-csharp-3-numeral-arithmetic-and-predicate**

The previous part defined Church numerals in lambda calculus and implemented 0, 1, 2, 3 in 2 different ways. By observing the definition and code, there are some patterns when the Church numeral increases from 0 to 3.

# Increase

In the definitions of Church numerals:

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

The underlined parts can be substituted by the following underlined parts in the applications:

```
0 f x ≡ x
1 f x ≡ f x
2 f x ≡ f (f x)
...
```

Then Church numerals’ definition become:

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

which shows how the the Church numerals increases. Generally, for a Church numeral n, the next numeral will be λf.λx.f (n f x). So:

`Increase := λn.λf.λx.f (n f x)`

The C# implementation is:

// Increase = n => f => x => f(n(f)(x)) public static Numeral<T> Increase<T> (this Numeral<T> numeral) => f => x => f(numeral(f)(x));

In the other way, Church numeral N can be read as do something N times:

`n f ≡ f`^{n}

So increasing n means to do something one more time:

`Increase2 := λn.λf.f ∘ f`^{n} ≡ λn.λf.f ∘ (n f)

And in C#:

// Increase2 = n => f => f ^ (n + 1) public static Numeral<T> Increase2<T> (this Numeral<T> numeral) => f => f.o(numeral(f));

Just like the previous part of Church Boolean operators, here extension methods are used for convenience and readability, e.g.: n.Increase().

# Add

Again, from the definition, Church numeral a adding b means to “apply f” b times then “apply f” a times:

`Add := λa.λb.λf.λx.a f (b f x)`

Also it means to do something a times then b times:

`Add2 := λa.λb.λf.f`^{a} ∘ f^{b} ≡ λa.λb.λf.(a f) ∘ (b f)

So in C#:

// Add = a => b => f => x => a(f)(b(f)(x)) public static Numeral<T> Add<T> (this Numeral<T> a, Numeral<T> b) => f => x => a(f)(b(f)(x)); // Add2 = a => b => f => f ^ (a + b) public static Numeral<T> Add2<T> (this Numeral<T> a, Numeral<T> b) => f => a(f).o(b(f));

There is also a third way to understand a adding b - “apply Increase” a times based on b:

`Add3 := λa.λb.a Increase b`

And C#:

// Add3 = a => b => a(Increase)(b) public static Numeral<T> Add3<T> (this Numeral<Numeral<T>> a, Numeral<T> b) => a(Increase)(b);

# Decrease and subtract

Similarly, once Decrease is defined, Subtract can be defined easily:

```
Decrease := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
Subtract := λa.λb.b Decrease a
```

This definition of Decrease is complex and the explanation will be skipped. Later after defining Church pairs (2-tuples), a more intuitive version will be defined.

C# code will be:

// Decrease = n => f => x => n(g => h => h(g(f)))(_ => x)(_ => _) public static Numeral<T> Decrease<T> (this Numeral<Func<Func<T, T>, T>> numeral) => f => x => numeral(g => h => h(g(f)))(_ => x)(_ => _); // Cannot be compiled. // Subtract = a => b => b(Decrease)(a) public static Numeral<T> Subtract<T> (Numeral<T> a, Numeral<Numeral<Func<Func<T, T>, T>>> b) => b(Decrease)(a);

However, Subtract cannot be compiled. The reason is, as a Church numeral, b requires the first parameter to be Func<TSomething, TSomething>, but Decrease becomes Func<TSomething, TSomethingElse>. The next part will show how to work with this paradox in C#.