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.

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🔗

3.1.4. Delaborators🔗

3.1.5. Evaluation🔗

Now we need to add an st parameter to both evaluation functions:

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

A nonterminating theorem loop_false (n : Nat) : False := loop_false n would make False provable, so Lean rejects it.

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.

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.