The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
There are several reasons why we want to represent expressions in a normal form:
Idealised manipulation of equations. If we have x == 1 + y but, elsewhere, we additionally know that x == y, then we can arrive at a contradiction.
Reduced Search Space. If we knew x == y but didn't exploit this, then we could end up generating separate facts, such as x == 1 + z as distinct from y == 1 + z.
Easier manipulation of terms. For example, having arithmetic expressions in the form of a Polynomial does make life more convenient. That said, have two possible representations for the same thing (e.g. x and its polynomial form 0+x) also makes life tricky.
On the negative side, there is the problem of "lost representation". Consider this example:
define contains(int[] items, int item) is:
exists(int k).(items[k] == item)
assert:
forall(int[] xs, int x):
if:
|xs| > 0
!contains(xs,x)
then:
xs[0] > x
In a proof-by-contradiction, we'll end up with the equivalence xs[0] == x. In order to prove the contradiction, we need to instantiate against xs[0]. But, if we had decided xs[0] was the representative of the equivalence class containing both xs[0] and x, then we can end up missing xs[0] and not triggering instantiation. This happens because automatically substitution moves terms to their normal form.
Other situations where normal form representation can cause problems:
Array length axiom. This triggers specifically on array length terms of the form |A|. For example, it would trigger on |A| < 0. But, we might have (|A| := x) && (x < 0).
Array index axioms. These are similar for array length. This axiom looks for terms of the form A[i] and then triggers on various situations, including those involving |A|.
Fresh term construction. Whenever a new term is created from existing terms (e.g. |A| is created from A) we have to make sure to convert that term into the appropriate normal form. Otherwise, we end up with some terms in the wrong form, and this causes things to be missed.
The other difficult thing caused by normal form representation is that the printed proofs don't resemble their original form. The normal form tends to be a bit ugly in places as well (especially with have inequalities always represented by >= because you end with gross things like |A| >= (i+1) which is much better denoted as i < |A|.
DavePearce
commented
7 years ago
There are several reasons why we want to represent expressions in a normal form:
x == 1 + ybut, elsewhere, we additionally know thatx == y, then we can arrive at a contradiction.x == ybut didn't exploit this, then we could end up generating separate facts, such asx == 1 + zas distinct fromy == 1 + z.Polynomialdoes make life more convenient. That said, have two possible representations for the same thing (e.g.xand its polynomial form0+x) also makes life tricky.On the negative side, there is the problem of "lost representation". Consider this example:
define contains(int[] items, int item) is: exists(int k).(items[k] == item) assert: forall(int[] xs, int x): if: |xs| > 0 !contains(xs,x) then: xs[0] > xIn a proof-by-contradiction, we'll end up with the equivalence
xs[0] == x. In order to prove the contradiction, we need to instantiate againstxs[0]. But, if we had decidedxs[0]was the representative of the equivalence class containing bothxs[0]andx, then we can end up missingxs[0]and not triggering instantiation. This happens because automatically substitution moves terms to their normal form.Other situations where normal form representation can cause problems:
|A|. For example, it would trigger on|A| < 0. But, we might have(|A| := x) && (x < 0).A[i]and then triggers on various situations, including those involving|A|.|A|is created fromA) we have to make sure to convert that term into the appropriate normal form. Otherwise, we end up with some terms in the wrong form, and this causes things to be missed.The other difficult thing caused by normal form representation is that the printed proofs don't resemble their original form. The normal form tends to be a bit ugly in places as well (especially with have inequalities always represented by
>=because you end with gross things like|A| >= (i+1)which is much better denoted asi < |A|.