[Prev][Next][Index]
LP
I think that LP 3.1 (94/12/30) has a problem with alpha conversion, it
does not always rename bound variables properly. This results in a
soundness problem.
Example:
declare sorts Nat
declare operators
__ + __: Nat, Nat -> Nat
, __ <= __: Nat, Nat -> Bool
..
declare variables a,b,k,n,m : Nat
assert (n <= m <=> \E k (n + k = m))
show norm a <= b
The sequence of reductions leading to the normal form of the term is:
1. a <= b
2. \E k (a + k = b)
^^^^^
This is as expected, but when other variables are used, LP makes a
mistake:
show norm n <= k
The sequence of reductions leading to the normal form of the term is:
1. n <= k
2. \E n (n + n = k)
^^^^^
When the sort Nat is renamed to fNat the names do not clash, in that
case the normal form of n <= k is: \E f (n + f = k) but the normal
form of f <= k is: \E f (f + f = k).