Lambda Syntax

Advanced Logic Notation

λ-calculus has a grammar small enough to fit on a stamp — but it reads nothing like school algebra at first. This page is the phrasebook.

The grammar, whole

Every legal λ-term is one of those three things, built from smaller λ-terms. Nothing else exists.

Reading an abstraction

The λ ends at a dot: λx.M means the body is everything after the dot. So λx.x y is a function whose body is x y — it is not (λx.x) y.

Application hugs left

When applications chain, they group to the left:

So λf.λx.f (f x) means: a function of f that gives a function of x that applies f twice — written with no extra ink.

Currying: functions that take one thing

λ-calculus has no multi-argument functions. It doesn't need them — a function can return a function:

This trick — one argument per function, nested λs for more — is called currying, after Haskell Curry. Two placeholders, one at a time.

See the structure

Every λ-term is a tree: λ nodes bind a variable, @ nodes apply, and leaves are variables. Here's (λx.λy.x) a b:

Free vs bound

Inside λx.M, every x in M is bound — owned by that λ. A variable with no λ owning it is free. In λx.x y: x is bound, y is free — it floats in from whoever wrote the term. Free variables are the inputs; bound variables are the machine's moving parts. This matters enormously on the next page, when substitution arrives.

AdaLogic BASIC is kept by the ALB team — a family-friendly site for learning and sharing programs. Guidelines · Privacy · Terms · Trademarks · AI disclosure · Contact · Giants · Technology · IDE.