4.1.1. Syntax🔗

Here is the syntax of program terms, informally:

And here it is formally:

4.1.2. Operational Semantics🔗

Here is the single-step relation, informally.

                   -----------------------------                 (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₃

                              t₁ ⟶ t₁'
                         -------------------                     (succStep)
                         succ t₁ ⟶ succ t₁'

                           -----------                           (predZero)
                           pred 0 ⟶ 0

                            IsNValue v
                        ------------------                       (predSucc)
                        pred (succ v) ⟶ v

                              t₁ ⟶ t₁'
                         -------------------                     (predStep)
                         pred t₁ ⟶ pred t₁'

                          ----------------                       (isZeroZero)
                          iszero 0 ⟶ true

                             IsNValue v
                      ------------------------                   (isZeroSucc)
                      iszero (succ v) ⟶ false

                              t₁ ⟶ t₁'
                       -----------------------                   (isZeroStep)
                       iszero t₁ ⟶ iszero t₁'

The formal rules are below. We are defining them differently than we have previously: We are using the relation's own notation (⟶) inside the constructors. We achieve this by defining Tm.Step within a section, and within that section using set_option hygiene false on ⟶ so that the constructors read in this syntax; after the section closes, we use a scoped notation as we have done before.

The Tm.IsNValue premises in predSucc and isZeroSucc are needed for determinism (this will be proved in an optional exercise below).

Notice that the Tm.Step relation doesn't care about whether the expression being stepped makes global sense — it just checks that the operation in the next reduction step is being applied to the right kinds of operands. For example, the term succ true cannot take a step, but the almost as obviously nonsensical term

succ (if true then true else true)

can take a step (once, before becoming stuck).

4.1.3. Normal Forms and Values🔗

The first interesting thing to notice about this Tm.Step relation is that the strong progress theorem from the Smallstep chapter fails here. That is, there are terms that are normal forms (they can't take a step) but not values (they are not included in our definition of possible "results of reduction").

Such terms are stuck.

However, although values and normal forms are not the same in this language, the set of values is a subset of the set of normal forms.

This is important because it shows we did not accidentally define things so that some value could still take a step.

iszero (if true then (succ 0) else 0)

if (succ 0) then true else false

succ (succ 0)

succ (if true then true else true)

Optional aside, good practice with step relations but tangential to the main development. We define an alternate step relation ⇢ and a step function for it.

Suppose we define an alternate single-step relation, written t ⇢ t', that drops the Tm.IsNValue premise from the predSucc and isZeroSucc rules — so pred (succ t) and iszero (succ t) may step even when t is not a numeric value. (It is built with exactly the same notation setup as Tm.Step; note predSucc/isZeroSucc no longer take a premise.)

Some questions about this relation (answers inline):

• Is ⇢ deterministic (∀ t t' t'', t ⇢ t' → t ⇢ t'' → t' = t'')? No: pred (succ (pred 0)) steps to both pred 0 (by predSucc) and pred (succ 0) (by predStep, since pred 0 ⇢ 0).

• Is every Tm.Step normal form also a ⇢ normal form? No: pred (succ true) is stuck for Tm.Step but steps under ⇢ (to true, by predSucc, now that the Tm.IsNValue premise is gone).

• Is every ⇢ normal form also a Tm.Step normal form? Yes — Tm.Step is a subrelation of ⇢, so anything stuck for ⇢ is stuck for Tm.Step.

• Is every value reachable by Tm.Step (in many steps) also reachable by ⇢ (in many steps)? Yes, for the same subrelation reason.

• Conversely? No: iszero (succ true) reaches the value false under ⇢ but is stuck under Tm.Step.

A functional version computes a single ⇢ step of a term, returning none when the term is a ⇢ normal form. This is a nice chance to see a step function, which the chapter otherwise gives only as a relation:

4.1.4. Typing🔗

The next critical observation is that, although this language has stuck terms, they are always nonsensical, mixing booleans and numbers in a way that we don't even want to have a meaning. We can easily exclude such ill-typed terms by defining a typing relation that relates terms to the types (either numeric or boolean) of their final results.

The typing relation ⊢ t ⦂ τ relates terms to the types of their results. In informal notation it is often written ⊢ t ⦂ τ and pronounced "t has type τ." The ⊢ symbol is called a "turnstile." The ⦂ between the term and its type is a dedicated type-colon glyph (distinct from an ordinary :); in the editor you enter it with the Lean input abbreviation \tc followed by a space. Below, we're going to see richer typing relations where one or more additional "context" arguments are written to the left of the turnstile. For the moment, the context is always empty.

                     -------------                (tru)
                     ⊢ true ⦂ Bool

                     --------------               (fls)
                     ⊢ false ⦂ Bool

          ⊢ t₁ ⦂ Bool    ⊢ t₂ ⦂ τ    ⊢ t₃ ⦂ τ
          -----------------------------------     (ite)
              ⊢ if t₁ then t₂ else t₃ ⦂ τ

                       ---------                  (zero)
                       ⊢ 0 ⦂ Nat

                      ⊢ t₁ ⦂ Nat
                    ---------------               (succ)
                    ⊢ succ t₁ ⦂ Nat

                      ⊢ t₁ ⦂ Nat
                    ---------------               (pred)
                    ⊢ pred t₁ ⦂ Nat

                      ⊢ t₁ ⦂ Nat
                   ------------------             (isZero)
                   ⊢ iszero t₁ ⦂ Bool

Here are the formal rules.

The typing judgment is written <{ ⊢ t ⦂ T }>: the whole judgment is wrapped in <{ … }>, the term is in the object grammar (bare variables, no inner <{ }>) and the type as Bool/Nat (a type variable is spliced, ~T escapes to a Lean Ty). As with Tm.Step, we define the relation using its own notation. The detailed definition of the notation is folded into the box below.

It's important to realize that the typing relation is a conservative (or static) approximation: it does not consider what happens when the term is reduced — in particular, it does not calculate the type of its normal form.

4.1.5. Canonical forms🔗

The following two lemmas capture the fundamental fact that the definitions of boolean and numeric values agree with the typing relation: a well-typed value of type Bool is a boolean value, and of type Nat a numeric value.

4.1.6. Progress🔗

The typing relation enjoys two critical properties.

The first is that well-typed normal forms are not stuck — or conversely, if a term is well typed, then either it is a value or it can take at least one step. We call this progress.

This theorem is more interesting than the strong progress theorem that we saw in the Smallstep chapter, where all normal forms were values. Here a term can be stuck, but only if it is ill typed.

4.1.7. Type Preservation🔗

The second critical property of typing is that, when a well-typed term takes a step, the result is a well-typed term (of the same type).

The preservation theorem is often called subject reduction, because it tells us what happens when the "subject" of the typing relation is reduced. This terminology comes from thinking of typing statements as sentences, where the term is the subject and the type is the predicate.

4.1.8. Type Soundness🔗

Putting progress and preservation together, we see that a well-typed term can never reach a stuck state.