Koen, does "let binding" in fof improve performance?
Nathan Collins
The contracts draft "let binds" the term of interest in many formulas,
e.g. for functions it has
[| f xs = case e of p1 -> e1 ... pn -> en |] =
forall xs a. (min a /\ f xs = a) ->
(min e /\ (e = bad \/ (\/_i exists xsi. e = Ki xsi) \/ a = unr)
/\ (e = bad -> a = bad)
/\ (/\_i forall xsi. e = Ki xsi -> a = ei))
whereas I implemented something more like
[| f xs = case e of p1 -> e1 ... pn -> en |] =
forall xs. (min (f xs) ->
(min e /\ (e = bad \/ (\/_i exists xsi. e = Ki xsi) \/ f xs = unr)
/\ (e = bad -> f xs = bad)
/\ (/\_i forall xsi. e = Ki xsi -> f xs = ei))
Do you expect a performance improvement from the "let binding" in the
former? It's not hard to implement, but even easier to ask :)
Cheers,
-nathan
Koen Claessen
The only reason to do this "let binding" is to avoid explosion of the
formula in the input problem (i.e. if you neglect to do it repeatedly,
you might get a doubling in term size every time).
If this is not a problem, and it is hard to do, then you might just as
well not bother.
I expect any theorem prover worth its name to do some kind of common
subexpression elimination which will internally give the same
representation as when you did it explicitly.
(Although, one reason to do the naming trick is to avoid making
mistakes when you repeatedly construct the same term.)
/Koen