I guess I'm not on the list that received the original announce. But I have to say, I played with the demo ( http://www.doc.ic.ac.uk/~ws506/tryzeno/ ). Wow! I am delighted and impressed, and I think this is a huge step forward. Great work!
Luke On Sat, Nov 13, 2010 at 1:31 AM, Petr Pudlak <[email protected]> wrote: > 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 > > -----BEGIN PGP SIGNATURE----- > Version: GnuPG v1.4.10 (GNU/Linux) > > iQEcBAEBAgAGBQJM3kzdAAoJEC5dcKNjBzhn6ZgH/24Yy1TBsCCtwmvItROvucms > VNlaJ9lAEwbFtQT4X0HJtBX0MaMc/2QcPXhXsTTXm5CG+28N7ohrVDz9WIn3Zmri > Tet1c+NFeZ5s4dK9Xjc450r1zlBYu6Uc8y/z9+RRbUTdDKpifGScwoxqFQPeWWYX > fUY9zfM6RW4W7A/hTzFIZlRpa2l8/1d4ojBeRw8PnxpPftBk8KvXAVBxq1Nf21Pc > pKmcfMFfhTCPAXsroLMXzP22A51XhIXrSREpvE+OgDSHsoaO+0D2/q8VMV+J1zPw > PPYvmM/BOYAPcjy/Z34kNv2g6letXKOjH5ofHREr5arHpsrsmJxP+rcveZWQi1A= > =58nx > -----END PGP SIGNATURE----- > > _______________________________________________ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
