Stream: Beginner Questions

Topic: ✔ the meaning of "no solution" for a function equation

Chengsong Tan (Aug 19 2021 at 18:51):

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?

Manuel Eberl (Aug 19 2021 at 19:17):

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.

Manuel Eberl (Aug 19 2021 at 19:18):

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…

Chengsong Tan (Aug 19 2021 at 19:25):

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.

Manuel Eberl (Aug 19 2021 at 19:26):

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.

Manuel Eberl (Aug 19 2021 at 19:27):

e.g. for Booleans, undefined = True ∨ undefined = False is provable, but undefined = True and undefined = False individually are not.

Manuel Eberl (Aug 19 2021 at 19:28):

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.

Chengsong Tan (Aug 19 2021 at 19:28):

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.

Chengsong Tan (Aug 19 2021 at 19:51):

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).

Manuel Eberl (Aug 19 2021 at 19:58):

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.

Manuel Eberl (Aug 19 2021 at 19:59):

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.

Notification Bot (Aug 20 2021 at 15:59):

Chengsong Tan has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC