Abstract
Concatenative programming languages like Forth or Joy have their theoretical foundation in a computational model that is equivalent to 𝜆-calculus and Combinatory Logic: the Concatenative Combinatory Logic. This article shows a simple abstraction algorithm that is akin to the process of compilation.
In [1], Kerby discusses abstraction by converting expressions containing 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 at making 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 made while implementing the algorithm, but we won't discuss them here.
Expressions
The language of concatenative combinators is defined by the following EBNF:
expression := term+
term := combinator | var | quote
quote := '(' expression? ')'
combinator := [A-Za-z_][A-Za-z_0-9]*
var := [𝑎𝑏𝑐-𝑥𝑦𝑧]
That can be summarized as:
- An expression is a list of terms
- A combinator is a term
- A variable is a term
- A quote (an expression enclosed in parenthesis) is a term
- The nil quote
()is a term
Note that variables are notated with a different set of symbols.
Some examples:
(𝑦) dup
(cons (𝑧)) sip (𝑦)
(alpha) (beta) dip
The evaluation of an expression proceeds from left to right by finding the first combinator that can be successfully reduced (i.e. the one that has enough quotes at its left) and replacing it and its arguments with the result of its application to the arguments.
We assume that, as in classical Combinatory Logic, the Church-Rosser theorem holds. While not a real proof, at the end of this paper we'll provide a reasoning that reassures us on the validity of the Church-Rosser theorem.
Concatenative Combinators
Let's use an intuitive definition of what a concatenative combinator is:
A combinator is an operator that shuffles, duplicates or removes
quotes there are at their left in an expression.
The behavior of a combinator is defined as an equivalence like this:
(𝑦) (𝑥) swap = (𝑥) (𝑦)
You can interpret the definition of swap above by saying that in any given expression you can replace any occurrence of:
(𝑦) (𝑥) swap
with:
(𝑥) (𝑦)
For the sake of reasoning (and as a possible strategy of implementation) we can think of a combinator as a program that operates on a stack:
A combinator is a program that pulls a certain number of quoted expressions from a stack and pushes back in the stack a number of expressions containing any number of them (even zero), possibily in a different order
(Non minimal) Base for concatenative combinators
To simplify the abstraction algorithm we'll use the following combinators:
(𝑥) i = 𝑥
(𝑥) zap =
(𝑥) run = 𝑥 (𝑥)
(𝑥) dup = (𝑥) (𝑥)
(𝑦) (𝑥) cons = ((𝑦) 𝑥)
(𝑦) (𝑥) cosp = ((𝑦) 𝑥) (𝑦)
(𝑦) (𝑥) dip = 𝑥 (𝑦)
(𝑦) (𝑥) sip = (𝑦) 𝑥 (𝑦)
which are a superset of the bases defined in [1] and, hence, ensure that every possible expression can be represented using those combinators.
We'll extend the concept of combinator defintions by allowing a combinator to add other elements that were not in the original arguments.
For example:
(𝑦) (𝑥) add = (𝑦) (succ) 𝑥
(𝑦) (𝑥) mult = (zero) ((𝑦) add) 𝑥
Abstraction
The abstraction of an expression 𝓕 with respect to the variable 𝑥 is denoted with {𝓕}[(𝑥)].
The result of the abstraction of the variable 𝑥 from the expression 𝓕 is an expression 𝓖 that does not contain 𝑥 and that, when applied to (𝑥). will return 𝓕:
𝓖 = {𝓕}[(𝑥)] -> (𝑥) 𝓖 = 𝓕
In a sense, abstraction is similar to compilation. Given an expression 𝓕 containing a variable 𝑥 (the source code) we can see {𝓕}[(𝑥)] as a program that when applied to a quoted expression (𝓡) will result in the original expression where any occurence of the variable 𝑥 is replaced by 𝓡.
When abstracting multiple variable we'll have:
{𝓕}[(𝑦) (𝑥)] = {{𝓕}[(𝑥)]}[(𝑦)] = 𝓖
In other words, we first abstract wrt 𝑥, then 𝑦 and the result 𝓖 is such that (𝑦) (𝑥) 𝓖 = 𝓕.
Note that abstraction is defined with respect to a quoted variable as concatenative combinators are defined to only operate on quotes.
Abstraction rules
We'll use the following definitions:
-
𝑥is a generic variable -
𝓖is a non empty expression that does not contain𝑥(i.e.𝑥does not occur in𝓖) -
𝓜is an expressions that may contain𝑥(𝑥may occur in𝓜) -
𝓝is an expressions that do contain𝑥(𝑥occurs in𝓝)
Given an expression, looking at the list of terms from left to right there can only be the following cases:
The expression is empty;
The expression can be split in two parts with first terms containing the variable
𝑥followed by other terms not containing𝑥;The expression can be split in two parts with first terms not containing the variable
𝑥followed by other terms containing𝑥;The first term is a quote containing
𝑥(otherwise it would have been accounted for in case 3) followed by an expression containing𝑥(otherwise it would have been accounted for in case 0);The first term is the variable
𝑥(unquoted).
This leads to the following abstraction rules:
1 {}[(𝑥)] = zap
2 {𝓝 𝓖}[(𝑥)] = {𝓝}[(𝑥)] 𝓖
3 {𝓖 𝓝}[(𝑥)] = (𝓖) dip {𝓝}[(𝑥)]
4 {(𝓝) 𝓜}[(𝑥)] = ({𝓝}[(𝑥)]) cosp {𝓜}[(𝑥)]
5 {𝑥 𝓜}[(𝑥)] = run {𝓜}[(𝑥)]
Note that the expressions on the right side can't be reduced further without being applied to a quote.
It's easy to prove, by induction on the length of the expressions, that the algorithm converges: at each step the expressions to be abstracted become smaller and smaller.
In the following subsection we'll show that the rules do hold by applying them to (𝑥) and checking that the result is, indeed, the original expression.
Rule 1
This is the base case for when the expression is empty.
1 {}[(𝑥)] = zap
Let's check that applying the result to (𝑥) we got the empty expression:
(𝑥) zap
╰─────╯ by def. of zap
◄── empty expression
╰╯ by def. of abstraction
(𝑥) {}[(𝑥)]
Rule 2
This rule allows us to stop earlier in the abstraction process: trailing terms not containing 𝑥 can be left untouched.
This is implied by the fact that the combinators are concatenative.
2 {𝓝 𝓖}[(𝑥)] = {𝓝}[(𝑥)] 𝓖
Let's check that rule 2 holds:
(𝑥) {𝓝}[(𝑥)] 𝓖
╰───────────╯ by definition of abstraction
𝓝 𝓖
╰──╯ by definition of abstraction
(𝑥) {𝓝 𝓖}[(𝑥)]
Rule 3
This rule is to be applied when the expression consists of a list of terms which do not contain 𝑥 followed by a list of terms which contain 𝑥.
3 {𝓖 𝓝}[(𝑥)] = (𝓖) dip {𝓝}[(𝑥)]
To prove that this rule holds, let's apply it to (𝑥) and check that the result is 𝓖 𝓝.
(𝑥) (𝓖) dip {𝓝}[(𝑥)]
╰─────────╯ by def. of dip
𝓖 (𝑥) {𝓝}[(𝑥)]
╰───────────╯ by def of abstraction
𝓖 𝓝
╰──╯ by def of abstraction
(𝑥) {𝓖 𝓝}[(𝑥)]
Rule 4
This rule is to be applied when the expression consist of a quote that contains 𝑥 followed by a list of terms which contain 𝑥 (if they didn't we would have used rule 0).
4 {(𝓝) 𝓜}[(𝑥)] = ({𝓝}[(𝑥)]) cosp {𝓜}[(𝑥)]
Let's apply it to (𝑥):
(𝑥) ({𝓝}[(𝑥)]) cosp {𝓜}[(𝑥)]
╰──────────────────╯ by def. of cosp
((𝑥) {𝓝}[(𝑥)]) (𝑥) {𝓜}[(𝑥)]
╰───────────╯ by def. of abstraction
(𝓝) (𝑥) {𝓜}[(𝑥)]
╰────────────╯ by def. of abstraction
(𝓝) 𝓜
╰─────╯ by def. of abstraction
(𝑥) {(𝓝) 𝓜}[(𝑥)]
Rule 5
This is the rule to apply when the first term is 𝑥.
5 {𝑥 𝓜}[(𝑥)] = run {𝓜}[(𝑥)]
To show that rules 5 holds, let's apply it to (𝑥):
(𝑥) run {𝓜}[(𝑥)]
╰─────╯ by def. of run
𝑥 (𝑥) {𝓜}[(𝑥)]
╰───────────╯ by def. of abstraction
𝑥 𝓜
╰──╯ by def. of abstraction
(𝑥) {𝑥 𝓜}[(𝑥)]
Optimization
The only optimization we mention here is the possibility of simplifying some special cases:
3a {𝓖}[(𝑥)] = zap 𝓖
4a {(𝑥) 𝓜}[(𝑥)] = dup {𝓜}[(𝑥)]
4b {(𝓝)}[(𝑥)] = ({𝓝}[(𝑥)]) cons
4c {(𝑥)}[(𝑥)] =
5a {𝑥}[(𝑥)] = i
They can be easily checked as we did in the previous section.
Note that those special cases are included in the general case when one of the expressions is empty or has a special form.
Let's give just one example that shows that rule 4b is implied in rule 4 when the expression 𝓜 is empty.
4 {(𝓝) 𝓜}[(𝑥)] = ({𝓝}[(𝑥)]) cosp {𝓜}[(𝑥)]
4b {(𝓝)}[(𝑥)] = ({𝓝}[(𝑥)]) cons
It's easy to see that, under the assumption of 𝓜 being empty, the two are equivalent:
(𝑥) {(𝓝) 𝓜}[(𝑥)]
╰────────────╯ by rule 4
(𝑥) ({𝓝}[(𝑥)]) cosp {𝓜}[(𝑥)]
╰────────╯ by hypotesis that 𝓜 is empty
(𝑥) ({𝓝}[(𝑥)]) cosp {}[(𝑥)]
╰──────────────────╯ by def. of cosp
((𝑥) ({𝓝}[(𝑥)])) (𝑥) {}[(𝑥)]
╰──────╯ by rule 1
((𝑥) ({𝓝}[(𝑥)])) (𝑥) zap
╰──────╯ by def. of zap
((𝑥) ({𝓝}[(𝑥)]))
╰───────────────╯ by def. of cons
(𝑥) ({𝓝}[(𝑥)]) cons
╰──────────────────╯ by rule 4b
(𝑥) {(𝓝)}[(𝑥)]
Quotes
As said at the beginning. combinators only operate on quotes.
This is needed since (as in CL and 𝜆-calculus) there is no distinction between functions (programs) and data. Quotes are what make this distinction.
Note that we have assumed that quotes are transparent. i.e. that reductions may happen within a quote. This has the advantage that all expressions are reduced to their minimal form but also has the disadvantage of having to compute any single quotes even if they might be discarded at a later time. Opaque quotes allow for lazy evaluation and the content of a quote is evaluated only when (and if) it is really needed, not before.
From the abstraction algorithm there is no difference as the two type of quotes are equivalent.
The Church-Rosser theorem
The Church-Rosser theorem, plays a key role in the evaluation of an expression and the fact that it holds for concatenative combinators is an assumption for the abstraction algorithm to work. It is also essential for the discussion on transparent/opaque quotes in the preceding section.
It can be formulated in many different ways, this is one of them:
Let 𝓐 ⊳ 𝓑 be the reduction of the expression 𝓐 to the expression 𝓑; then
𝓤 ⊳ 𝓧 ∧ 𝓤 ⊳ 𝓨 ⇒ ∃𝓩: 𝓧 ⊳ 𝓩 ∧ 𝓨 ⊳ 𝓩
In plain words, if an expression 𝓤 can be reduced to two different expressions 𝓧 and 𝓨, then there is an expression 𝓩 to whom both 𝓧 and 𝓨 can be reduced.
Which means that the strategy of reductions is irrelevant as any of them will lead to the same expression 𝓩.
While the general proof of this theorem is quite complex, in our specific case (concatenative combinators that only act on quotes) it's pretty straightforwad to convince ourselves that the theorem holds.
Let's consider the following expression:
(𝓊) A (𝓋) B
where A and B are combinators and 𝓊 and 𝓋 are generic expressions.
The only interesting case is when both of them can be reduced (i.e. they both are a redex). Let's consider one step of reduction.
If we reduce (𝓊) A, there will be no consequence on (𝓋) B, since it is already a redex.
If we reduce (𝓋) B the result can be:
- a redex itself, which brings us in the same situation we were before the reduction,
- a non reducible expression like
(𝓈) (𝓉) C.
The resulting expression (𝓊) A (𝓈) (𝓉) C now contains only one redex ((𝓊) A) because the combinator C only operates on quotes and A is unquoted.
This reasoning can be repeated for a more general case but it's easy to see that the redex in an expression to do not interfere with each other and, hence, the order in which they are reduced is irrelevant for the end result.
UPDATE: An AI-generated proof is now available here. Please check it and provide your feedback if you feel inclined to do so.
Conclusion
We have defined an abstraction algorithm for Concatenative combinators that is simple enough to be implemented and even applied by hand
This frees us from the need to handle variables when using Concatenative Combinators.
We have also argued around the validity of the Church-Rosser theorem that is an assumption for the abstraction algorithm to work.
Here are the list of all the abstraction rules (including the special cases):
1 {}[(𝑥)] = zap
2 {𝓝 𝓖}[(𝑥)] = {𝓝}[(𝑥)] 𝓖
3 {𝓖 𝓝}[(𝑥)] = (𝓖) dip {𝓝}[(𝑥)]
3a {𝓖}[(𝑥)] = zap 𝓖
4 {(𝓝) 𝓜}[(𝑥)] = ({𝓝}[(𝑥)]) cosp {𝓜}[(𝑥)]
4a {(𝑥) 𝓜}[(𝑥)] = dup {𝓜}[(𝑥)]
4b {(𝓝)}[(𝑥)] = ({𝓝}[(𝑥)]) cons
4c {(𝑥)}[(𝑥)] =
5 {𝑥 𝓜}[(𝑥)] = run {𝓜}[(𝑥)]
5a {𝑥}[(𝑥)] = i
where
-
𝑥is a generic variable -
𝓖is a non empty expression that does not contain𝑥(i.e.𝑥does not occur in𝓖) -
𝓜is an expressions that may contain𝑥(𝑥may occur in𝓜) -
𝓝is an expressions that do contain𝑥(𝑥occurs in𝓝)
Bibliography
[1] The Theory of Concatenative Combinators,
Brent Kerby (bkerby at byu dot net).
Completed June 19, 2002. Updated February 5, 2007.
(link)
[2] Lambda-Calculus and Combinators, an introduction,
J. Roger Hindley, Jonathan P. Seldin
(link)
Top comments (0)