Re: [isabelle] Isabelle functions: Always total, sometimes undefined

> you have a deep embedding of the extracted code equations, right? So
> you could state termination, and (at least in theory) prove it in
> Isabelle, couldnât you?

The initial semantics (plain HO term rewriting) has no notion of
evaluation order or normal forms.

Instead one would need to define an alternative semantics that
prescribes an evaluation order and prove its correctness wrt original
semantics, or run my compiler to CakeML (which does precisely that).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.