Syntax, Semantics & the Lambda Calculus

Concrete syntax is the textual representation that humans type: character strings governed by a grammar. Abstract syntax is the tree-shaped data structure (an Abstract Syntax Tree, or AST) that a parser produces after discarding all syntactic sugar, parentheses, and whitespace.

Think of concrete syntax as the sentence "3 + 4 * 2" and abstract syntax as the tree with + at the root, 3 as the left child, and * (with children 4 and 2) as the right child. The tree encodes precedence structurally rather than relying on convention. Every subsequent phase of a compiler or interpreter operates on the AST, not the raw string.

This separation matters because:

• The same abstract syntax can have multiple concrete syntaxes (Haskell and ML look different but share deep structural similarities).
• Transformations (optimization, type-checking, evaluation) are cleanly defined as functions on trees, not string manipulations.
• It makes the semantics of a language independent of its notation.

A grammar defines the concrete syntax; the AST type definition defines the abstract syntax. In a functional language, the AST is literally an algebraic data type:

-- Haskell: abstract syntax for a tiny arithmetic language
data Expr
  = Num  Int
  | Add  Expr Expr
  | Mul  Expr Expr
  | Var  String
  | Let  String Expr Expr   -- let x = e1 in e2

-- Concrete:  "let x = 3 + 4 in x * 2"
-- Abstract:  Let "x" (Add (Num 3) (Num 4)) (Mul (Var "x") (Num 2))

A formal grammar is a set of production rules that generates a language (a set of strings). The most common class used for programming languages is context-free grammars (CFGs), which sit in the second tier of the Chomsky hierarchy.

A CFG is a 4-tuple G = (V, Σ, R, S) where V is a set of non-terminal symbols, Σ is the alphabet of terminals, R is the set of production rules (each of the form A → α for a non-terminal A and string α over V∪Σ), and S is the start symbol.

Example: a minimal expression grammar in BNF:

E ::= E '+' T | T
T ::= T '*' F | F
F ::= '(' E ')' | num

The left-recursive structure encodes left-associativity. Parsing transforms a concrete token stream into an AST. Two dominant algorithms are recursive descent (top-down, easy to implement by hand, the basis of most hand-written parsers) and LR parsing (bottom-up, used by parser generators like yacc/bison).

Why context-free and not regular? Because nesting — balanced parentheses, nested blocks — cannot be recognized by a finite automaton. CFGs handle nesting naturally via recursive non-terminals.

Ambiguity is a cardinal sin in a programming language grammar: if a string has two parse trees, the language's meaning is undefined. Good language designers ensure their grammars are unambiguous, or they resolve ambiguity with explicit disambiguation rules (precedence, associativity).

# A tiny recursive descent parser in Python
# Grammar: E ::= T ('+' T)*    T ::= F ('*' F)*    F ::= num | '(' E ')'

class Parser:
    def __init__(self, tokens): self.tokens = tokens; self.pos = 0
    def peek(self): return self.tokens[self.pos] if self.pos < len(self.tokens) else None
    def consume(self, t): assert self.peek() == t; self.pos += 1

    def parse_E(self):
        left = self.parse_T()
        while self.peek() == '+':
            self.consume('+')
            left = ('Add', left, self.parse_T())
        return left

    def parse_T(self):
        left = self.parse_F()
        while self.peek() == '*':
            self.consume('*')
            left = ('Mul', left, self.parse_F())
        return left

    def parse_F(self):
        t = self.peek()
        if isinstance(t, int): self.pos += 1; return ('Num', t)
        self.consume('('); e = self.parse_E(); self.consume(')'); return e

Semantics is the meaning of a program — what it computes, what effects it has. There are three major styles:

1. Operational semantics: meaning is defined by a step-by-step evaluation relation on the AST. The most intuitive style and the one we use for the λ-calculus.
2. Denotational semantics: meaning is defined by a mathematical function mapping programs to values in some domain (e.g., a function in set theory).
3. Axiomatic semantics: meaning is defined by logical assertions (pre/postconditions) — the basis of formal verification (Hoare logic).

In small-step operational semantics (also called structural operational semantics, SOS), you define a relation e → e' ("expression e reduces to e' in one step") using inference rules. For our arithmetic language:

