# ¶Reduction semantics for CC

Starting with the natural basis:

```[B] [A] cat  ≜ [B A]
[A] drop ≜
[A] dup  ≜ [A] [A]
[A] i    ≜ A
[B] [A] swap ≜ [A] [B]
[A] unit ≜ [[A]]
```

The natural normal concatenative basis

Some examples using reduction instead of stacks:

```[B] [A] cons ≜ [B] [A] [unit] swap unit cat i cat
^^^^^^^^^^^^^^^
= [B] [unit] [A] unit cat i cat
^^^^^^^^
= [B] [unit] [[A]] cat i cat
^^^^^^^^^^^^^^^^
= [B] [unit [A]] i cat
^^^^^^^^^^^^
= [B] unit [A] cat
^^^^^^^^
= [[B]] [A] cat
^^^^^^^^^^^^^
= [[B] A]
```
```[B] [A] cons ≜ [B] [A] swap unit swap cat
^^^^^^^^^^^^
= [A] [B] unit swap cat
^^^^^^^^
= [A] [[B]] swap cat
^^^^^^^^^^^^^^
= [[B]] [A] cat
^^^^^^^^^^^^^
= [[B] A]
```
```[B] [A] k ≜ [B] [A] swap drop i
^^^^^^^^^^^^
= [A] [B] drop i
^^^^^^^^
= [A] i
^^^^^
= A
```
```false ≜ [drop]
true  ≜ [swap drop]
or    ≜ dup i

false true or ≜ [drop] [swap drop] dup i
^^^^^^^^^^^^^^^
= [drop] [swap drop] [swap drop] i
^^^^^^^^^^^^^
= [drop] [swap drop] swap drop
^^^^^^^^^^^^^^^^^^^^^^^
= [swap drop] [drop] drop
^^^^^^^^^^^
= [swap drop]
= true

false false or ≜ [drop] [drop] dup i
^^^^^^^^^^
= [drop] [drop] [drop] i
^^^^^^^^
= [drop] [drop] drop
^^^^^^^^^^^
= [drop]
= false
```

All of these have a single sequence of reductions that is possible, because they do not require reducing anything nested in a quotation. Here's an example from Kerby that does have multiple reduction paths:

```[B] [A] cat ≜ [B] [A] [[i] dip i] cons cons
^^^^^^^^^^^^^^^^^^^^
= [B] [[A] [i] dip i] cons
^^^^^^^^^^^^^^^^^^^^^^^^
= [[B] [A] [i] dip i]
^^^^^^^^^^^
= [[B] i [A] i]
^^^^^
= [B [A] i]
^^^^^
= [B A]
```

## ¶Church numerals

Aiming for

```[B] [A] ℕ₀ == B
[B] [A] ℕ₁ == [B] A
[B] [A] ℕ₂ == [[B] A] A
[B] [A] ℕ₃ == [[[B] A] A] A
…
```

Definitions

```[B] [A] ℕ₀ ≜ [B] [A] drop i
^^^^^^^^
= [B] i
^^^^^
= B
```
```[B] [A] ℕ₁ ≜ [B] [A] i
^^^^^
= [B] A
```
```[ℕ] succ ≜ [ℕ] [ℕ₁] +
= [ℕ] [i] [cons b] cons s
^^^^^^^^^^^^^^^^^
= [ℕ] [[i] cons b] s
```
```[B] [A] ℕ₂ ≜ [B] [A] [ℕ₁] succ
= [B] [A] [i] [[i] cons b] s
^^^^^^^^^^^^^^^^^^^^^^
= [B] [[A] i] [A] [i] cons b
^^^^^^^^^^^^
= [B] [[A] i] [[A] i] b
^^^^^^^^^^^^^^^^^^^^^
= [[B] [A] i] [A] i
^^^^^
= [[B] [A] i] A
^^^^^
= [[B] A] A
```