On Fri, 23 Oct 1998, Maarten de Mol wrote:
| Actually, a prototype for declaring and proving properties in Clean
| has been implemented and will be upgraded to a fully integrated
| language tool.
I think this is very interesting and should certainly be further
developed!
In the paper, found on:
http://www.cs.kun.nl/~maartenm/IFLPaper.ps
you say that you have written your own proof tool, because existing
theorem provers might not correspond to the semantics of Clean.
With all respect, it seems that your own tool doesn't do this either!
Because two of the example theorems your tool can prove:
Reverse (xs++ys) == Reverse ys ++ Reverse xs
Reverse (Reverse xs) == xs
are not true in general! Namely, they are not true for infinite lists.
Now, this is just an example, so I am sure it can be fixed (induction over
data types shopuld include a bottom case, or only work for "strict"
functions).
But how can you be sure that the theorems your tool proves are actually
conform the Clean semantics? (read: How do you convince the user of the
tool?)
Regards,
Koen.
--
Koen Claessen,
[EMAIL PROTECTED],
http://www.cs.chalmers.se/~koen,
Chalmers University of Technology.