──────────────────── (E-ADD)
 n₁ + n₂ → n₁+n₂

    e₁ → e₁'
─────────────────── (E-ADDL)
 e₁ + e₂ → e₁' + e₂

The second rule says: to evaluate e₁ + e₂, first reduce the left subexpression. The order of the rules encodes evaluation order (left-to-right here).

In big-step operational semantics (natural semantics), you write e ⇓ v meaning "e evaluates to value v in (possibly many) steps." Big-step is more concise but harder to use for analyzing divergence and intermediate states.

For the λ-calculus, small-step semantics gives us a precise definition of what β-reduction means and in what order it proceeds, letting us reason carefully about termination, confluence, and equivalence.

The untyped lambda calculus (λ-calculus) has the following abstract syntax — the entirety of the language:

e ::= x           -- variable
    | λx. e       -- abstraction (function definition)
    | e₁ e₂       -- application (function call)

That is literally it. No numbers, no booleans, no conditionals, no recursion built in. Everything must be encoded.

Variables are names that refer to a binding site.

Abstraction λx. e creates an anonymous function with parameter x and body e. In Python this is lambda x: e; in Haskell \x -> e.

Application e₁ e₂ applies function e₁ to argument e₂. Application is left-associative: f g h means (f g) h.

Scope is lexical. In λx. (λy. x y), the x in the body refers to the outermost λx. A variable is bound if it occurs within the scope of a matching λ; otherwise it is free.

Formal definition of free variables FV(e):

• FV(x) = {x}
• FV(λx. e) = FV(e) \ {x} (binding x removes it from the free set)
• FV(e₁ e₂) = FV(e₁) ∪ FV(e₂)

A term with no free variables is called a combinator or a closed term. Combinators are the building blocks of combinator-based computation (SKI calculus).

Convention: λ binds as loosely as possible, so λx. f x y means λx. ((f x) y), NOT (λx. f x) y.

-- Some lambda terms written in Haskell notation (\x -> ...)
-- Identity function:  λx. x
id_fn = \x -> x

-- Constant function:  λx. λy. x  (returns first argument, ignores second)
const_fn = \x -> \y -> x

-- Self-application:   λx. x x
-- (not typeable in simply-typed λ-calculus, but valid in untyped)
self_app = \x -> x x   -- Haskell will actually reject this type-wise

-- Application example: (λx. x) (λy. y)
-- This is id applied to id, which should reduce to  λy. y

These are the three fundamental equational laws of the λ-calculus.

α-equivalence (α-conversion): Renaming a bound variable does not change the meaning of a term. λx. x is α-equivalent to λy. y — both are the identity function. Formally, λx. e =α λy. e[y/x] provided y is not free in e. This is like the fact that the mathematical function f(x) = x² and f(t) = t² are the same function.

β-reduction (β-reduction): This is the computation rule — the heart of the λ-calculus. Applying a function to an argument reduces by substituting the argument for the bound variable:

(λx. e₁) e₂ →β e₁[e₂/x]

where e₁[e₂/x] means "replace all free occurrences of x in e₁ with e₂."

Substitution must be capture-avoiding! A naive substitution can accidentally capture free variables. Consider (λx. λy. x) y. A naive substitution gives λy. y, which is wrong (the y we substituted got captured by the inner λy). The correct substitution renames the bound y first: (λx. λz. x) y →β λz. y. The rule: before substituting e₂ for x, rename any bound variables in e₁ that appear free in e₂.

η-conversion (eta): λx. f x =η f if x ∉ FV(f). This says that a function that just applies f to its argument is f. In Haskell, this is the motivation for point-free style: \x -> map f x is η-equivalent to map f.

A term is in β-normal form if no β-reduction is possible (no subterm of the form (λx. e₁) e₂ exists). Not every term has a normal form — (λx. x x)(λx. x x) (the Ω combinator) reduces to itself forever.

# Demonstrating beta reduction by hand (Python as notation, not execution)

# Term: (λx. λy. x + y) 3
# Step 1: beta-reduce outer application
#   substitute 3 for x in (λy. x + y)
#   = λy. 3 + y
# This is a partially applied function (currying!)

# Term: ((λx. λy. x + y) 3) 4
# Step 1: (λx. λy. x + y) 3 → λy. 3 + y
# Step 2: (λy. 3 + y) 4   → 3 + 4  =  7

