Brainfuck Encoded Concatenative Calculus
Paradigm(s)  Concatenative 

Designed by  User:Olus2000 
Appeared in  2022 
Memory system  Expression rewriting 
Computational class  Turingcomplete 
Major implementations  Canonical 
Influenced by  Brainfuck Concatenative Calculus 
File extension(s)  .txt 
Brainfuck Encoded Concatenative Calculus (BECC, pronounced [beck]) is a minimalistic programming language based on Concatenative Calculus. It keeps brainfuck's eight singlecharacter 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 Churchencoded number at a time.
Computational class
BECC is Turingcomplete because it is a variant of Concatenative Calculus which is Turingcomplete. 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 [[[A] [B]] + [+] <++] + cons rule; call is executed on the result of cat [[[A] [B]] + [+] <++] [[A] [B] + [+] <++]  dup rule [[A] [B]] + [+] <++ k rule [[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] true call

[A]

[[]]

not

[A] not

[~A]

[[[]>][[]]]<++

and

[A] [B] and

[A&B]

[[[[]]]<+]<++

or

[A] [B] or

[AB]

[[[]>]]<++

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

[A1]

[[[]][[]][[]>+[[+<+]<++]>]]<++[]



[A] [B] 

[AB]

[[[[[]][[]][[]>+[[+<+]<++]>]]<++[]]]<++

0=

[A] 0=

[A=0]

[[[]>][[][[]]]]<++

0>

[A] 0>

[A>0]

[[[]][[][[]>]]]<++

>

[A] [B] >

[A>B]

[[[[[]][[]][[]>+[[+<+]<++]>]]<++[]]]<++[[[]][[][[]>]]]<++

Code examples
These examples assumes that input and output numbers are Churchencoded 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