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
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
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Will Sonnex wrote:
Zeno is a fully automated inductive theorem proving tool for Haskell programs.
I tried it via the web interface, and it seems to be quite cool. Good work! However:
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.
That is surprising, given that this property does not seem to be true for p = const undefined and xs /= []. Tillmann
However:
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.
That is surprising, given that this property does not seem to be true for p = const undefined and xs /= [].
Tillmann
This is a very interesting observation. When Zeno does induction/case-splitting it does not consider the value _|_ as a potential inhabitant of a type. This could be a feature I might add in a later version or some option for being able to turn this behaviour on/off but thanks for spotting it. Infinite values (lazy-evaluation in general) also give Zeno a problem, since you can no longer use structure as a well-defined ordering for induction. A property such as "reverse (reverse xs) === xs" does not work for infinite lists, since you can successfully case-analyse values from "xs" but case-analysing "reverse (reverse xs)" will give an infinite loop. You could say the values are equal in some sense (maybe given infinite computation time) but they do not behave in the same way. Cheers, Will
On 11/13/10 8:15 AM, Will Sonnex wrote:
Infinite values (lazy-evaluation in general) also give Zeno a problem, since you can no longer use structure as a well-defined ordering for induction. A property such as "reverse (reverse xs) === xs" does not work for infinite lists, since you can successfully case-analyse values from "xs" but case-analysing "reverse (reverse xs)" will give an infinite loop. You could say the values are equal in some sense (maybe given infinite computation time) but they do not behave in the same way.
Generally speaking the solution for handling possibly infinite structures is to use coinduction rather than induction. The reason "reverse (reverse xs) === xs" doesn't work for (possibly)infinite lists is that we can't prove that reverse.reverse makes any progress (since reverse of an infinite list is bottom). But there are plenty of other things you could still prove for infinite structures, "map f (map g xs) === map (f.g) xs" for example. -- Live well, ~wren
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
Yeah as it is Zeno can only prove equality properties, but I would love to extend it with these other proof features. I'm currently working on a more general notion of well-founded ordering within the program (so that it can hopefully verify quicksort/mergesort) and I guess I could expose this feature so one could prove the totality of functions in the way you said. Cheers, Will
Is the source code public, so I can run it on my own machine? Luke
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Oops. It's right there on the site. My eyes skipped over it for some reason.
On Sat, Nov 13, 2010 at 2:11 PM, Luke Palmer
Is the source code public, so I can run it on my own machine?
Luke
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (5)
-
Luke Palmer -
Petr Pudlak -
Tillmann Rendel -
Will Sonnex -
wren ng thornton