Inductive Datatypes II

In class 7, we will be continuing to work with linked lists. In class 8, we will work with a more elaborate type for representing mathematical expressions, and it is that Expr type we introduce in this reading.

Example: arithmetic expressions

Let’s begin with an inductive datatype for some simple mathematical expressions:

datatype Expr =
  | Const(value: int)
  | Var(name: string)
  | Plus(left: Expr, right: Expr)

That is, an expression is either an integer constant, a named variable, or a sum of two expressions.

type State = map<string, int>

datatype Expr =
  | Const(value: int)
  | Var(name: string)
  | Plus(left: Expr, right: Expr)

type State = map<string, int>

function Eval(expr: Expr, state: State): int { 
  match expr
  
  
  
}

lemma Example() {
  var expr := Plus(Plus(Var("x"), Const(3)), Var("y")); // x + 3 + y
  var xyz := map["x" := 10, "y" := 20, "z" := 30];
  assert Eval(expr, xyz) == 33;

  var empty := map[];
  assert Eval(expr, empty) is int;
}

In the exercise above, example.dfy is a “test case” whose correctness Dafny is able to prove. As with all of our verification, the program is not being run! Dafny is repeatedly unfolding functions and expanding definitions in order to attempt a proof. This strategy is more likely to work for expressions that require only a small number of unfoldings, and it is less likely to work as the computation grows in complexity. For sufficiently intricate examples, even if they are correct, Dafny will no longer be able to prove their correctness because it does not manage to complete its “simulation” of the computation.

Nevertheless, when we’re not sure if our definitions are working as intended, constructing concrete examples and checking their behavior can give us confidence.

Example: free variables

Hopefully you are grumpy about the -42 in our solution above and in general about Eval’s specification in the face of undefined Var names. The natural thing to do is restrict evaluation to expressions and states where every variable has a value in the state.

datatype Expr =
  | Const(value: int)
  | Var(name: string)
  | Plus(left: Expr, right: Expr)

type State = map<string, int>

function FreeVars(expr: Expr): set<string> { 
  match expr
  case Const(_) => ?
  case Var(name) => ?
  case Plus(left, right) => ?
}

lemma Example() {
  var expr := Plus(Plus(Var("x"), Const(3)), Var("y")); // x + 3 + y
  assert FreeVars(expr) == {"x", "y"};

  assert FreeVars(Const(3)) == {};
}

function Eval(expr: Expr, state: State): int
  // ???
{
  match expr
  case Const(value) => value
  case Var(name) => state[name] // no more -42
  case Plus(left, right) => Eval(left, state) + Eval(right, state)
}

Example lemma: same value

We can use these last two definitions of Eval and FreeVars to prove a simple property of expression evaluation by induction.

datatype Expr =
  | Const(value: int)
  | Var(name: string)
  | Plus(left: Expr, right: Expr)

type State = map<string, int>

function Eval(expr: Expr, state: State): int {
  match expr
  case Const(value) => value
  case Var(name) => if name in state then state[name] else -42
  case Plus(left, right) => Eval(left, state) + Eval(right, state)
}

function FreeVars(expr: Expr): set<string> {
  match expr
  case Const(_) => {}
  case Var(name) => {name}
  case Plus(left, right) => FreeVars(left) + FreeVars(right)
}

lemma Weakening(expr: Expr, state1: State, state2: State) 
  requires ?
  ensures Eval(expr, state1) == Eval(expr, state2)
{
}

lemma Example() {
  var expr := Plus(Plus(Var("x"), Const(3)), Var("y"));
  var xyz := map["x" := 10, "y" := 20, "z" := 30];

  var empty := map[];
  Weakening(Const(3), empty, xyz);

  var different := map["a" := 5, "b" := 10, "x" := 10, "y" := 20];
  Weakening(expr, xyz, different);
}

Summary

Inductive type definitions are often associated with recursive functions, which then become handy to use in preconditions and postconditions. Whenever you notice a verification isn’t going through because some property (“obvious” or not) about an inductive type isn’t being taken into account, consider formalizing the property with a recursive function and adding it to related specifications.