This is an old revision of the document!
Homework 2
Quantifier Elimination
Consider a fragment of Presburger arithmetic where atomic formulas are equalities or inequalities of the form
, for arbitrary integer variables
and arbitrary constants
.
Verify whether this language admits quantifier elimination.
- If it does admit quantifier-elimination, prove that this is the case by describing this algorithm informally, but precisely. The algorithm should take a formula of the form Qx.F where Q is a quantifier and F is quantifier-free, and it should eliminate the quantifier.
- If it does not admit quantifier elimination, give an example formula that you believe does not have a corresponding equivalent quantifier-free formula and describe constructs that you need to add to make quantifier elimination possible.
The basic ideas described in the class for dense linear orders should suffice to do this problem, but you need to change and adapt them to make them work for the ordering on integers. You can read the following papers to help you construct the proof, but cannot just say that the result follows from e.g. quantifier elimination of Presburger arithmetic. Indeed, the question is whether quantifier elimination is possible in this simpler language and not in the language of general Presburger arithmetic.
- On the theory of structural subtyping (especially Sections 3.1 and 3.2)
- Early technical report on BAPA (see only Appendix 11.1)
For in depth understanding you can also read references in there, in particular the relevant Wilfrid Hodges model theory book sections.
Verification condition generator
1. Implement a verification condition generator that takes abstract syntax trees of the following form
S ::= (x=T) | assume(F) | assert(F) | havoc(v,...,v) | S ; S | while (F) { S } | if (F) { S } else { S } T ::= T+T | T-T | K*T | v A ::= T=T | T < T F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F K ::= 0 | 1 | 2 | ... v ::= x | y | z | ...
and computes a formula wp(S,F) for a given statement S and a given formula F. Here, the ASCII notation is the following:
& denotes conjunction | denotes disjunction ALL denotes universal quantifier EX denotes existential quantifier
This notation corresponds to a fragment of the language of the Isabelle theorem prover, as well as the Jahob system.
You do not need to build a parser for programs and formulas for this exercise, but it may make the testing of your implementation easier.
2. Given a statement S, compute wp(S,true) and pretty print it as a string conforming to the above grammar. Test your program on
- two input programs that generate valid formulas
- two input programs that generate invalid formulas
Try using the Isabelle theorem prover or formDecider in the Jahob system to prove the validity of the printed formulas and describe your experience.