3.1.1. States🔗

Since we'll want to look variables up to find out their current values, we'll use total maps from the Typeclasses chapter of Logical Foundations. A machine state (or just state) represents the current values of all variables at some point in the execution of a program.

For simplicity, we assume that the state is defined for all variables, even though any given program is only able to mention a finite number of them. Because each variable stores a natural number, we represent the state as a total map from strings (variable names) to Nat, and will use 0 as the default value in the store.

We give the type of variable identifiers a name, Ident. For now it is just String; naming it makes the intent clearer.

3.1.2. Syntax🔗

We can add variables to the arithmetic expressions we had before simply by including one more constructor. (This is a fresh Aexp, replacing the variable-free one from the Slang chapter.)

The Bexp definition is unchanged, except that it now refers to the new Aexp.

Defining a few variable names as shorthands will make examples easier to read.

3.1.3. Notations🔗

To make Imp programs easier to read and write, we introduce some notations.

You do not need to understand exactly what these declarations do. Briefly, though, here is how the two blocks below fit together:

• The declare_syntax_cat directive adds a new non-terminal to Lean's grammar, called imp_aexp. We'll add additional non-terminals further below.

• Each syntax directive defines a grammar production. Seven of them build the imp_aexp category itself: the first two make a numeric literal and an identifier into an imp_aexp, the next three build larger expressions (with annotations that fix precedence and associativity), and the last two are parentheses for grouping and ~, the escape back to Lean. The eighth, aexp { … }, is a production of Lean's own term category — it is what lets an Imp expression appear in ordinary Lean code.

• ~e splices an already-elaborated Lean term e into Imp syntax. We use it throughout the chapter to drop a previously-defined expression or command into a larger program, as in imp { while (X ≠ 0) { ~subtract_slowly_body } }.

• Finally, macro_rules is used to translate each production of the imp_aexp non-terminal into a Lean expression.

Boolean expressions and, later, commands follow this same pattern exactly, so their declarations are collapsed where they appear: open one if you want to see the pattern repeated, and skip it otherwise.

3.1.4. Delaborators🔗

Next, we write a suite of delaborators for Aexp and Bexp. Delaborators are like the opposite of macro_rules -- they are used to pretty print elaborated terms back to the user.

With these delaborators in place, Lean pretty-prints Imp expressions with the higher-level notations rather than their raw constructors.

The pretty-printed version of an expression might not exactly match its original form. For example, the parentheses around X * 2 in aexp { 3 + (X * 2) } are not printed because they are redundant, which the parenthesizer knows.

3.1.5. Evaluation🔗

The arithmetic and boolean evaluators must now be extended to handle variables, taking a state st as an extra argument. A variable is looked up in the state with the map-indexing notation st[x] from the Typeclasses chapter in the Logical Foundations book. For the notation to work, we used open scoped MyGetElem earlier, which opens only the scoped items like notation from the module.

We reuse the total-map notation (x →ₜ v etc.) for states.

3.2.1. Desugaring Notations🔗

Even though the notations are useful for getting the high-level picture, it's sometimes helpful to turn off the notation to see the parsed structure as a plain term. This can be done with set_option pp.notation false (which we briefly mentioned in the Typeclasses chapter) as follows:

imp {X := X + 1} : Com

Com.asgn X ((Aexp.id X).plus (Aexp.num 1)) : Com

3.2.2. More Examples🔗

A few more examples.

Assignment:

Loops:

An infinite loop:

3.3.1. Evaluation as a Function (Failed Attempt)🔗

In a more conventional functional language like OCaml or Haskell, we could define the evaluation function as follows:

fail to show termination for
  Com.eval
with errors
failed to infer structural recursion:
Cannot use parameter st:
  the type TotalMap Ident Nat does not have a `.brecOn` recursor
Cannot use parameter c:
  failed to eliminate recursive application
    eval st (imp {~c; while (~b) {~c}})


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
st:Stateb:Bexpc:Comh✝:Bexp.eval st b = true⊢ 1 + sizeOf c + (1 + sizeOf b + sizeOf c) < 1 + sizeOf b + sizeOf c

Lean doesn't accept such a definition because the function we want to define is not guaranteed to terminate. Indeed, it doesn't always terminate: the full Com.eval applied to the loop program above would run forever. Since Lean aims to be not just a programming language but also a consistent logic, any potentially non-terminating function must be rejected.

Here is what would go wrong if Lean allowed non-terminating recursive functions:

That is, propositions like False would become provable (loop_false 0 would be a proof of False), a disaster for logical consistency.

Thus, because it doesn't terminate on all inputs, the full Com.eval cannot be written in Lean -- at least not without additional tricks and workarounds.

3.3.2. Evaluation as a Relation🔗

Here's a better way: define Com.eval as a relation rather than a function -- i.e., make its result a Prop rather than a State, similar to what we did for Aexp.EvalR in the Slang chapter.

This is an important change. Besides freeing us from awkward workarounds, it gives us more flexibility in the definition. For example, if we add nondeterministic features like any to the language, we want the definition of evaluation to be nondeterministic -- i.e., not only will it not be total, it will not even be a function!

3.3.3. Operational Semantics🔗

We'll use the notation st =[ c ]=> st' for the Com.EvalR relation: st =[ c ]=> st' means that executing program c in a starting state st results in an ending state st'. This can be pronounced "c takes state st to st'".

Here is an informal definition of evaluation, presented as inference rules for readability:

                      -----------------                  (skip)
                      st =[ skip ]=> st

                      a.eval st = n
              --------------------------------           (asgn)
              st =[ x := a ]=> (x →ₜ n ; st)

                      st  =[ c₁ ]=> st'
                      st' =[ c₂ ]=> st''
                    ---------------------                (seq)
                    st =[ c₁;c₂ ]=> st''

                     b.eval st = true
                      st =[ c₁ ]=> st'
           ---------------------------------------       (ifTrue)
           st =[ if (b) { c₁ } else { c₂ } ]=> st'

                    b.eval st = false
                      st =[ c₂ ]=> st'
           ---------------------------------------       (ifFalse)
           st =[ if (b) { c₁ } else { c₂ } ]=> st'

                    b.eval st = false
               ----------------------------              (whileFalse)
               st =[ while (b) { c } ]=> st

                     b.eval st = true
                      st =[ c ]=> st'
             st' =[ while (b) { c } ]=> st''
             -------------------------------             (whileTrue)
             st  =[ while (b) { c } ]=> st''

Here is the formal definition. Make sure you understand how it corresponds to the inference rules.