# The Omega combinator: (λx. x x)(λx. x x)
# Let M = λx. x x
# M M  →β  (x x)[M/x]  =  M M   -- loops forever!
omega = (lambda x: x(x))(lambda x: x(x))  # RecursionError in Python

When a redex (λx. e₁) e₂ appears, β-reduction can be applied. But in a complex term there may be many redexes. The evaluation strategy dictates which one to reduce first.

Call-by-value (CBV) — the argument e₂ must be reduced to a value before the function is applied. This is what most languages (Python, C, Java, ML, Scheme) do. It is strict: the argument is always evaluated even if the function never uses it.

Call-by-name (CBN) — apply the function immediately, substituting the unevaluated argument expression. The argument may be evaluated multiple times (once per use) or not at all. This is the semantics of Algol 60's call-by-name and is related to how macros work.

Call-by-need (lazy evaluation) — like call-by-name, but the argument is evaluated at most once: the first time it is needed, and then the result is memoized (shared). This is what Haskell implements. It enables infinite data structures (like infinite lists) and elegant programs that would be impossible or inefficient in strict languages.

The Church-Rosser theorem guarantees that if a normal form exists, it will be found regardless of reduction order. But CBV may loop on terms that have a normal form (e.g., (λx. λy. y) Ω has normal form λy. y under CBN/lazy, but loops under CBV because Ω diverges).

In Haskell:

take 5 [1..]  -- works under lazy evaluation; [1..] is an infinite list

Under CBV semantics, this would require fully evaluating [1..] before passing it to take, which would loop forever.

-- Call-by-value vs call-by-need illustration in Haskell

-- Under lazy evaluation (call-by-need), Haskell can define:
ones :: [Int]
ones = 1 : ones   -- infinite list of 1s

fifthElement :: Int
fifthElement = ones !! 4   -- = 1; only 5 elements are ever evaluated

-- Also: lazy short-circuit (hypothetical strict language would evaluate both)
badDiv :: Int -> Int -> Bool
badDiv _ 0 = False   -- pattern match, never evaluates second branch
badDiv x y = x `mod` y == 0

Church encodings demonstrate the remarkable expressive power of the λ-calculus: we can represent data using functions. The key insight is that a value is characterized by what it does, not by what it is. A Boolean, for instance, is something that makes a binary choice — so we encode it as a function that takes two branches and picks one.

Church Booleans:

true  = λt. λf. t    -- takes two args, returns the first
false = λt. λf. f    -- takes two args, returns the second

Conditional:

if_then_else = λb. λx. λy. b x y

Applying: if_then_else true A B = (λb.λx.λy. b x y) true A B →* true A B = A. Correct!

Logical operators:

and = λp. λq. p q p     -- if p then q else p (=false)
or  = λp. λq. p p q     -- if p then p (=true) else q
not = λp. p false true

Verification that and true false = false:

and true false
= (λp. λq. p q p) true false
→  true false true
= (λt.λf. t) false true
→  false

This is not a trick or curiosity. It is the discovery that control flow is data. In a language like Haskell, the Bool type and if expression ultimately reduce to this structure in the mathematical semantics.

# Church booleans in Python (as pure lambdas)
true_  = lambda t: lambda f: t
false_ = lambda t: lambda f: f

if_then_else = lambda b: lambda x: lambda y: b(x)(y)
and_ = lambda p: lambda q: p(q)(p)
or_  = lambda p: lambda q: p(p)(q)
not_ = lambda p: p(false_)(true_)

# Convert Church bool to Python bool
to_bool = lambda b: b(True)(False)

print(to_bool(true_))                     # True
print(to_bool(and_(true_)(false_)))       # False
print(to_bool(or_(false_)(true_)))        # True
print(to_bool(not_(false_)))              # True

Church numerals encode natural numbers as iteration. The number n is represented as a function that applies its first argument n times to its second argument:

0 = λf. λx. x          -- apply f zero times
1 = λf. λx. f x        -- apply f once
2 = λf. λx. f (f x)    -- apply f twice
n = λf. λx. fⁿ x       -- apply f n times

This is the mathematical definition of a natural number via iteration — strikingly similar to Peano arithmetic's definition of n as "apply successor n times to zero."

