Abstract In [1], Kerby discuss abstraction by converting expressions containg concatenative combinators to lambda expressions with variables and then proceeds by abstracting variables from the lambda expressions. This article follows a more direct approach and provides abstraction rules that are aimed to make the algorithm easier to apply and implement. Even if we are mostly interested in showing that such algorithm exists we have made an effort to choose a base of combinators that will keep the resulting expression as short as possible (abstraction usually leads to very long and complex expressions). Further improvements can be done while implementing the algorithm, but we won't discuss them here. Expressions The language of concatenative combinators is defined by the following EBNF:

A striking difference between classic Combinatory Logic (CL) and Concatenative Combinatory Logic (CCL) is the use of quotes. The reason we don't need quotes in CL is that we know that Combinators are left associative and reduction moves from left to right meaning that the expression: 𝐒 𝐈 𝐊 is to be understood as: (𝐒 𝐈) 𝐊

Let's use the small base {s',k} as described in [1] [B] [A] k = A [C] [B] [A] [X] s' = [[C] B] X [C] A Following an approach similar to what we described in [2], we'll look for a combinator base such that [base] base = k [[base] base] base = s' = [k] base

Let's find a combinator 𝜟 such that 𝜟 𝜟 = 𝐊 and 𝜟 𝐊 = 𝐒. If such a combinator exists, it forms a base for the Combinatory Logic. Let's assume 𝜟 has the form 𝐃 𝛼 𝛽 where 𝐃 is the constructor of pairs (i.e. 𝜟 has the form ⟨𝛼,𝛽⟩). The 𝐃 combinator is defined as: 𝐃 𝑥 𝑦 𝑡 = 𝑡 𝑥 𝑦 We want to have 𝜟 𝐊 = 𝐒, so it must be:

We'll define here the free algebra of trees using the concepts already outlined in Foundations of the gerku language whose contents the reader is supposed to be familiar with and won't be repeated here. Data type The Data type of binary trees of integers has two constructors: 𝓓 = ⟨{ℕ,𝕋}, {bic:ℕ⭢𝕋⭢𝕋⭢𝕋 , empb:𝕋 }⟩ such that empb: returns a binary tree with 0 nodes (an empty binary tree)

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.