5.2.1. Types🔗

5.2.2. Terms🔗

We need some notation magic to set up the concrete syntax, as we did in the Types chapter...

The upshot of this section is that STLC types and terms are both written inside one pair of brackets, <{ … }>, and that ~e inside the brackets escapes back to an arbitrary Lean expression:

• <{ Bool → Bool }> is a type;

• <{ λ x : Bool . x }> is a term — a bare identifier inside the brackets is the object-language variable of that name, so <{ x }> is the variable x;

• <{ ~t₁ ~t₂ }> applies one Lean-level term to another.

Lean works out from context which of the two a given bracket holds, so the same brackets serve for types, for terms, and — when we come to typing — for typing judgments too. How that works is in the collapsed blocks below; nothing later in the chapter depends on it.

We'll write types inside of <{ ... }> brackets:

A few checks that the grammar parses the way it should — application associating to the left, conditionals nesting without parentheses, and ~ escaping to Lean:

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.

The example terms named above are all abstractions, hence all values. We record that once each, so that the reduction examples can cite the fact by name instead of unfolding the definition again at every use.

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:

As we did for the evaluators in the Slang chapter, we pair the definition with one simplification lemma per constructor, saying how subst behaves on that constructor. The variable and abstraction cases each need two lemmas, since substitution treats a bound name differently depending on whether it is the name being substituted for.

Checks that the substitution notation parses and nests as intended.

[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🔗

The small-step reduction relation for STLC now follows the same pattern as the ones we have seen before. Intuitively, to reduce a function application, we first reduce its left-hand side (the function) until it becomes an abstraction; then we reduce its right-hand side (the argument) until it is also a value; and finally we substitute the argument for the bound variable in the body of the abstraction. This last rule, written informally as

(λx:T. t₁₂) v₂ ⟶ [x:=v₂] t₁₂

is traditionally called beta-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:

                  --------------------------------                (ifTrue)
                   (if true then t₁ else t₂) ⟶ t₁

                  ---------------------------------               (ifFalse)
                   (if false then t₁ else t₂) ⟶ t₂

                              t₁ ⟶ t₁'
        ----------------------------------------------------      (ifStep)
         (if t₁ then t₂ else t₃) ⟶ (if t₁' then t₂ else t₃)

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.

Formally:

As in the Smallstep chapter, ⟶* is the multi-step closure of ⟶ — that is, Multi applied to this chapter's step relation. We inherit its reflexivity lemma along with it, so a zero-step execution goal t ⟶* t is closed by rfl.

(λ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.