# Foundations of the gerku language

## Abstract
We outline here the theoretical foundation that inspired the development of the `gerku` language.

In [1] a method is presented to automatically derive 𝜆-functions (or, equivalently, Combinatory Logic terms) from the definition of iterative functions.

The method relies on encoding data types with 𝜆-functions (or CL terms) in a specific way so that deriving the 𝜆-function (or CL term) to compute an iterative function is completely automatic.

We will only present the general idea here, using practical examples. The original papers (see bibliography) provide a more formal description.

The last section contains a full example on how to write a program that reverses a given list.

The `gerku` project objectives are:
- to prove that the same results hold in Concatenative Combinatory Logic (see [3])
- to create an interpreter to execute programs automatically derived from their iterative definition.

## Data types

We define a *data type* 𝓓 as a pair of sets:

  𝓓 = ⟨{*carriers*}, {*constructors*}⟩

Let's define some common data types.

### Natural numbers (ℕ)

Natural numbers (ℕ) are defined by Peano's axioms:
- 0 is a natural number;
- if 𝑛 is a natural number then 𝒔(𝑛) is a natural number;
- nothing else is a natural number.

Any natural number can be represented as 𝒔(𝒔( ... 𝒔(𝒔(0)) ... )).

The *constructors* of natural numbers are the two functions 0:ℕ and 𝒔:ℕ⭢ℕ.

We can say that the data type for natural numbers is:

  𝓓 = ⟨{ℕ}, {𝒔:ℕ⭢ℕ , 0:ℕ}⟩

### Pairs (ℙ)
The carrier set of a data type contains all the elements of the data type but can also contain other elements that are not generated by the constructors but are given a priori. Let's call them *atoms*.

  𝓓 = ⟨{𝔸,ℙ}, {pair:𝔸×𝔸⭢ℙ}⟩

The `pair()` constructor is often abbreviated using angle brackets `⟨⟩`.

### Booleans (𝔹)

  𝓓 = ⟨{𝔹}, {true:𝔹 , false:𝔹}⟩

### Lists (𝕃)

Lists that can be defined by axioms similar to the ones we have used for Naturals:
- nil is a list;
- if 𝑙 is a list and 𝑎 is an atom, then cons(𝑎,𝑙) is a list;
- nothing else is a list.

Any list is represented by a term like:

  cons(𝑎₁, (cons(𝑎₂, ... cons(𝑎ₙ,nil) ... )))

The data type for the lists is:

  𝓓 = ⟨{𝔸,𝕃}, {cons:𝔸⭢𝕃⭢𝕃 , nil:𝕃}⟩

We can abbreviate a list using the following notation `[𝑎₁ 𝑎₂ ... 𝑎ₙ]`.

## Iterative functions

We will focus on the class of *iterative functions* which is closed under composition.

### Iterative functions on ℕ

A function `𝑓` on Naturals is said to be *iterative* if it can be defined as follows:

   𝑓(0) = ℎ₀
   𝑓(𝒔(n)) = ℎ₁(𝑓(n))

If this definition is possible, we'll have that:

  𝑓(n) = ℎ₁(ℎ₁( ... ℎ₁(ℎ₀) ... )) = ℎ₁ⁿ(ℎ₀)
        ╰────── n times ────────╯

for example:

  𝑓(3) = ℎ₁(𝑓(2))
       = ℎ₁(ℎ₁(𝑓(1)))
       = ℎ₁(ℎ₁(ℎ₁(𝑓(0))))
       = ℎ₁(ℎ₁(ℎ₁(ℎ₀))))

Typical examples of iterative functions are the addition and the multiplication on Naturals:

  add(m,0)    = m
  add(m,𝒔(n)) = 𝒔(add(m,n))

  mult(m,0)    = 0
  mult(m,𝒔(n)) = add(m,mult(m,n))

### Iterative functions on ℙ
The pair data type has only one constructor, meaning that the iterative scheme will only have one case.

Two fundamental functions are the *projectors* that extract the elements from a pair:

  Π₁(⟨𝑎₁,𝑎₂⟩) = 𝑎₁      Π₂(⟨𝑎₁,𝑎₂⟩) = 𝑎₂

It's easy to see that they are iterative.

### Iterative functions on 𝕃

A function 𝑓 on lists is said to be *iterative* if it can be defined as follows:

   𝑓(nil) = ℎ₀
   𝑓(cons(a,l)) = ℎ₁(a,𝑓(l))

