Brainfuck Encoded Concatenative Calculus
| Paradigm(s) | Concatenative |
|---|---|
| Designed by | User:Olus2000 |
| Appeared in | 2022 |
| Memory system | Expression rewriting |
| Computational class | Turing-complete |
| Reference implementation | Python |
| Influenced by | Brainfuck Concatenative Calculus |
| File extension(s) | .txt |
Brainfuck Encoded Concatenative Calculus (BECC, pronounced [bɛkʰ]) is a minimalistic programming language based on Concatenative Calculus. It keeps brainfuck's eight single-character commands and maps CC operators onto them, with additional input and output operators. If you came here looking for info on the Concatenative Calculus itself check out External resources.
Language overview
BECC operates by expression substitution. A program consists of a single expression which consists of operators (+-><.,) and quoted subexpressions (expressions encased in []). Any other characters are considered comments and removed before evaluation.
Evaluating a BECC expression consists of finding patterns in the outermost expression and performing substitutions according to these rules:
| Operator | Pattern | Substitution | CC equivalent |
|---|---|---|---|
>
|
[A][B]>
|
[[A]B]
|
cons |
<
|
[A][B]<
|
[B[A]]
|
take |
+
|
[A]+
|
[A][A]
|
dup |
-
|
[A][B]-
|
B
|
k |
.
|
[A].
|
Empty | No equivalent |
,
|
,
|
[INPUT]
|
No equivalent |
Rules are structured as a single operator acting on preceding quoted arguments. In case that multiple rules match at a time the leftmost substitution should be performed. I/O operators interface with the outside world in an implementation dependent way. Author suggests that input is read and written as one Church-encoded number at a time.
Computational class
BECC is Turing-complete because it is a variant of Concatenative Calculus which is Turing-complete. Some standard CC operators that are usually used as basis can be defined like this:
| CC operator | Pattern | Substitution | BECC implementation |
|---|---|---|---|
dup
|
[A] dup
|
[A] [A]
|
+
|
swap
|
[A] [B] swap
|
[B] [A]
|
[]<<+-
|
drop
|
[A] drop
|
Empty | []-
|
quote
|
[A] quote
|
[[A]]
|
[]> or []<
|
cat
|
[A] [B] cat
|
[A B]
|
[[+-]<+-+-]>>*
|
call
|
[A] call
|
A
|
+-
|
k
|
[A] [B] k
|
B
|
-
|
cake
|
[A] [B] cake
|
[[A] B] [B [A]]
|
[]>>+[+->]<+-+-<
|
*This BECC code doesn't produce exactly the same results as cat, but they are equivalent. Since CC doesn't provide any way of looking into the quotations except from calling them it is sufficient that [A] [B] cat call is equivalent to [A] [B] [[+-]<+-+-]>> call, which can be easily shown to be true:
[A] [B] [[+-] <+-+-] >> +- Starting expression; code of cat split with spaces for readability and BECC code substituted for call [A] [[B] [+-] <+-+-] > +- cons rule [[A] [B] [+-] <+-+-] +- cons rule; call is executed on the result of cat [[A] [B] [+-] <+-+-] [[A] [B] [+-] <+-+-] - dup rule [A] [B] [+-] <+-+- k rule [A] [+- [B]] +-+- take rule [A] [+- [B]] [+- [B]] -+- dup rule [A] +- [B] +- k rule [A] [A] - [B] +- dup rule A [B] +- k rule; A is executed A [B] [B] - dup rule A B k rule; B is executed
This equivalence may break on some output interpretation schemes.
Church encoding
The only values in Concatenative Calculus are quotations, so numbers, booleans and others have to be encoded in some way. Since the only way to check what's inside a quotation is to call it the values should be defined in terms of what effects they should have when called. One such encoding can be borrowed from Alonzo Church's work on Lambda Calculus.
Boolean values
Lambda Calculus Church encoding of boolean values defines them as functions of two parameters returning either of them depending on the boolean value. In CC it corresponds to substitutions [A] [B] true call -> [B] and [A] [B] false call -> [A]. Based on that a whole set of boolean operations can be defined:
| CC operator | Pattern | Substitution | BECC implementation |
|---|---|---|---|
true
|
[A] [B] true call
|
[B]
|
[[]>-]
|
false
|
[A] [B] false call
|
[A]
|
[[]-]
|
not
|
[A] not
|
[~A]
|
[[[]>-][[]-]]<+-+-
|
and
|
[A] [B] and
|
[A&B]
|
[[[[]-]]<+-]<+-+-
|
or
|
[A] [B] or
|
[A|B]
|
[[[]>-]]<+-+-
|
ifte
|
[A] [B] [C] ifte
|
if [A] then B else C
|
[]<<[]<<+-[+-]<+-+-+-
|
Natural numbers
Lambda Calculus Church encoding of natural numbers defines them as functions of two parameters returning the result of applying the first parameter to the second N times. In CC it would correspond for example to `[A] [B] 3 -> [A] B B B`, but since the second argument isn't actually modified in any way by the numbers they can be redefined as just calling their only argument N times:
| CC operator | Pattern | Substitution | BECC implementation |
|---|---|---|---|
0
|
[A] 0 call
|
Empty
|
[[]-]
|
1
|
[A] 1 call
|
A
|
[+-]
|
1+
|
[N] 1+
|
[N+1]
|
[[+<+-]<+-+-]>
|
+
|
[A] [B] +
|
[A+B]
|
[[[[+<+-]<+-+-]>]]<+-+-
|
1-
|
[A] 1-
|
[A-1]
|
[[[]-][[]-][[]>-+[[+<+-]<+-+-]>]]<+-+-[]-
|
-
|
[A] [B] -
|
[A-B]
|
[[[[[]-][[]-][[]>-+[[+<+-]<+-+-]>]]<+-+-[]-]]<+-+-
|
0=
|
[A] 0=
|
[A=0]
|
[[[]>-][[]-[[]-]]]<+-+-
|
0>
|
[A] 0>
|
[A>0]
|
[[[]-][[]-[[]>-]]]<+-+-
|
>
|
[A] [B] >
|
[A>B]
|
[[[[[]-][[]-][[]>-+[[+<+-]<+-+-]>]]<+-+-[]-]]<+-+-[[[]-][[]-[[]>-]]]<+-+-
|
Code examples
These examples assume that input and output numbers are Church-encoded according to the above explanation and read on EOF returns 0.
Y combinator
[[+>]<+-+-]>++-
Cat
A cat program writes its input directly to its output. Not to be confused with "cat" - a concatenation operator.
[ Pseudocode:
[ input dup output 0=
[ drop ] [ call ] ifte ] Y
][]-
[ , + . [[[]>-][[]-[[]-]]]<+-+-
[ []- ] [ +- ] []<<[]<<+-[+-]<+-+-+-
] [[+>]<+-+-]>++-
External resources
- Concatenative languages wiki - check out less pure but more usable concatenative languages
- Foundations of Dawn: Untyped Concatenative Calculus - the best formal explanation of CC I found on the internet
- The Theory of Concatenative Combinators - exploration of different combinators and their relation to lambda calculus by people who invented CC