Successor:

succ = λn. λf. λx. f (n f x)

succ n applies f one extra time.

Addition:

add = λm. λn. λf. λx. m f (n f x)

add m n applies f m times to the result of applying f n times to x — applying f m+n times total.

Multiplication:

mul = λm. λn. λf. m (n f)

Apply n f (which is "apply f n times") a total of m times — applying f m×n times.

Exponentiation is the most beautiful:

exp = λm. λn. n m

Apply the Church numeral m (which is an iteration function) n times — this is m^n.

Subtraction requires the predecessor function, which is notoriously tricky to define — it needs pairs (see next concept) and was a key challenge for Church's original development.

# Church numerals in Python
zero  = lambda f: lambda x: x
one   = lambda f: lambda x: f(x)
two   = lambda f: lambda x: f(f(x))
three = lambda f: lambda x: f(f(f(x)))

succ = lambda n: (lambda f: lambda x: f(n(f)(x)))
add  = lambda m: lambda n: (lambda f: lambda x: m(f)(n(f)(x)))
mul  = lambda m: lambda n: (lambda f: m(n(f)))
exp_ = lambda m: lambda n: n(m)   # m^n

# Convert Church numeral to Python int
to_int = lambda n: n(lambda x: x + 1)(0)

four = succ(three)
print(to_int(four))                      # 4
print(to_int(add(two)(three)))           # 5
print(to_int(mul(two)(three)))           # 6
print(to_int(exp_(two)(three)))          # 8  (2^3)

Church pairs encode a pair (a, b) as a function that, when given a selector, returns the appropriate element:

pair  = λx. λy. λs. s x y     -- construct a pair
fst   = λp. p (λx. λy. x)    -- select first element
snd   = λp. p (λx. λy. y)    -- select second element

Verification: fst (pair a b) = (λp. p true) ((λx.λy.λs. s x y) a b) →* true a b = a. ✓

Predecessor of a Church numeral uses a clever trick with pairs. The idea: slide a window of (n-1, n) pairs starting from (0, 0), applying the "shift" function n times, then take the first element:

shift = λp. pair (snd p) (succ (snd p))
pred  = λn. fst (n shift (pair zero zero))

After n applications of shift to (0, 0): we get (n-1, n). Taking fst gives n-1.

Subtraction: sub = λm. λn. n pred m (apply predecessor m times)

Booleans on numerals:

iszero = λn. n (λx. false) true

Applying (λx. false) even once gives false; applying it zero times leaves true. So iszero 0 = true, iszero (n+1) = false. ✓

Lists can be encoded as iterated pairs (or via a fold encoding). The Scott encoding (an alternative) maps constructors directly to continuations and is better for pattern matching.

# Church pairs and predecessor in Python
pair_ = lambda x: lambda y: lambda s: s(x)(y)
fst_  = lambda p: p(lambda x: lambda y: x)
snd_  = lambda p: p(lambda x: lambda y: y)

# Predecessor
succ_ = lambda n: (lambda f: lambda x: f(n(f)(x)))
shift = lambda p: pair_(snd_(p))(succ_(snd_(p)))
zero_ = lambda f: lambda x: x
pred_ = lambda n: fst_(n(shift)(pair_(zero_)(zero_)))

to_int = lambda n: n(lambda x: x + 1)(0)
one_  = succ_(zero_)
two_  = succ_(one_)
three_ = succ_(two_)

print(to_int(pred_(three_)))   # 2
print(to_int(pred_(one_)))     # 0  (predecessor of 0 = 0 in Church encoding)

In the λ-calculus, functions are anonymous — a function cannot call itself by name because it has no name. How then do we encode recursion?

The answer is the Y combinator (fixed-point combinator), one of the most beautiful results in theoretical computer science:

Y = λf. (λx. f (x x)) (λx. f (x x))

The key property: Y f = f (Y f) — i.e., Y f is a fixed point of f. If f is a function that takes "a continuation" representing recursive calls and returns the next step of the computation, then Y f is the recursive function itself.

Derivation that Y f = f (Y f):

Y f
= (λf. (λx. f(x x))(λx. f(x x))) f
→β  (λx. f(x x))(λx. f(x x))
→β  f ((λx. f(x x))(λx. f(x x)))
=   f (Y f)  ✓

