DEV Community

Cover image for A Concatenative Combinators abstraction algorithm
Remo Dentato
Remo Dentato

Posted on • Edited on

A Concatenative Combinators abstraction algorithm

#concatenative

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 := [π‘Žπ‘π‘-π‘₯𝑦𝑧]
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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  = (π‘₯) (𝑦)
Enter fullscreen mode Exit fullscreen mode

You can interpret the definition of swap above by saying that in any given expression you can replace any occurrence of:

    (𝑦) (π‘₯) swap
Enter fullscreen mode Exit fullscreen mode

with:

    (π‘₯) (𝑦)
Enter fullscreen mode Exit fullscreen mode

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  = (𝑦) π‘₯ (𝑦)
Enter fullscreen mode Exit fullscreen mode

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) π‘₯
Enter fullscreen mode Exit fullscreen mode

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 𝓕:

           𝓖 = {𝓕}[(π‘₯)]  ->  (π‘₯) 𝓖 = 𝓕
Enter fullscreen mode Exit fullscreen mode

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:

         {𝓕}[(𝑦) (π‘₯)] = {{𝓕}[(π‘₯)]}[(𝑦)] = 𝓖
Enter fullscreen mode Exit fullscreen mode

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:

  1. The expression is empty;

  2. The expression can be split in two parts with first terms containing the variable π‘₯ followed by other terms not containing π‘₯;

  3. The expression can be split in two parts with first terms not containing the variable π‘₯ followed by other terms containing π‘₯;

  4. 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);

  5. The first term is the variable π‘₯ (unquoted).

This leads to the following abstraction rules:

     1           {}[(π‘₯)] = zap
     2       {𝓝 𝓖}[(π‘₯)] = {𝓝}[(π‘₯)] 𝓖
     3       {𝓖 𝓝}[(π‘₯)] = (𝓖) dip {𝓝}[(π‘₯)]
     4    {(𝓝) π“œ}[(π‘₯)] = ({𝓝}[(π‘₯)]) cosp {π“œ}[(π‘₯)]
     5       {π‘₯ π“œ}[(π‘₯)] = run {π“œ}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

Let's check that applying the result to (π‘₯) we got the empty expression:

       (π‘₯) zap
       ╰─────╯            by def. of zap
                      ◄── empty expression
       β•°β•―                 by def. of abstraction
       (π‘₯) {}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

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      {𝓝 𝓖}[(π‘₯)] = {𝓝}[(π‘₯)] 𝓖
Enter fullscreen mode Exit fullscreen mode

Let's check that rule 2 holds:

     (π‘₯) {𝓝}[(π‘₯)] 𝓖
     ╰───────────╯        by definition of abstraction
     𝓝 𝓖
     ╰──╯                 by definition of abstraction
     (π‘₯) {𝓝 𝓖}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

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 {𝓝}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

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
       (π‘₯) {𝓖 𝓝}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

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 {π“œ}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

Let's apply it to (π‘₯):

       (π‘₯) ({𝓝}[(π‘₯)]) cosp {π“œ}[(π‘₯)]
       ╰──────────────────╯                by def. of cosp
       ((π‘₯) {𝓝}[(π‘₯)]) (π‘₯) {π“œ}[(π‘₯)]
        ╰───────────╯                      by def. of abstraction
       (𝓝) (π‘₯) {π“œ}[(π‘₯)]
           ╰────────────╯                  by def. of abstraction
       (𝓝) π“œ
       ╰─────╯                             by def. of abstraction
       (π‘₯) {(𝓝) π“œ}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

Rule 5

This is the rule to apply when the first term is π‘₯.

     5         {π‘₯ π“œ}[(π‘₯)] = run {π“œ}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

To show that rules 5 holds, let's apply it to (π‘₯):

               (π‘₯) run {π“œ}[(π‘₯)]
               ╰─────╯              by def. of run
               π‘₯ (π‘₯) {π“œ}[(π‘₯)]
                 ╰───────────╯      by def. of abstraction
               π‘₯ π“œ
               ╰──╯                 by def. of abstraction
               (π‘₯) {π‘₯ π“œ}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

Optimization

The only optimization we mention here is the possibility of simplifying some special cases:

     3a         {𝓖}[(π‘₯)] = zap 𝓖
     4a    {(π‘₯) π“œ}[(π‘₯)] = dup {π“œ}[(π‘₯)]
     4b      {(𝓝)}[(π‘₯)] = ({𝓝}[(π‘₯)]) cons
     4c       {(π‘₯)}[(π‘₯)] = 
     5a         {π‘₯}[(π‘₯)] = i
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
  (π‘₯) {(𝓝)}[(π‘₯)]
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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)

Read next

keertana_d_ea3967a9d000bc profile image

Indian Law For A Common Man

keertana d -

patrek profile image

SOPS - Secrets encryptΓ©s dans un dΓ©pΓ΄t GIT

Patrick Turcotte -

chetan_hs_c12b4d5cd3fdded profile image

Untold Aspects of Software Engineering Interviews from an ex-Meta Engineer

Chetan HS -

sreekeshiyer profile image

Setting up a Queue Ingestion system for S3 to Redshift Transfer

Sreekesh Iyer -