I have read this interesting blog

https://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined#cb10-2

about Isabelle functions being total.

I am just a bit puzzed at the section "non-terminating functions are also just underspecified"

and "not all function specifications are ok"

To me,

fixpoint (λb. ¬b) True = fixpoint (λb. ¬b) False

and

bogus () = Suc (bogus ())

are both non-terminating equations with no solution.

Why is the fixpoint function allowed and the other not?

For tail-recursive specifications like `fixpoint f x = fixpoint f (f x)`

, you can always find a consistent solution, e.g. by simply returning some dummy value (like `undefined`

) if it doesn't terminate. For non-tail-recursive ones like `bogus () = Suc (bogus ())`

, this is generally not possible.

There's probably more theory behind this that tells you when this is okay and when it isn't – perhaps domain theory? I don't know enough about that to be able to say…

Manuel Eberl said:

For tail-recursive specifications like

`fixpoint f x = fixpoint f (f x)`

, you can always find a consistent solution, e.g. by simply returning some dummy value (like`undefined`

) if it doesn't terminate. For non-tail-recursive ones like`bogus () = Suc (bogus ())`

, this is generally not possible.

Thank you!

So the main difference here is whether the function is tail-recursive or not?

To me `fixpoint f _ = undefined`

and `bogus _ = undefined`

seem both valid solutions.

No, the important thing to understand is that `undefined`

is *not* some special value that lives outside the normal type universe (like $\bot$ in Haskell). It is a value inside the type, you just don't know which one.

e.g. for Booleans, `undefined = True ∨ undefined = False`

is provable, but `undefined = True`

and `undefined = False`

individually are not.

That means that `bogus _ = undefined`

is *not* a valid solution because then one would have to have `undefined = Suc undefined`

, which is false because `x ≠ Suc x`

holds for all natural numbers.

Manuel Eberl said:

There's probably more theory behind this that tells you when this is okay and when it isn't – perhaps domain theory? I don't know enough about that to be able to say…

This reminds me of series in calculus.

Both 1 0 1 0 1 and

1 2 3 4 5 ........

are divergent series.

Ah the above is a bad analogy.

It breaks down for the example

`bogus2 n = bogus2 n+1`

which has the solution `bogus2 _ = undefined`

And

```
partial_function (tailrec) bogus::"nat ⇒ nat" where
"bogus n = bogus (Suc n)"
```

is permitted by Isabelle (since it is tail-recursive).

Note that when you have a lattice structure on your result, you can also do non-"terminating" definitions if your step function is monotonic. E.g. for the extended natural numbers (i.e. natural numbers + ∞) you can define `f = f + 1`

and that gives you `f = ∞`

. Not with the function package though.

If I recall correctly, the reason is that the existence of a unique least fixed point is guaranteed by the Knaster–Tarski theorem in such settings.

Last updated: Jul 15 2022 at 23:21 UTC