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.
==See also==
* Binary lambda calculus
==External resources==
* Official Introduction to the LAST programming language, including a simple playground.
Category:Languages
Category:Functional paradigm
Category:Implemented
Category:Low-level
Category:2022
Category:Turing tarpits
Category:Turing complete