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 {๐',๐ธ}
:
(๐ฆ) (๐ฅ) ๐ธ = ๐ฅ
(๐ง) (๐ฃ) (๐ฆ) (๐ฅ) ๐' = ((๐ง) ๐ฃ) ๐ฅ (๐ง) ๐ฆ
We are looing for a combinator ๐ฏ
from which we can calculate the two base combinators ๐'
and ๐ธ
:
๐ธ = (๐ฏ) ๐ฏ
๐' = ((๐ฏ) ๐ฏ) ๐ฏ = (๐ธ) ๐ฏ
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:
๐ฏ = (๐พ) (๐ฝ) (๐ผ) ๐
where ๐
is a combinator such that:
(๐ง) (๐ฃ) (๐ฆ) (๐ฅ) ๐ = (๐ฃ) (๐ฆ) (๐ฅ) ๐ง
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 (๐ธ) ๐ฏ = ๐'
:
(๐ธ) ๐ฏ = (๐ธ) (๐พ) (๐ฝ) (๐ผ) ๐
= (๐พ) (๐ฝ) (๐ผ) ๐ธ
= (๐พ) ๐ผ
= ๐'
In other words, we need to find ๐ผ
and ๐พ
such that (๐พ) ๐ผ = ๐'
.
This can be simply achieved by choosing: ๐ผ = ๐ถ
and ๐พ = ๐'
:
(๐พ) ๐ผ = (๐') ๐ถ = ๐'
We also need (๐ฏ) ๐ฏ = ๐ธ
, which means:
(๐ฏ) ๐ฏ = ((๐พ) (๐ฝ) (๐ผ) ๐) (๐พ) (๐ฝ) (๐ผ) ๐
= (๐พ) (๐ฝ) (๐ผ) (๐พ) (๐ฝ) (๐ผ) ๐
= (๐พ) (๐ฝ) (๐พ) (๐ฝ) (๐ผ) ๐ผ
= ๐ธ
Lookin at the last equality, it means that ๐ผ
, ๐ฝ
, and ๐พ
must be such that:
๐ธ = (๐พ) (๐ฝ) (๐พ) (๐ฝ) (๐ผ) ๐ผ
We already found ๐ผ
and ๐พ
, we can substitute them in the expression to obtain:
๐ธ = (๐พ) (๐ฝ) (๐พ) (๐ฝ) (๐ผ) ๐ผ
= (๐') (๐ฝ) (๐') (๐ฝ) (๐ถ) ๐ถ
= (๐') (๐ฝ) (๐') (๐ฝ) ๐ถ
= (๐') (๐ฝ) (๐') ๐ฝ
Now, to satisfy the equality
๐ธ = (๐') (๐ฝ) (๐') ๐ฝ
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:
๐ฝ = (((๐ธ) ๐ธ) ๐ธ) ๐ธ
In fact:
(๐ง) (๐ฆ) (๐ฅ) ๐ฝ = (๐ง) (๐ฆ) (๐ฅ) (((๐ธ) ๐ธ) ๐ธ) ๐ธ
= (๐ง) (๐ฆ) ((๐ธ) ๐ธ) ๐ธ
= (๐ง) (๐ธ) ๐ธ
= ๐ธ
Which gives us a definition for ๐ฏ
:
๐ฏ = (๐') ((((๐ธ) ๐ธ) ๐ธ) ๐ธ) (๐ถ) ๐
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))
Top comments (0)