[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

[Petr Pudlak]

     Hi Will,

I was wondering, Zeno capable of proving just equational statements, or 
is it able to prove more general statements about programs? In 
particular, it would be interesting if Zeno would be able to prove that 
a function is total by verifying that it uses only structural 
(inductive) recursion (on a well defined inductive type), i.e. each 
recursive function call must be on a syntactic subcomponent of its 
parameter. And dually, one might want to prove that a function is 
corecursive, meaning that each recursive call is guarded by a 
constructor.

     Best regards,
     Petr

> Hi all,
> 
> My masters project Zeno was recently mentioned on this mailing list so
> I thought I'd announce that I've just finished a major update to it,
> bringing it slightly closer to being something useful. Zeno is a fully
> automated inductive theorem proving tool for Haskell programs. You can
> express a property such as "takeWhile p xs ++ dropWhile p xs === xs"
> and it will prove it to be true for all values of p :: a -> Bool and
> xs :: [a], over all types a, using only the function definitions.
> 
> Now that it's updated it can use polymorphic types/functions, and you
> express properties in Haskell itself (thanks to SPJ for the
> suggestion). It still can't use all of Haskell's syntax: you can't
> have internal functions (let/where can only assign values), and you
> can't use type-classed polymorphic variables in function definitions -
> you'll have to create a monomorphic instance of the function -but I
> hope to have these added reasonably soon. It's also still missing
> primitive-types/IO/imports so it still can't be used with any
> real-world Haskell code, it's more a bit of theorem proving "fun".
> 
> You can try it out at http://www.doc.ic.ac.uk/~ws506/tryzeno, the code
> file given there has some provable properties about a few prelude
> functions among other things.
> 
> Another feature is that it lists all the sub-properties it has proven
> within each proof. When it verifies insertion-sort "sorted (insertsort
> xs) === True" it also proves the antisymmetry of "<=" and that the
> "insert" function preserves the "sorted" property.
> 
> Any suggestions or feedback would be greatly appreciated.
> 
> Cheers,
> 
> Will
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20101113/57309778/attachment.bin