Description
" - In QED-at-large, you seem to state that Isabelle/HOL does not
support partial functions. In a recent assignment where I tried to
understand the support of inductive predicates in both HOL based and
type-theory-based provers, I noted some work by Krauss "Partial and
Nested Recursive Function Definitions in Higher-order Logic" which
contradicts this assertion. Here is a very short summary:
-
you can describe a recursive function, potentially non-terminating,
as a function that returns an arbitrary value when not terminating. -
All theorems about the behavior of this function are prefixed by
the condition that the input must be in the domain of definition. -
The domain definition itself can be described as an inductive predicate.
-
In practice, the function is first described as an inductive
relation: R_f(x, y) that holds exactly when f(x) terminates and f(x) =
y. The HOL logic in Isabelle contains the "Hilbert" choice operator,
which makes it possible to construct the final value f(x) from the
relation R_f.
It is probably too late to correct the paper, but it is useful to know
that Isabelle has a powerful tool to handle potentially non-terminating
recursive functions in a comfortable way (in some sense, it is more
comfortable that what is available in plain Coq, because you can write
f(x) even before you have proved that recursion terminates on x)."