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. 2 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.