Anemone
Anemone is an implemented (see talk page), Turing-complete (see proof) language by User:Afarnen which builds upon combinatory logic, pattern recognition, algebraic data types, and similar concepts.
Syntax, semantics
The syntax of a term (expression):
- If a is an atom, then 'a' is a term. Atoms are the basic units of a term.
- If X and Y are terms, then '(X Y)' is a term. This is called "application". Here X is applied to Y.
Application is left-associative, so '(X Y) Z' can be written as 'X Y Z'.
However, reduction of terms has not been defined. There is no "abstraction" as there is in the Lambda Calculus--instead, a program is made up of a series of "reduction rules" which take the form:
<rule> ::= <left-term> '=' <right-term> '.'
which reads as "<left-term> reduces to <right-term>." A single step of computation is a single reduction according to one such rule. The reduction strategy is call-by-value, where the outer-most reducible term is reduced.
Rules are applied (attempted to be applied) in the order they are written (left->right), unlike languages such as Thue in which this is non-deterministic.
Unlike a Matrioshka language, you do not actually define, in the program, the initial term which is to be reduced. Instead, an interactive interpreter repeatedly asks the user for a term, which is printed back to the user after being reduced according to the loaded program(s).
A simple example
For example, one way to write Boolean AND and OR is:
and t t = t. and t f = f. and f t = f. and f f = f. or t t = t. or t f = t. or f t = t. or f f = f.
Variables
We employ "variables" in our reduction rules as wild cards to take the place of a single term. For instance, we can shorten our implementations of Boolean AND and OR, and even make them short-circuit:
and t X = X. and f X = f. or t X = t. or f X = X.
To distinguish atoms from variables, a variable must start with an uppercase, and an atom must not. Neither atoms nor variable names may include white-space, equals signs, periods, or parentheses.
Equal terms, order of rules
The following defines the predicate "equals":
eq X X = t. eq X Y = f.
This works because the first rule uses the same variable name twice, meaning that eq must be applied to two equivalent terms.
Also, the order in which the rules are written is important. If we changed the order of these two rules, "equals" would always return false, which isn't correct. For this reason, rules will typically be written in the order more specific->less specific.
Examples
This section includes implementations of common calculi, data types and functions, as well as example "test runs" which show how a term would reduce given a set of rules.
SKI combinator calculus
The following is a complete implementation of SKI combinator calculus, which is Turing-complete.
s X Y Z = X Z (Y Z). k X Y = X. i X = X.
Test runs
Self application:
(s i i) a i a (i a) a (i a) a a
Reversal:
(s (k (s i)) k) a b (k (s i)) a (k a) b (s i) (k a) b i b ((k a) b) b ((k a) b) b a
B, C, K, W
b X Y Z = X (Y Z) c X Y Z = X Z Y k X Y = X w X Y = X Y Y
cons, car, cdr, map
The following implements cons, written 'cons X Y', and the related functions car, cdr and map. Map recursively applies a given term to every leaf in a binary tree (cons).
car (cons X Y) = X. cdr (cons X Y) = Y. map T (cons X Y) = cons (map T X) (map T Y). map T X = T X.
Test runs
Get the third element out of a list:
car (cdr (cdr (cons a (cons b (cons c (cons d (cons e))))))) car (cdr (cons b (cons c (cons d (cons e))))) car (cons c (cons d (cons e))) c
Boolean NOT every element in a list:
map not (cons t (cons f (cons t (cons t f)))) cons (map not t) (map not (cons f (cons t (cons t f)))) cons (not t) (map not (cons f (cons t (cons t f)))) cons f (map not (cons f (cons t (cons t f)))) cons f (cons (map not f) (map not (cons t (cons t f)))) cons f (cons (not f) (map not (cons t (cons t f)))) cons f (cons t (map not (cons t (cons t f)))) cons f (cons t (cons (map not t) (map not (cons t f)))) cons f (cons t (cons (not t) (map not (cons t f)))) cons f (cons t (cons f (map not (cons t f)))) cons f (cons t (cons f (cons (map not t) (map not f)))) cons f (cons t (cons f (cons (not t) (map not f)))) cons f (cons t (cons f (cons f (map not f)))) cons f (cons t (cons f (cons f (not f)))) cons f (cons t (cons f (cons f t)))
Natural numbers and common functions
The following program is the natural numbers, as well as some common functions on them.
+ X 0 = X. + X (s Y) = s (+ X Y). * X 0 = 0. * X (s Y) = + X (* X Y). fib 0 = s 0. fib (s 0) = s 0. fib (s (s X)) = + (fib (s X)) (fib X). fact 0 = s 0. fact (s X) = * (s X) (fact X).
Test runs
The sixth Fibonacci number:
fib (s (s (s (s (s 0))))) + (fib (s (s (s (s 0))))) (fib (s (s (s 0)))) + (+ (fib (s (s (s 0)))) (fib (s (s 0)))) (fib (s (s (s 0)))) + (+ (fib (s (s (s 0)))) (fib (s (s 0)))) (+ (fib (s (s 0))) (fib (s 0))) + (+ (+ (fib (s (s 0))) (fib (s 0))) (fib (s (s 0)))) (+ (fib (s (s 0))) (fib (s 0))) + (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (+ (fib (s (s 0))) (fib (s 0))) + (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (+ (+ (fib (s 0)) (fib 0)) (fib (s 0))) + (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (+ (+ (fib (s 0)) (fib 0)) (s 0)) + (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (s (+ (+ (fib (s 0)) (fib 0)) 0)) s (+ (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (+ (+ (fib (s 0)) (fib 0)) 0)) s (+ (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (+ (fib (s 0)) (fib 0))) s (+ (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (+ (s 0) (fib 0))) s (+ (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (+ (s 0) (s 0))) s (+ (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (s (+ (s 0) 0))) s (s (+ (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (+ (s 0) 0))) s (s (+ (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) (s 0))) s (s (s (+ (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))) 0))) s (s (s (+ (+ (fib (s (s 0))) (fib (s 0))) (+ (fib (s 0)) (fib 0))))) s (s (s (+ (+ (+ (fib (s 0)) (fib 0)) (fib (s 0))) (+ (fib (s 0)) (fib 0))))) s (s (s (+ (+ (+ (fib (s 0)) (fib 0)) (s 0)) (+ (fib (s 0)) (fib 0))))) s (s (s (+ (s (+ (+ (fib (s 0)) (fib 0)) 0)) (+ (fib (s 0)) (fib 0))))) s (s (s (+ (s (+ (fib (s 0)) (fib 0))) (+ (fib (s 0)) (fib 0))))) s (s (s (+ (s (+ (fib (s 0)) (fib 0))) (+ (s 0) (fib 0))))) s (s (s (+ (s (+ (fib (s 0)) (fib 0))) (+ (s 0) (s 0))))) s (s (s (+ (s (+ (fib (s 0)) (fib 0))) (s (+ (s 0) 0))))) s (s (s (s (+ (s (+ (fib (s 0)) (fib 0))) (+ (s 0) 0))))) s (s (s (s (+ (s (+ (fib (s 0)) (fib 0))) (s 0))))) s (s (s (s (s (+ (s (+ (fib (s 0)) (fib 0))) 0))))) s (s (s (s (s (s (+ (fib (s 0)) (fib 0))))))) s (s (s (s (s (s (+ (s 0) (fib 0))))))) s (s (s (s (s (s (+ (s 0) (s 0))))))) s (s (s (s (s (s (s (+ (s 0) 0))))))) s (s (s (s (s (s (s (s 0)))))))
The factorial of three:
fact (s (s (s 0))) * (s (s (s 0))) (fact (s (s 0))) * (s (s (s 0))) (* (s (s 0)) (fact (s 0))) * (s (s (s 0))) (* (s (s 0)) (* (s 0) (fact 0))) * (s (s (s 0))) (* (s (s 0)) (* (s 0) (s 0))) * (s (s (s 0))) (* (s (s 0)) (+ (s 0) (* (s 0) 0))) * (s (s (s 0))) (* (s (s 0)) (+ (s 0) 0)) * (s (s (s 0))) (* (s (s 0)) (s 0)) * (s (s (s 0))) (+ (s (s 0)) (* (s (s 0)) 0)) * (s (s (s 0))) (+ (s (s 0)) 0) * (s (s (s 0))) (s (s 0)) + (s (s (s 0))) (* (s (s (s 0))) (s 0)) + (s (s (s 0))) (+ (s (s (s 0))) (* (s (s (s 0))) 0)) + (s (s (s 0))) (+ (s (s (s 0))) 0) + (s (s (s 0))) (s (s (s 0))) s (+ (s (s (s 0))) (s (s 0))) s (s (+ (s (s (s 0))) (s 0))) s (s (s (+ (s (s (s 0))) 0))) s (s (s (s (s (s 0)))))