Concatenative calculus
Concatenative calculus (also called concatenative combinatory logic) is a combinator calculus where all combinators apply concatenatively.[1]
There are two types of terms; primitive and quoted. Primitive terms are combinators, or atoms of data. A quoted term is an ordered list of terms (or empty). Since quotes can nest arbitrarily, the quotation delimiters are generally brackets or parentheses.
Combinators operate on quoted values only, each capturing and rewriting several terms which precede it. Rewriting is called reduction, as in other calculi. Like other calculi, concatenative calculus without evaluation order is nondeterministic.
Combinators
Combinators rewrite several quoted values which precede them, and remove themselves. For this listing a syntax where quoted terms are wrapped in square brackets will be used. To users of Forth or other stack-based languages, these combinators may seem familiar (Kerby terminology):
[A] [B] swap ⊢ [B] [A] [A] dup ⊢ [A] [A] [A] zap ⊢
For the swap combinator, [A] [B] swap ⊢ [B] [A] means that [A] [B] swap (swap preceded by two quoted terms) rewrites to (⊢) [B] [A] (the same two quoted terms except swapped positions). Here, A and B can be anything, in this case they are meaningless atoms, but they could also be combinators, sequences of combinators, quoted terms, etc.
Note that these relations are two-way in the same way that other forms of algebraic manipulation are. However, evaluation seeks to eventually reduce the amount of combinators in the expression. To evaluate an expression the above and below ordering of the expressions (prior ⊢ reduced) is used.
The swap, dup, and zap combinators have analogs with pushdown automata and stack-based languages. Zap may also be called pop or drop.
These combinators alone are not especially interesting, they do not consider the contents of quotes, they only shuffle their positions or copy/delete. The following combinators access the contents of quotes and build new ones:
[A] [B] cat ⊢ [A B] [A] unit ⊢ [[A]] [A] i ⊢ A
The first combinator, cat, unquotes the two terms which precede it, concatenates them together, and quotes the result. The unit (or wrap, quote) combinator wraps its argument in another layer of quotes. The i (or unwrap, unquote) combinator unwraps its arguments outermost layer of quotes.
These six combinators form a complete basis, which can be seen as the programming language mlatu-6. This means that expressions made up solely of these combinators, and quotes, is Turing complete.
Using dup and unwrap, we can create a small looping (non-normalizing) expression:
[dup unwrap] dup unwrap ⊢ [dup unwrap] [dup unwrap] unwrap ⊢ [dup unwrap] dup unwrap
Kerby provides two more combinators for an alternate basis:
[A] [B] cons ⊢ [[A] B] [A] [B] dip ⊢ B [A]
Lambdas
A lambda is an expression which consumes prior quotes, unquotes them, binds them to variables, then rewrites them to produce a new expression. Lambdas are named after the construct in lambda calculus. An example lambda is (Kerby notation):
A\ B\ A [B]
This is an expression of the dip combinator in lambda form. The terms with a final slash pop, unquote, and bind variables. Following binding is the rewrite rule.
All combinators can be expressed in terms of lambdas. In fact, the term combinator refers to a special type of lambda expression which has no free variables. A free variable is one which is taken from the environment. In the following lambda:
B\ A [B]
The variable A is from the environment, it is free. This means that this lambda is not a combinator. The above implementation of dip is however a combinator, since it doesn't reference any external variables. This is in line with the general definition of combinator in functional calculus.
All combinators are expressible as lambdas, and the converse is also true. Kerby provides an algorithm which restates all lambda expressions in terms of i, dup, dip, cons, zap, which proves that this basis is Turing complete.
Applicative combinators
An applicative combinator is one whose rewritten form consists of any number of quoted terms followed by a single dequoted term. Unwrap/unquote/i is the simplest applicative combinator, with no quoted terms.
Kerby provides the following applicative combinators:[1]
[A] i ⊢ A [A] [B] w ⊢ [A] [A] B [A] [B] k ⊢ A [A] [B] [C] b ⊢ [[A] B] C [A] [B] [C] c ⊢ [B] [A] C [A] [B] [C] s ⊢ [[A] B] [A] C
These combinators effectively implement a postfix notation for the combinatory logic bases BCKW and SKI.
Evaluation
Concatenative calculus without evaluation strategy is nondeterministic. User:Xylochoron provided the example [[dup i] dup i] zap (Kerby notation) or ((+<)+<)- (mlatu notation), which loops forever if innermost evaluation is used, but immediately rewrites to the empty expression if outermost evaluation is used.
Kerby refers to systems where quotes are meaningless data as having opaque quotation, with systems that evaluate the contents of quotes having transparent quotation. Joy and mlatu have opaque quotation.
Opaque evaluation is deterministic without evaluation order. That is, where reduce(Z) refers to the reduced form of Z, and X || Y is the concatenation of X followed by Y, for two non-reduced concatenative expressions A and B, reduce(reduce(A) || reduce(B)) is the same as reduce(A || B).[verify]
Bases
Combinators are able to express behaviors of other combinators. This means that a set of combinators can implement other additional combinators. A set of combinators is called a basis, with a basis capable of implementing any combinator being referred to as a complete basis, although a complete basis is often referred to as simply a basis. Since there is an algorithm which converts any lambda expression into a combinator expression, and lambda calculus is Turing complete, a complete basis is also Turing complete.
Kerby lists several small complete bases:[1]
The i, dip, cons, dup, zap basis (used in the lambda translation algorithm):
[A] i ⊢ A [A] [B] dip ⊢ B [A] [A] [B] cons ⊢ [[A] B] [A] dup ⊢ [A] [A] [A] zap ⊢
The cons, sip, k basis:
[A] [B] cons ⊢ [[A] B] [A] [B] sip ⊢ [A] B [A] [A] [B] k ⊢ B
The s', k basis:
[A] [B] [F] [G] s' ⊢ [[A] B] G [A] F [A] [B] k ⊢ B
The cake, k basis:
[A] [B] cake ⊢ [[A] B] [B [A]] [A] [B] k ⊢ B
The j', i basis, which lacks combinators which delete arguments (like zap or k) this is called conservative:
[A] [B] [C] [D] [E] j' ⊢ [[B] E [A] D] [C] D [A] i ⊢ A
The coup, sap basis, another conservative basis:
[A] [B] [C] coup ⊢ [[A] B] [C] [C] [A] [B] sap ⊢ B A
The take, cat, i basis, which is both conservative and non-duplicating, a basis with both of these properties is linear:
[A] [B] take ⊢ [B [A]] [A] [B] cat ⊢ [A B] [A] i ⊢ A
The cons, sap basis, another linear basis:
[A] [B] cons ⊢ [[A] B] [A] [B] sap ⊢ B A
Combinator listing
Kerby lists the following combinators:
[A] zap ==
[A] i == A
[A] unit == [[A]]
[A] rep == A A
[A] m == [A] A
[A] run == A [A]
[A] dup == [A] [A]
[B] [A] k == A
[B] [A] z == B
[B] [A] nip == [A]
[B] [A] sap == A B
[B] [A] t == [A] B
[B] [A] dip == A [B]
[B] [A] cat == [B A]
[B] [A] swat == [A B]
[B] [A] swap == [A] [B]
[B] [A] cons == [[B] A]
[B] [A] take == [A [B]]
[B] [A] tack == [B [A]]
[B] [A] sip == [B] A [B]
[B] [A] w == [B] [B] A
[B] [A] peek == [B] [A] [B]
[B] [A] cake == [[B] A] [A [B]]
[C] [B] [A] poke == [A] [B]
[C] [B] [A] b == [[C] B] A
[C] [B] [A] c == [B] [C] A
[C] [B] [A] dig == [B] [A] [C]
[C] [B] [A] bury == [A] [C] [B]
[C] [B] [A] flip == [A] [B] [C]
[C] [B] [A] s == [[C] B] [C] A
[D] [C] [B] [A] s' == [[D] C] A [D] B
[D] [C] [B] [A] j == [[C] [D] A] [B] A
[E] [D] [C] [B] [A] j' == [[D] A [E] B] [C] B
Languages
See also
References
- ↑ 1.0 1.1 1.2 Kerby, Brent. (2002, June 19). The Theory of Concatenative Combinators. http://tunes.org/~iepos/joy.html