Concise Specification Maybe the shortest turing-complete PL spec of all times
Abstract Syntax
Expr ::= 'u' | Expr Expr
We write expressions using parentheses where necessary (assuming left-associativity), for example u u (u u u)
.
Abstract Semantics
An expressions may be reducible to another expression, otherwise (if irreduible) we also call it a value.
Expressions are equal (=
) exactly if they reduce to the same value or reduction does not terminate for either expression.
Reduction
Extend Expr
with two new abstract expressions s
and k
.
Apply the following rewrite rules as long as possible.
u α ⟶ α s k
k α β ⟶ α
s α β γ ⟶ α γ (β γ)
Observability
Given an expression ■
, we define ⟦■⟧
as
⟦■⟧ = argmin n
(n, i, a) ∈ S
where S = { (n, i, a) ∈ ℕ × ℕ₀ × ℕ₀
| ∀ α₀, ..., αₙ :
∃ β₁, ..., βₐ :
■ α₀ ... αₙ = αᵢ β₁ ... βₐ }
An implementation may assume that it is only asked to compute ⟦■⟧
if it is defined.
Concrete Syntax
The notation used so far is not succinct since multiple copies of identical subexpressions need to be written out.
We hence introduce a let binding syntax, like in Haskell or OCaml.
In case of name collisions, inner definitions hide outer ones.
The expression u u (u u u)
could be written as let i = u u in i (i u)
.
However, since Lambada is aimed towards ease of implementation, simplicity and minimalism, this will not be our concrete syntax.
Instead, we linearize the notation and allow any non-empty sequences of non-whitespace Unicode characters as names.
The only predefined (but not reserved!) name is “u”, which represents expression u
.
Grammar
Terminator ::= ' ' -- space 0x20
Define ::= '\n' -- newline 0x0A
Name ::= \S+
Expression ::= α:Name Terminator -- Case: α (name)
| β:Expression γ:Expression Terminator -- Case: β γ (application)
| β:Expression α:Name Define γ:Expression -- Case: let α = β in γ