Re: [isabelle] Termination Proof ``fun'' ;)



Hi Scott,

all_children :: obj => obj set => obj set
all_children src seen =
  if src \<in> seen
    then seen
    else
      foldr all_children (children src) (seen \<union> {src})

This is nonterminating in general, unless the obj type is finite. So there can't be just a simple "measure".

If your application does not require the functional view (like for code generation), you best define all_children as an inductive set or predicate, which avoids all termination issues and is usually much simpler.

You can define partial functions in Isabelle (see the function tutorial for a small example), but this introduces explicit domain predicates and in particular prevents code generation unless your function is tail-recursive (this is how it is done in Stefan's formalization...)

But if you really just need all_children defined somehow, then just use "inductive"

Alex






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