5.2.1. Types🔗

5.2.2. Terms🔗

The constructors above give us a precise representation of STLC syntax, but expressions written directly with them quickly become hard to read. We need some notation magic to set up the concrete syntax, as we did in the Types chapter...

We will write STLC syntax inside <{ ... }> brackets. For example, <{ λ X : Bool . X }> represents the term Tm.abs "X" Ty.bool (Tm.var "X").

We write STLC syntax inside <{ ... }> brackets. Capital Latin names are literal STLC names. Lowercase and Greek names refer to Lean variables in the surrounding proof. Larger Lean expressions are inserted with ~.

Here are the terms we will use as running examples, written in the new notation:

Note that an abstraction λ x : T . t (formally, Tm.abs applied to x, T, and t) is always annotated with the type T of its parameter, in contrast to Lean (and other functional languages like ML, Haskell, etc.), which use type inference to fill in missing annotations. We're not considering type inference at all here.

5.3.1. Values🔗

To define the values of the STLC, we have a few cases to consider.

First, for the boolean part of the language, the situation is clear: true and false are the only values. An if expression is never a value.

Second, an application is not a value: it represents a function being invoked on some argument, which clearly still has work left to do.

Third, for abstractions, we have a choice:

• We can say that λx:T. t is a value only when t is a value — i.e., only if the function's body has been reduced (as much as it can be without knowing what argument it is going to be applied to).

• Or we can say that λx:T. t is always a value, no matter whether t is one or not — in other words, we can say that reduction stops at abstractions.

Our usual way of evaluating expressions in Lean makes the first choice — for example,

yields:

fun _x => 7

But Lean is rather unusual in this respect. Most functional programming languages make the second choice — reduction of a function's body only begins when the function is actually applied to an argument.

We also make the second choice here.

5.3.2. STLC Programs🔗

Finally, we must consider what constitutes a complete program.

Intuitively, a "complete program" must not refer to any undefined variables. We'll see shortly how to define the free variables in a STLC term. A complete program, then, is one that is closed — that is, that contains no free variables.

(Conversely, a term that may contain free variables is often called an open term.)

Having made the choice not to reduce under abstractions, we don't need to worry about whether variables are values, since we'll always be reducing programs "from the outside in," and that means the step relation will always be working with closed terms.

5.3.3. Substitution🔗

Now we come to the heart of the STLC: the operation of substituting one term for a variable in another term. This operation is used below to define the operational semantics of function application, where we will need to substitute the argument term for the function parameter in the function's body. For example, we reduce

(λX:Bool. if X then true else X) false

to

if false then true else false

by substituting false for the parameter X in the body of the function.

In general, we need to be able to substitute some given term s for occurrences of some variable x in another term t. Informally, this is written [x:=s]t and pronounced "substitute s for x in t."

Here are some examples:

• [X:=true] (if X then true else false) yields if true then true else false

• [X:=true] X yields true

• [X:=true] (if X then X else Y) yields if true then true else Y

• [X:=true] Y yields Y

• [X:=true] false yields false (vacuous substitution)

• [X:=true] (λY:Bool. if Y then X else false) yields λY:Bool. if Y then true else false

• [X:=true] (λY:Bool. X) yields λY:Bool. true

• [X:=true] (λY:Bool. Y) yields λY:Bool. Y

• [X:=true] (λX:Bool. X) yields λX:Bool. X

The last example is illuminating: substituting X with true in λX:Bool. X does not yield λX:Bool. true! The reason for this is that the X in the body of λX:Bool. X is bound by the abstraction: it is a new, local name that just happens to be spelled the same as some global name X.

Here is the definition, informally...

[x:=s]x               = s
[x:=s]y               = y                     if x ≠ y
[x:=s](λx:T. t)       = λx:T. t
[x:=s](λy:T. t)       = λy:T. [x:=s]t         if x ≠ y
[x:=s](t₁ t₂)         = ([x:=s]t₁) ([x:=s]t₂)
[x:=s]true            = true
[x:=s]false           = false
[x:=s](if t₁ then t₂ else t₃) =
                if [x:=s]t₁ then [x:=s]t₂ else [x:=s]t₃

... and formally:

[X:=s](λY:T₁. X (λX:T₂. X))

Technical note: Substitution becomes trickier to define if we consider the case where s, the term being substituted for a variable in some other term, may itself contain free variables. We say that s is an open term.

Here is an example. Using the above definition to substitute the open term

s = λX:Bool. R

(where R is a free reference to some global resource) for the free variable Z in the term

t = λR:Bool. Z

where R is a bound variable, we would get

λR:Bool. λX:Bool. R

where the free reference to R in s has been "captured" by the binder at the beginning of t.

Why would this be bad? Because it violates the principle that the names of bound variables do not matter. For example, if we rename the bound variable in t, e.g., let

t' = λW:Bool. Z

then [Z:=s]t' is

λW:Bool. λX:Bool. R

which does not behave the same as the substituting in the original t:

[Z:=s]t = λR:Bool. λX:Bool. R

That is, renaming a bound variable in t would change how t behaves under our simple substitution. So substitution gets more complicated in that setting, but fortunately we don't have that problem in our STLC variant.

Fortunately, since we are only interested here in defining the step relation on closed terms (i.e., terms like λX:Bool. X that include binders for all of the variables they mention), we can sidestep this extra complexity, but it must be dealt with when formalizing richer languages.

5.3.4. Reduction🔗

                              v.IsValue
                       -----------------------      (appAbs)
                        (λx:T. t) v ⟶ [x:=v]t

                              t₁ ⟶ t₁'
                          ----------------          (app1)
                           t₁ t₂ ⟶ t₁' t₂

                              v.IsValue
                              t₂ ⟶ t₂'
                          ----------------          (app2)
                           v₁ t₂ ⟶ v₁ t₂'

(plus the usual rules for conditionals).

The appAbs rule is often called beta-reduction.

This is call by value reduction: to reduce an application (t₁ t₂), we

• first reduce t₁ to a value: a function λx:T. t

• then reduce the argument t₂ to a value v

• then reduce the application itself by substituting v for the bound variable x in the body t.

(λX:Bool → Bool. X) (λX:Bool. X) ⟶ ???

(λX:Bool → Bool. X)
    ((λX:Bool → Bool. X) (λX:Bool. X))
⟶ ???

(λX:Bool → Bool. X) notB true  ⟶* ???

(λX:Bool. X) (notB true) ⟶* ???

5.3.5. Examples🔗

Example:

(λX:Bool → Bool. X) (λX:Bool. X) ⟶* λX:Bool. X

i.e.,

idBB idB ⟶* idB

Example:

(λX:Bool → Bool. X) ((λX:Bool → Bool. X) (λX:Bool. X))
      ⟶* λX:Bool. X

i.e.,

(idBB (idBB idB)) ⟶* idB.

Example:

(λX:Bool → Bool. X)
   (λX:Bool. if X then false else true)
   true
      ⟶* false

i.e.,

(idBB notB) true ⟶* false.

Example:

(λX:Bool → Bool. X)
   ((λX:Bool. if X then false else true) true)
      ⟶* false

i.e.,

idBB (notB true) ⟶* false.

(Note that this term doesn't actually typecheck; even so, we can ask how it reduces.)