-----Original Message-----
Date: Friday, October 23, 1998 1:17 PM
Subject: Re: declaring properties
>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.
That is correct; the prototype only applies to finite cases. This is being
fixed,
but the prover should also be able to prove theorems which are valid only
for
finite cases, like this one. It could first try to prove it for all cases,
fail, and then try
to prove it for finite cases only and succeed.
(difference in proving: another induction scheme)
>
>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?)
This can be done by reusing an interpreter for Clean (ensured to use the
correct semantics) in the prover. This makes sure the rewriting of
function-definitions is OK. The second step is then to check that no other
derivation step violates this rewrite-strategy (this is mostly needed for
induction). For this a formalization of the strategy is needed, as well
a formalization of what the prover defines to be `equivalence'.
>
>Regards,
>Koen.
>
>--
>Koen Claessen,
>[EMAIL PROTECTED],
>http://www.cs.chalmers.se/~koen,
>Chalmers University of Technology.
>
Maarten de Mol
University of Nijmegen
