[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

[Will Sonnex]

> 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