If this definition is possible, for a list of length n we'll have that:

  𝑓(l) = ℎ₁(𝑎₁, ℎ₁(𝑎₂, ... ℎ₁(𝑎ₙ,ℎ₀) ... ))
        ╰─────────── n times ────────────╯

Some examples of iterative functions on lists:

  len(nil)       = 0
  len(cons(a,l)) = succ(len(l))

  head(nil)       = 𝜀
  head(cons(a,l)) = 𝒰₁(a,head(l))

The auxiliary function 𝒰₁() returns the first among its arguments.

## Primitive Recursive functions

Let's restrict our attention on Naturals. The reasoning below can be generalized to any data type.
A function 𝑓 on Naturals is said to be *primitive recursive* if it can be defined as follows:

   𝑓(0) = 𝑔₀
   𝑓(𝒔(n)) = 𝑔₁(n,𝑓(n))

The key difference with *iterative* functions is that the recursive step depends not only on `𝑓(n)` but also on `n` itself.

An important property (proven in [2]) is that:
> For any primitive recursive function `𝑓()` , there exists an iterative function `𝐹()` that (using tuples) produces the same result.

In other words: `∃𝐺₀,𝐺₁` such that

   𝐹(0) = 𝐺₀
   𝐹(𝒔(n)) = 𝐺₁(𝐹(n))

and `∀n∈ℕ 𝑓(n) = 𝐹(n)`

This means that working with iterative functions does not restrict us in any way.

Let's show how this works with the factorial.

   fact(0) = 1
   fact(𝒔(n)) = mult(𝒔(n),fact(n))

We can choose the following iterative functions:

  𝐺₀    = ⟨0,1⟩
  𝐺₁(y) = ⟨𝒔(Π₁(y)), mult(𝒔(Π₁(y)), Π₂(y))⟩

