# [Lambda Calculus via C# series]

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 ≡ fn`

So increasing n means to do something one more time:

`Increase2 := λn.λf.f ∘ fn ≡ λ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().

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.fa ∘ fb ≡ λa.λb.λf.(a f) ∘ (b f)`

So in C#:

```// Add = a => b => f => x => a(f)(b(f)(x))
(this Numeral<T> a, Numeral<T> b) => f => x => a(f)(b(f)(x));

// Add2 = a => b => f => f ^ (a + b)
(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)
(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#.