In a call-by-value language, the naive Y combinator loops infinitely (because x x is evaluated before f is applied). The fix is the Z combinator (the CBV fixed-point combinator):

Z = λf. (λx. f (λv. x x v)) (λx. f (λv. x x v))

The η-expansion λv. x x v delays evaluation until v is provided.

In practice, real languages use letrec (recursive let) as a built-in construct that desugars to fixed points. But the Y combinator proves that recursion is not a primitive — it emerges from the three basic constructs of the λ-calculus.

# Y combinator (call-by-value / Z combinator) in Python
Z = lambda f: (lambda x: f(lambda v: x(x)(v)))(lambda x: f(lambda v: x(x)(v)))

# Factorial without any def or recursion
fact = Z(lambda self: lambda n: 1 if n == 0 else n * self(n - 1))

print(fact(5))   # 120
print(fact(10))  # 3628800

# Fibonacci
fib = Z(lambda self: lambda n: n if n <= 1 else self(n-1) + self(n-2))
print(fib(10))   # 55

One of the most important theoretical properties of the λ-calculus is confluence (also called the Church-Rosser property):

If a term e can be reduced in two different ways to terms e₁ and e₂, then there exists a term e' such that both e₁ and e₂ can be reduced to e'.

Diagrammatically (a "diamond"):

    e
   / \
  e₁  e₂
   \ /
    e'

This theorem (proved by Alonzo Church and J. Barkley Rosser in 1936) has two major corollaries:

1. Uniqueness of normal forms: If a term has a normal form, that normal form is unique (up to α-equivalence). Different evaluation orders may take different paths, but they cannot arrive at different answers.

2. Decidability of equality for normalizing terms: Two terms are equal if and only if they have the same normal form.

Confluence is a strong sanity check for a language's semantics: it means there is no ambiguity in what a program computes, even if the how varies.

Note: confluence does NOT mean all terms terminate. The Ω combinator (λx. x x)(λx. x x) has no normal form and diverges under every evaluation order. Adding normalization (every term reaches a normal form) would give us strong normalization, which is a property of the simply-typed λ-calculus (but not the untyped version).

The untyped λ-calculus is the mathematical core, but real functional languages add crucial layers:

Types: The simply-typed λ-calculus (STLC) adds a type system that rejects non-terminating programs (like Ω) at the cost of expressiveness. The System F (polymorphic λ-calculus) adds universal quantification over types, enabling parametric polymorphism (forall a. a -> a). Hindley-Milner type inference (used in Haskell, ML, OCaml) automatically infers the principal type of every expression without type annotations, using a unification algorithm.

Algebraic Data Types (ADTs): Pattern matching on sum types (tagged unions) is the functional analogue of if/else and switch. In the λ-calculus, this is Church/Scott encoding; in a real language it is a built-in construct that compiles down to it.

Syntactic sugar: Haskell's do notation is syntactic sugar for monadic bind (>>=), which is itself modeled by the Kleisli category structure on monads — a concept from category theory. The where clause, list comprehensions, and record syntax are all surface-level conveniences that desugar to core λ-calculus with ADTs.

Currying: Every multi-argument function in Haskell is actually a chain of single-argument λ-abstractions. f :: Int -> Int -> Int means f :: Int -> (Int -> Int). This is not a limitation — it is a feature enabling partial application and higher-order programming for free.

The Curry-Howard Correspondence: Types are propositions, programs are proofs, type-checking is proof verification. A -> B is logical implication. A function of type A -> B is a proof that A implies B. This profound connection means that a type-correct functional program is a constructive mathematical proof.

-- Haskell showing the continuum from lambda calculus to real code

-- Pure lambda calculus style (curried, higher-order)
apply :: (a -> b) -> a -> b
apply f x = f x

-- Currying: these are identical
add1 :: Int -> Int -> Int
add1 x y = x + y

add2 :: Int -> (Int -> Int)
add2 = \x -> (\y -> x + y)   -- explicit lambda, identical semantics

-- Partial application (enabled by currying)
add5 :: Int -> Int
add5 = add1 5   -- partially apply, get a new function

-- Higher-order function (map is λf. λxs. ...)
doubles :: [Int] -> [Int]
doubles = map (* 2)   -- point-free, eta-reduced