> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe