Wiki Agenda Contact Version française

Disambiguation of Plus Expressions

Show equivalence of two grammars describing concrete Plus Expressions

Authors: Quentin Garchery

Topics: Mathematics / Tricky termination

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

Disambiguation of Plus Expressions

Author: Quentin Garchery (LRI, Université Paris-Sud)

use int.Int
use list.ListRich

Consider the 'concrete' syntax of Plus Expressions containing only : integers, the symbol PLUS and parentheses.

type token = INT | PLUS | LPAREN | RPAREN

Plus Expressions are lists of tokens that satisfy the original following inductive predicate.

inductive pe (e : list token) =
    | Plus : forall e1 e2. pe e1 -> pe e2 -> pe (e1 ++ Cons PLUS e2)
    | Paren : forall e. pe e -> pe (Cons LPAREN (e ++ (Cons RPAREN Nil)))
    | Int : pe (Cons INT Nil)

goal pe1 : pe (Cons INT Nil)
goal pe2 : pe (Cons INT (Cons PLUS (Cons INT (Cons PLUS (Cons INT Nil)))))

Define another predicate to recognize Plus Expressions but that removes the ambiguity coming from the associativity of PLUS.

inductive pe' (e : list token) =
   | Plus' : forall e1 e2. pe' e1 -> pt e2 -> pe' (e1 ++ Cons PLUS e2)
   | T' : forall t. pt t -> pe' t
with pt (e : list token) =
    | Paren' : forall e. pe' e -> pt (Cons LPAREN (e ++ (Cons RPAREN Nil)))
    | Int' : pt (Cons INT Nil)

goal pep1 : pe' (Cons INT Nil)
goal pep2 : pe' (Cons INT (Cons PLUS (Cons INT (Cons PLUS (Cons INT Nil)))))

Show that the two predicates recognize the same expressions.

Strengthen the disambiguation_included formula, making sure the pt predicate appears.

let rec lemma di_str (n : int)
    variant { n }
    ensures { forall e. (length e <= n /\ pt e) \/ (length e < n /\ pe' e) ->
    	      	     	pe e }
    if n <= 0
    then ()
    else di_str (n-1)

let lemma disambiguation_included (e : list token)
    requires { pe' e }
    ensures { pe e }
    di_str (length e + 1)

Strengthen the original_included formula and prove it by using mutal recursion (showing that we can decompose an expression w.r.t its last toplevel PLUS symbol).

let rec lemma oi_str (n : int) (ghost m : int)
    variant { n, m }
    requires { m > n }
    ensures { forall e. length e <= n -> pe e -> pe' e }
    = if n > 0 then (decomp_last_plus n (m-1); oi_str (n-1) m)

with ghost decomp_last_plus (n : int) (ghost m : int)
     variant { n, m }
     requires { m >= n }
     ensures { forall e. length e <= n -> pe e -> not pt e ->
     	       exists e1 e2. pe e1 /\ pt e2 /\ e = e1 ++ Cons PLUS e2 }
     if n > 0 then (decomp_last_plus (n-1) n; oi_str (n-1) n)

lemma original_included :
      forall e. pe e -> pe' e

lemma original_equiv_disambiguation :
      forall e. pe e <-> pe' e

download ZIP archive

Why3 Proof Results for Project "disamb"

Theory "disamb.Top": fully verified

ObligationsAlt-Ergo 2.3.0CVC4 1.6
VC for di_str0.03---
VC for disambiguation_included---0.04
VC for oi_str0.03---
VC for decomp_last_plus0.14---