Leftmost‑outermost means:
Reduce the redex whose λ appears first when scanning from left to right.
Real‑world analogy:
Imagine you have a list of tasks, and you always do the first task at the top before touching anything else.
Even if another task looks easier, you always start with the leftmost one.
Why it matters:
LMO is guaranteed to reach a normal form if one exists.
This is like always choosing the “safe path” that eventually finishes.
2. Rightmost‑Outermost Reduction (RMO)
Rightmost‑outermost means:
Reduce the redex whose λ is the last outermost one in the term.
Real‑world analogy:
You clean your room by starting with the item farthest from the door.
Sometimes this is faster, sometimes you get stuck in a loop.
Why it matters:
RMO can be shorter than LMO, but it may loop forever even when a normal form exists.
3. Head Reduction & Head Normal Form
Head reduction always reduces the head redex — the redex at the “front” of the term.
Real‑world analogy:
Think of a queue at a shop.
You always serve the person at the front first, even if people behind them have simple requests.
A term is in head normal form when the front is no longer reducible, even if the inside still contains redexes.
4. Call‑by‑Name
Call‑by‑name reduces the leftmost‑outermost redex but never reduces inside λ‑abstractions.
Analogy:
You only open a gift when you absolutely must.
If a function doesn’t need the argument, you never evaluate it.
5. Call‑by‑Value
Call‑by‑value reduces arguments before applying the function.
Arguments must be values (usually λ‑abstractions).
Analogy:
Before cooking a recipe, you prepare (evaluate) all ingredients first.
6. de Bruijn Indices
de Bruijn indices remove variable names and replace them with numbers representing how many λ’s you must pass to reach the binder.
Analogy:
Instead of calling people by name, you refer to them by how many seats away they are from you at a table.