Turing Complete

The Relision system is now Turing complete. This is a good thing, but there is a crazy amount of work left to do. Right now only the simplest matching is performed to allow somewhat trivial lambda expressions to work.

The screenshot is probably not that impressive. What is going on?

SKI Calculus

The SKI calculus consists of three operators.

• The identity: for any term x; Ix = x.
• The constant function generator: for any terms x,y; Kxy = x
• The substitution: for any terms x,y,z; Sxyz = (xz)(yz)

The SKI calculus is useful because it is relatively simple (it only has the above three rules) and because it is Turing complete. Thus any system that is powerful enough to implement the SKI calculus is also Turing complete.

Implementing the SKI calculus in Relision is (relatively) straightforward using single-argument lambdas.

• The identity: $x -> $x
• The constant function generator: $x -> $y -> $x
• The substitution operator: $x -> $y -> $z -> (($x.$z).($y.$z))

The Relision language provides lambdas that consist of two parts: a pattern and a body, joined by a lambda map symbol ->. When a lambda is applied to an argument (using the applicative dot), the pattern is matched against the argument, yielding (potentially) a set of bindings. These bindings are then applied to the lambda’s body, yielding the final result.

$x -> $x . 15
// Match $x against 15; the match succeeds with {bind $x=>15}.
// Apply this binding to the lambda body.
--> {bind $x=>15} . $x
--> 15

The lambda map is right-associative, so the constant function generator is really $x -> ($y -> $x). Here’s an example of how it creates constant functions.

$x -> $y -> $x . 21
// Match $x against 21; the match succeeds with {bind $x=>21}.
// Apply this binding to the lambda body.  Note that $x is not
// bound in the second lambda.
--> {bind $x=>21} . ($y -> $x)
--> $y -> 21

// This is a constant function; it always evaluates to 21.
$y -> 21 . 9
--> {bind $y=>9} . 21
--> 21

It turns out that in the SKI calculus SKK = I. We should be able to show that in Relision.

// SKK
// S = $x -> $y -> $z -> (($x.$z).($y.$z))
// K = $x -> $y -> $x
(($x -> $y -> $z -> (($x.$z).($y.$z))) . ($x -> $y -> $x)) . ($x -> $y -> $x)
//<------------- S ----------------->|   |<----- K ---->|    |<----- K ---->|
--> $z -> $z

If you look at the screenshot at the start of this post, you’ll see that Relision correctly handles this case. In fact, it handles many more; read up on the SKI calculus if you are interested.

Under the Hood

Variables that appear in a lambda pattern are rewritten to have a lambda index, and the lambda index of terms is computed based on this. It isn’t the same as a DeBruijn index, but it is really close and works well. Variables are no longer rewritten by name, per se, but by a UID that is computed for each variable name and lambda index. This makes matching during rewriting a constant time operation, whereas string comparison was not (necessarily).

One of the challenges of working in Rust is that you have to think very carefully about when and what data should be modifiable, who owns it, and how the compiler or runtime can know when to de-allocate it. The benefits are two: no garbage collection, and a cleaner and more deliberate design. Still, this puts a lot of cognitive burden on the programmer compared to, say, Python. Still, after I struggle through a particular part of the implementation I end up in a better place with a cleaner and simpler design. In short, I think the design of Relision is superior to the older Elision in many ways… and of course faster.

There is a roadmap to the first public release (1.0.0), and shockingly I am making really good progress on it. The only real challenge is getting access to my computer (I use my own computer for all development; my work computer is on the other side of the room and for paying work). My son has re-discovered the game “Slime Rancher.”