[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

[Luke Palmer]

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 <deb at pudlak.name> 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
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>