Re: [isabelle] Non terminating function proven terminating



I did not find Isabelle's bug tracker so I hope that this is the place where
I'm supposed to report this.

In principle, yes, although this concrete one is a misunderstanding. (We currently have no formal tracking of bugs or misunderstandings)


Pierre Boutillier's trick (which breaks Coq's SN) seems to work in Isabelle.
As in Agda, we do not lose SN but we do accept a function that is not
well-defined.

Some further remarks:

You seem to be using a specific notion of "well-defined", probably coming from constructive type theory.

In HOL, there is no formal notion of well-definedness other than a very primitive one. Leaving pattern matching aside for now, we should rather say that a function (given by a recursive equation) is "definable", iff there is a HOL term that satisfies the equation (here that term is "\<lambda> _. ()"). Finding that term basically amounts to "solving" the equation, and this is what the definition command does for you for a certain subclass of definable functions.

Note also that Isabelle has no notion of SN other than the trivial beta/eta reduction of simply-typed lambda calculus. In particular, definitions are not unfolded (aka reduced) automatically, unlike in Coq, Agda etc. This means that "f is terminating" is merely an informal way of saying "f can be defined using well-founded induction".

Alex





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