# 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 γ
```