LAST
LAST is an elegant encoding for lambda calculus which uses no explicit variables or indices and only 4 symbols: L, A, S, and T.
It is inspired by Binary lambda calculus and has a binary variant, called LAST-B, which has a BLC-style self-interpreter only 194 bits long.
LAST features S-optimization which is a novel form of expression reduction and equivalence, not possible in other variants of lambda calculus.
Syntax
The formal grammar of the language is as follows (in ABNF):
Term = "L" Term / "A" Term Term / "S" Term / "T"
Semantics
The semantics are defined by the LAST machine, which is a slightly simplified Krivine machine. The difference is that instead of using de Bruijn indices, the machine uses two simple (albeit more powerful) terms: S and T.
T is equivalent to 0 and S is equivalent to the successor function.
In other words, indices can be translated into LAST as follows:
- The index 0 is translated into T
- An index n + 1 is translated to S followed by a translation of index n
Meaning an index n is n repetitions of S followed by a T. For example:
index in BLC in LAST 0 10 T 1 110 ST 2 1110 SST 3 11110 SSST 4 111110 SSSST 5 1111110 SSSSST
This shows that the LAST machine can fully emulate the Krivine machine.
However the Krivine machine cannot fully emulate the LAST machine, as S can also precede L and A (semantics explained in S-optimization).
In effect, all programs in BLC can be translated to LAST, but not vice versa.
Therefore LAST can be seen as a superset of lambda calculus with de Bruijn indices.
S-optimization
LAST introduces the notion of S-optimization which is a kind of optimization that can turn some programs into shorter and more efficient equivalents.
The ability to encode these more efficient equivalents is unique to LAST.
Here is a basic example of S-optimization:
; the following lambda calculus term λx.λy.λz.x x x x ; can be encoded in LAST as: LLLAAASSTSSTSSTSST ; and S-optimized into a more efficient equivalent: LLLSSAAATTTT
BLC-style I/O
If we consider the symbols L, A, S, T to be digits, a LAST program is a number in quaternary.
LAST supports I/O similarly to BLC, except input and output in are strings of quaternary digits rather than bits.
For example the following LAST program:
LTLALALA
will output LALALA.
LAST-B
LAST can be translated to a binary variant called LAST-B by trivial mapping:
L -> 00 A -> 01 S -> 10 T -> 11
194-bit self-interpreter
A BLC-style self-interpreter for LAST is 97 characters:
ALATTLALLLATSLAAAATSASTLASTLLASSTLAATSTSSTSASTLASS TLASSTLAASSTTASTTSASTLASTLASTATLLTSATLATLLSTATT
This can be encoded in binary as:
01000111110001000000011110000101010111100110110001 10110000011010110001011110111010111001101100011010 11000110101100010110101111011011111001101100011011 00011011011100001110011100011100001011011111
That's 194 bits. 12 bits less than the original BLC self-interpreter.