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").

This notation must also support definitions and proofs about arbitrary piece of STLC syntax. For example, a theorem may introduce Lean variables t : Tm and τ : Ty, representing an arbitrary STLC term and type. Inside the brackets, we can then write <{ λ X : τ . t }>. Here X is the name of a variable in the STLC term being represented, while τ and t refer to the Lean variables in the surrounding theorem.

The notation distinguishes these two uses by naming convention, which we will follow throughout the STLC chapters:

• A name beginning with a capital Latin letter is taken literally as a name in the STLC syntax. Thus X, Y, and Z are STLC term variables. Such a name must be a single Lean identifier and cannot contain a dot. In languages with named base types, which we will see in the Sub chapter, names such as A, Int, and Bool name those types.

• A name beginning with a lowercase letter or a Greek letter refers to a Lean variable in the surrounding definition or proof. This lets us use the usual names x and y for strings, t and u for terms, τ for types, and Γ for contexts without additional punctuation.

• To insert a larger Lean expression, prefix it with ~. For example, <{ ~(Tm.var "X") t }> inserts the expression Tm.var "X" as the function and the Lean variable t as its argument. The same escape is needed to insert a capitalized Lean variable, since an unescaped capitalized name is assumed to be an STLC name.

This capitalization convention applies to actual variable names in concrete STLC examples and inside <{ ... }> brackets. In grammars, inference rules, and general explanations, symbols such as x, t, and T instead stand for an arbitrary variable name, term, or type. We keep the conventional lowercase notation for these schematic symbols.

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:

Note that due to an unfortunate limitation of Lean's notation system, we must use constructor names for match statements rather than our custom syntax.

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.

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

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.)