Brainfuck Encoded Concatenative Calculus

From Esolang
Jump to navigation Jump to search
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

Retrieved from "https://esolangs.org/w/index.php?title=Brainfuck_Encoded_Concatenative_Calculus&oldid=124017"