A very minimal base for Concatenative Combinators

Remo Dentato - Sep 15 - - Dev Community

Introduction

In a previous article I described an abstraction algorithm for Concatenative Combinatory Logic (CCL) which uses a quite large base for convenience.

The reason was practical: the bigger the base, the shorter the abstracted expressions will be.

In 1, Brent Kirby provided examples of much smaller bases for CCL up to just two combinators and we might ask ourselves: "Does a smaller base exists?".

In other words, we are looking for a single combinator (let's call it ๐—ฏ) from which we can derive any other concatenative combinator.

Of course, such combinator, if it exists, will equivalent to an expression using any of the other known bases.

In search of the single one

For our search, let's use the two-combinators base {๐˜€',๐—ธ}:

          (๐‘ฆ) (๐‘ฅ) ๐—ธ  = ๐‘ฅ
  (๐‘ง) (๐‘ฃ) (๐‘ฆ) (๐‘ฅ) ๐˜€' = ((๐‘ง) ๐‘ฃ) ๐‘ฅ (๐‘ง) ๐‘ฆ
Enter fullscreen mode Exit fullscreen mode

We are looing for a combinator ๐—ฏ from which we can calculate the two base combinators ๐˜€' and ๐—ธ:

      ๐—ธ  = (๐—ฏ) ๐—ฏ
      ๐˜€' = ((๐—ฏ) ๐—ฏ) ๐—ฏ = (๐—ธ) ๐—ฏ 
Enter fullscreen mode Exit fullscreen mode

If such combinator exists, it is a base for the Concatenative Combinatory Logic.

Using an helping hand

Before starting, let's assume that the ๐—ฏ has a certain structure:

    ๐—ฏ = (๐›พ) (๐›ฝ) (๐›ผ) ๐˜ 
Enter fullscreen mode Exit fullscreen mode

where ๐˜ is a combinator such that:

  (๐‘ง) (๐‘ฃ) (๐‘ฆ) (๐‘ฅ) ๐˜ = (๐‘ฃ) (๐‘ฆ) (๐‘ฅ) ๐‘ง
Enter fullscreen mode Exit fullscreen mode

Since {๐˜€', ๐—ธ} is a base, we could abstract the free variables ๐‘ง, ๐‘ฃ, ๐‘ฆ, and ๐‘ฅ from the left side expression and obtain a definition for ๐˜ which only contains ๐˜€' and ๐—ธ and no free variables. Due to the length of such definition, for convenience, we'll keep using ๐˜ in the following.

For the same reason, we'll use ๐—ถ as a shorthand for the equivalent expression () (๐—ธ) () ๐˜€' .

Searching ...

Let's start by finding combinators ๐›พ, ๐›ฝ, and ๐›ผ such that (๐—ธ) ๐—ฏ = ๐˜€':

  (๐—ธ) ๐—ฏ = (๐—ธ) (๐›พ) (๐›ฝ) (๐›ผ) ๐˜
        = (๐›พ) (๐›ฝ) (๐›ผ) ๐—ธ 
        = (๐›พ) ๐›ผ 
        = ๐˜€'
Enter fullscreen mode Exit fullscreen mode

In other words, we need to find ๐›ผ and ๐›พ such that (๐›พ) ๐›ผ = ๐˜€'.

This can be simply achieved by choosing: ๐›ผ = ๐—ถ and ๐›พ = ๐˜€':

   (๐›พ) ๐›ผ = (๐˜€') ๐—ถ = ๐˜€' 
Enter fullscreen mode Exit fullscreen mode

We also need (๐—ฏ) ๐—ฏ = ๐—ธ, which means:

  (๐—ฏ) ๐—ฏ = ((๐›พ) (๐›ฝ) (๐›ผ) ๐˜) (๐›พ) (๐›ฝ) (๐›ผ) ๐˜
        = (๐›พ) (๐›ฝ) (๐›ผ) (๐›พ) (๐›ฝ) (๐›ผ) ๐˜
        = (๐›พ) (๐›ฝ) (๐›พ) (๐›ฝ) (๐›ผ) ๐›ผ
        = ๐—ธ
Enter fullscreen mode Exit fullscreen mode

Lookin at the last equality, it means that ๐›ผ, ๐›ฝ, and ๐›พ must be such that:

  ๐—ธ = (๐›พ) (๐›ฝ) (๐›พ) (๐›ฝ) (๐›ผ) ๐›ผ
Enter fullscreen mode Exit fullscreen mode

We already found ๐›ผ and ๐›พ, we can substitute them in the expression to obtain:

  ๐—ธ = (๐›พ)  (๐›ฝ) (๐›พ)  (๐›ฝ) (๐›ผ) ๐›ผ
    = (๐˜€') (๐›ฝ) (๐˜€') (๐›ฝ) (๐—ถ) ๐—ถ
    = (๐˜€') (๐›ฝ) (๐˜€') (๐›ฝ) ๐—ถ
    = (๐˜€') (๐›ฝ) (๐˜€') ๐›ฝ
Enter fullscreen mode Exit fullscreen mode

Now, to satisfy the equality

  ๐—ธ = (๐˜€') (๐›ฝ) (๐˜€') ๐›ฝ
Enter fullscreen mode Exit fullscreen mode

we need ๐›ฝ to be a combinator that deletes three arguments and replaces them with ๐—ธ.

It's easy to see that the following combinator does the trick:

  ๐›ฝ = (((๐—ธ) ๐—ธ) ๐—ธ) ๐—ธ
Enter fullscreen mode Exit fullscreen mode

In fact:

  (๐‘ง) (๐‘ฆ) (๐‘ฅ) ๐›ฝ = (๐‘ง) (๐‘ฆ) (๐‘ฅ) (((๐—ธ) ๐—ธ) ๐—ธ) ๐—ธ
                = (๐‘ง) (๐‘ฆ) ((๐—ธ) ๐—ธ) ๐—ธ
                = (๐‘ง) (๐—ธ) ๐—ธ
                = ๐—ธ
Enter fullscreen mode Exit fullscreen mode

Which gives us a definition for ๐—ฏ:

   ๐—ฏ = (๐˜€') ((((๐—ธ) ๐—ธ) ๐—ธ) ๐—ธ) (๐—ถ) ๐˜
Enter fullscreen mode Exit fullscreen mode

Since, by definition, any expression using only combinators, is a combinator itself, we have found our single-combinator base.

Conclusion

We have proved that there exist a base {๐—ฏ} for the Concatenative Combinatory Logic that is formed by a single combinator.

The result is not surprising as the same result is valid in the standard Combinatory Logic and comes from the fact that the two computational model are equivalent.

For how impractical it may be to use a single combinator as a base, this results may be of interest in some specific context.

Bibliography

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

. . . . . . . . . . . . . . . . . . . . . .
Terabox Video Player