and define the function `𝐹':ℕ⭢ℙ`:

  𝐹'(0)    = 𝐺₀        = ⟨0,1⟩
  𝐹'(𝒔(n)) = 𝐺₁(𝐹'(n)) = ⟨𝒔(Π₁(𝐹'(n))), mult(𝒔(Π₁(𝐹'(n))), Π₂(𝐹'(n)))⟩

which follows the iterative scheme (everything depends on `𝐹'(n)`, not on `n` ).

We can now define `𝐹(x) = Π₂(𝐹'(x))` which, being the composition of iterative functions, is iterative and provides the factorial of `x`.

To show how this works, let's evaluate `F'(3)` by applying three times `𝐺₁` to `𝐺₀`:

 F'(0) = 𝐺₀            = ⟨0,1⟩
 F'(1) = 𝐺₁(𝐺₀)        = ⟨𝒔(Π₁(⟨0,1⟩)), mult(𝒔(Π₁(⟨0,1⟩)), Π₂(⟨0,1⟩)⟩ = ⟨𝒔(0), mult(𝒔(0),1)⟩ = ⟨1, 1⟩
 F'(2) = 𝐺₁(𝐺₁(𝐺₀))    = ⟨𝒔(Π₁(⟨1,1⟩)), mult(𝒔(Π₁(⟨1,1⟩)), Π₂(⟨1,1⟩)⟩ = ⟨𝒔(1), mult(𝒔(1),1)⟩ = ⟨2, 2⟩
 F'(3) = 𝐺₁(𝐺₁(𝐺₁(𝐺₀)) = ⟨𝒔(Π₁(⟨2,2⟩)), mult(𝒔(Π₁(⟨2,2⟩)), Π₂(⟨2,2⟩)⟩ = ⟨𝒔(2), mult(𝒔(2),2)⟩ = ⟨3, 6⟩

It's interesting to note what happens here: instead of using the *implicit* stack provided by the recursion scheme, we manage an explicit varaible (one element of the pair) to keep track of the partial results until we reach the desired outcome.

We can use the same technique to define the *predecessor* function `𝑝:ℕ⭢ℕ` :

  𝑝(0)    = 0
  𝑝(𝒔(n)) = n
  

which is primitive recursive (its value depends on `n`, not on `𝑝(n)` as it is required by the iterative scheme).

  𝑝'(0)    = 𝐺₀        = ⟨0,0⟩
  𝑝'(𝒔(n)) = 𝐺₁(p'(n)) = ⟨𝒔(Π₁(𝑝'(n))),Π₁(𝑝'(n))⟩

  𝑝(x) = Π₂(𝑝'(x))

Let's calculate the predecessor of 3:

  𝑝'(0) = 𝐺₀            = ⟨0,0⟩
  𝑝'(1) = 𝐺₁(𝐺₀)        = ⟨𝒔(Π₁(⟨0,0⟩)), Π₁(⟨0,0⟩)⟩ = ⟨1,0⟩
  𝑝'(2) = 𝐺₁(𝐺₁(𝐺₀))    = ⟨𝒔(Π₁(⟨1,0⟩)), Π₁(⟨1,0⟩)⟩ = ⟨2,1⟩
  𝑝'(3) = 𝐺₁(𝐺₁(𝐺₁(𝐺₀)) = ⟨𝒔(Π₁(⟨2,1⟩)), Π₁(⟨2,1⟩)⟩ = ⟨3,2⟩

  𝑝(3) = Π₂(𝑝'(3)) = Π₂(⟨3,2⟩) = 2

## Automatic Synthesis of data constructors
Since data are represented as functions, we need to define a method to derive the 𝜆-function (or CL terms) that encode those functions.
The method is summarized in proposition 5.3 in [1], we'll use it to derive the CL terms for the constructors of some data type.

The resulting encoding are similar, if not exactly the same, as those commonly known as Curch-encodings [4].

In the following, combinators are in bold, variables in italics.

### Constructors of Booleans 𝔹
For Booleans proposition 5.3 gives:

𝐭𝐫𝐮𝐞 𝑡 𝑓 = 𝑡
𝐟𝐚𝐥𝐬𝐞 𝑡 𝑓 = 𝑓

### Constructors of Naturals ℕ
For Naturals proposition 5.3 gives:

𝟎 𝑠 𝑧 = 𝑧
𝐬 𝑛 𝑠 𝑧 = 𝑠 (𝑛 𝑠 𝑧)

### Constructors of lists 𝕃
For Lists proposition 5.3 gives:

  𝐜𝐨𝐧𝐬 𝑎 𝑣 𝑐 𝑛 = 𝑐 𝑎 (𝑣 𝑐 𝑛)
  𝐧𝐢𝐥 𝑐 𝑛 = 𝑛

## Automatic Synthesis of programs

This is the main result (proven in [1]) that we want to leverage in `gerku`:
> By properly representing data types with 𝜆-functions (or CL terms), any iterative function can be automatically translated into a program that computes that function.

This means that writing a program is a four steps process:
- Properly define the data types
- Define an encoding for the data types constructors (determine the corresponding 𝜆-function or CL terms)
- Write the iterative definitions for the functions to be computed by the program
- Convert the functions to 𝜆-function (or CL terms)

Let's write a program that reverses a given list.

### Step 1
The first step is to properly define the data type (which we already did):

  𝓓 = ⟨{𝔸,𝕃}, {cons:𝔸⭢𝕃⭢𝕃, nil:𝕃}⟩

### Step 2
We have already defined the combinators for list constructors in the previous section:

  𝐜𝐨𝐧𝐬 𝑎 𝑣 𝑐 𝑛 = 𝑐 𝑎 (𝑣 𝑐 𝑛)
  𝐧𝐢𝐥 𝑐 𝑛 = 𝑛

### Step 3
Next step is to define the iterative functions we need.

We first define a *reverse cat* function that concatenates two lists in the following way:

   rcat([𝑎 𝑏 𝑐], [𝑑 𝑒])  = [𝑑 𝑒 𝑎 𝑏 𝑐]

It is an iterative function:

   rcat(q,nil)        = 𝒰₁(q)
   rcat(q,cons(a,l))  = cons(a,rcat(q,l)) = 

The auxiliary function `𝒰₁()` returns the first among its arguments.

Now we can define `rev()` in terms of `rcat()`:

   rev(nil) = nil
   rev(cons(a,l)) = rcat(cons(a,nil),rev(l))

Let's check that it works:

   rev([𝑎 𝑏 𝑐]) = rcat([𝑎], rev([𝑏 𝑐]))
                = rcat([𝑎], rcat([𝑏] ,rev([𝑐])))
                = rcat([𝑎], rcat([𝑏] ,rcat([𝑐],rev([]))))
                = rcat([𝑎], rcat([𝑏] ,rcat([𝑐],[])))
                = rcat([𝑎], rcat([𝑏] ,[𝑐]))
                = rcat([𝑎], [𝑐 𝑏])
                = [𝑐 𝑏 𝑎]

The function `rev()` is iterative since it is defined using only iterative functions.

### Step 4
Now we use Definition 5.5 in [1] to automatically derive our programs.

That, for lists, states that given the function:

   𝑓(nil) = ℎ₀
   𝑓(cons(a,l)) = ℎ₁(a,𝑓(l))

the corresponding *program* is:

   𝐟 𝐿 = 𝐿 𝐇₁ 𝐇₀

where `𝐿` is the encoding of the list and 𝐇₀, 𝐇₁ are the *programs* corresponding to the functions `ℎ₀`, `ℎ₁`.

Let's first identify the terms `𝐇₀` and `𝐇₁` that correspond to the iterative definition of the function:

   𝐫𝐜𝐚𝐭 𝑄 𝐧𝐢𝐥 = 𝐇₀ 𝑄 = 𝑄                       ⇒  𝐇₀ = 𝐈    (𝐈 𝑥 = 𝑥)
   𝐫𝐜𝐚𝐭 𝑄 (𝐜𝐨𝐧𝐬 𝑎 𝐿) = 𝐇₁ 𝑄 𝑎 (𝐫𝐜𝐚𝐭 𝑄 𝐿)
                    = 𝐜𝐨𝐧𝐬 𝑎 (𝐫𝐜𝐚𝐭 𝑄 𝐿)        ⇒  𝐇₁ 𝑄 = 𝐜𝐨𝐧𝐬

From definition 5.5 it must be:

   𝐫𝐜𝐚𝐭 𝑄 𝐿 = 𝐿 (𝐇₁ 𝑄) (𝐇₀ 𝑄)
           = 𝐿 𝐜𝐨𝐧𝐬 𝑄

Let's check that this is correct.
Remembering the definitions of `𝐜𝐨𝐧𝐬` and `𝐧𝐢𝐥` found prevously.

  𝐫𝐜𝐚𝐭 [𝑎 𝑏 𝑐] [𝑑 𝑒] = [𝑑 𝑒] 𝐜𝐨𝐧𝐬 [𝑎 𝑏 𝑐]
                   = 𝐜𝐨𝐧𝐬 𝑑 [𝑒] 𝐜𝐨𝐧𝐬 [𝑎 𝑏 𝑐]
                   = 𝐜𝐨𝐧𝐬 𝑑 ([𝑒] 𝐜𝐨𝐧𝐬 [𝑎 𝑏 𝑐])
                   = 𝐜𝐨𝐧𝐬 𝑑 (𝐜𝐨𝐧𝐬 𝑒 𝐧𝐢𝐥 𝐜𝐨𝐧𝐬 [𝑎 𝑏 𝑐])
                   = 𝐜𝐨𝐧𝐬 𝑑 (𝐜𝐨𝐧𝐬 𝑒 (𝐧𝐢𝐥 𝐜𝐨𝐧𝐬 [𝑎 𝑏 𝑐]))
                   = 𝐜𝐨𝐧𝐬 𝑑 (𝐜𝐨𝐧𝐬 𝑒 ([𝑎 𝑏 𝑐]))
                   = 𝐜𝐨𝐧𝐬 𝑑 (𝐜𝐨𝐧𝐬 𝑒 [𝑎 𝑏 𝑐])
                   = 𝐜𝐨𝐧𝐬 𝑑 ([𝑒 𝑎 𝑏 𝑐])
                   = 𝐜𝐨𝐧𝐬 𝑑 [𝑒 𝑎 𝑏 𝑐]
                   = [d 𝑒 𝑎 𝑏 𝑐]

Let's move to `𝐫𝐞𝐯`.

  𝐫𝐞𝐯 𝐧𝐢𝐥 = 𝐧𝐢𝐥                      ⇒  𝐇₀ = 𝐧𝐢𝐥  
  𝐫𝐞𝐯 (𝐜𝐨𝐧𝐬 𝑎 𝐿) = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐞𝐯 𝐿)  ⇒  𝐇₁ 𝑎 = 𝐫𝐜𝐚𝐭 [𝑎] 

We are not there yet as we need an explicit term for `𝐇₁` .
For this we can use the combinators `𝐁` and `𝐂` defined as follows:

  𝐁 𝑥 𝑦 𝑧 = 𝑥 (𝑦 𝑧)
  𝐂 𝑥 𝑦 𝑧 = 𝑥 𝑧 𝑦

and get:

    𝐇₁ 𝑎 = 𝐫𝐜𝐚𝐭 [𝑎] 
         = 𝐫𝐜𝐚𝐭 (𝐜𝐨𝐧𝐬 𝑎 𝐧𝐢𝐥)
         = 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥 𝑎)
         = 𝐫𝐜𝐚𝐭 ((𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥) 𝑎)
         = 𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥) 𝑎

 ⇒  𝐇₁ = 𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)

We can now derive the program for `𝐫𝐞𝐯`:

  𝐫𝐞𝐯 𝐿 = 𝐿 𝐇₁ 𝐇₀ = 𝐿 (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥

Let's check its correctness:

  𝐫𝐞𝐯 [𝑎 𝑏 𝑐] = [𝑎 𝑏 𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥
       = 𝐜𝐨𝐧𝐬 𝑎 [𝑏 𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥
       = (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝑎 ([𝑏 𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥)
       = 𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥) 𝑎 ([𝑏 𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥)
       = 𝐫𝐜𝐚𝐭 ((𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥) 𝑎) ([𝑏 𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥)
       = 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥 𝑎) ([𝑏 𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥)
       = 𝐫𝐜𝐚𝐭 (𝐜𝐨𝐧𝐬 𝑎 𝐧𝐢𝐥) ([𝑏 𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥)
       = 𝐫𝐜𝐚𝐭 [𝑎] ([𝑏 𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥)
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐜𝐨𝐧𝐬 𝑏 [𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥)
       = 𝐫𝐜𝐚𝐭 [𝑎] ((𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝑏 ([𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥) 𝑏 ([𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 ((𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥) 𝑏) ([𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥 𝑏) ([𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 (𝐜𝐨𝐧𝐬 𝑏 𝐧𝐢𝐥) ([𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] ([𝑐] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] (𝐜𝐨𝐧𝐬 𝑐 𝐧𝐢𝐥 (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] ((𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥)) 𝑐 (𝐧𝐢𝐥 (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥))) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥) 𝑐 (𝐧𝐢𝐥 (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥))) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] (𝐫𝐜𝐚𝐭 ((𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥) 𝑐) (𝐧𝐢𝐥 (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥))) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] (𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥 𝑐) (𝐧𝐢𝐥 (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥))) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] (𝐫𝐜𝐚𝐭 (𝐜𝐨𝐧𝐬 𝑐 𝐧𝐢𝐥) (𝐧𝐢𝐥 (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥))) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] (𝐫𝐜𝐚𝐭 [𝑐] (𝐧𝐢𝐥 (𝐁 𝐫𝐜𝐚𝐭 (𝐂 𝐜𝐨𝐧𝐬 𝐧𝐢𝐥))) 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] (𝐫𝐜𝐚𝐭 [𝑐] (𝐧𝐢𝐥)))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] (𝐫𝐜𝐚𝐭 [𝑐] 𝐧𝐢𝐥))
       = 𝐫𝐜𝐚𝐭 [𝑎] (𝐫𝐜𝐚𝐭 [𝑏] [𝑐])
       = 𝐫𝐜𝐚𝐭 [𝑎] [𝑐 𝑏]
       = [𝑐 𝑏 𝑎]

## Conclusion
We have summarized here the key aspects of the theory behind the `gerku` programming language.
It is still not proven if the same results will hold for Concatenative Combinators (and if yes, under which assumptions).
That's the objective of the entire project.

## Bibliography

[1] "*Automatic synthesis of typed Λ-programs on term algebras*", Corrado Böhm, Alessandro Berarducci,
in "*Theoretical Computer Science*", Volume 39, 1985, Pages 135-154, https://doi.org/10.1016/0304-3975(85)90135-5.

[2] "*Reducing recursion to iteration by means of pairs and N-tuples*", Corrado Böhm, in proceedings "*Foundations of Logic and Functional Programming*", 1988, Springer Berlin Heidelberg. https://link.springer.com/chapter/10.1007%2F3-540-19129-1_3

[3] *The Theory of Concatenative Combinators*, Brent Kerby (bkerby at byu dot net). Completed June 19, 2002. Updated February 5, 2007. http://tunes.org/~iepos/joy.html

[4] *Church encoding*, https://en.wikipedia.org/wiki/Church_encoding