Stream: Beginner Questions

Topic: Proving termination of function, if arguments well-formed

Maximilian Vollath (May 30 2025 at 19:13):

I have a function that only terminates if it's called with valid arguments, and that is always the case.
Can I prove this conditional termination to obtain executable code, or do I actually have to modify the function such that it also terminates with invalid arguments, then prove that?

Mathias Fleury (May 30 2025 at 19:19):

You can define the type of only valid arguments

Maximilian Vollath (May 30 2025 at 19:20):

Ooooh, thanks, I'll play around with that.

Mathias Fleury (May 30 2025 at 19:21):

I did this once https://github.com/IsaFoL/IsaFoL/blob/master/Weidenbach_Book/CDCL/DPLL_W_Implementation.thy#L361, but have forgotten all the details now. I just remember that this is described somewhere in the codegen tutorial

Jan van Brügge (May 31 2025 at 09:20):

What I did in a similar case is to modify the function definition like this: f x = if valid x then <recursion> else undefined and then derived a better simp rule afterwards that assumed valid x and did not have the undefined

Jan van Brügge (May 31 2025 at 09:21):

Dealing with subtypes can be annoying sometimes

Maximilian Vollath (May 31 2025 at 09:24):

Oh yeah that's even better in my case, thank you!

Mathias Fleury (May 31 2025 at 15:31):

Yes if valid x is simple enough and that you do not care about performance…

Manuel Eberl (Jun 03 2025 at 15:56):

These two approaches are probably the best ones for most use cases: a simple validity check if performance and decidability of that check is not an issue, and a typedef otherwise.

Another thing you can do is to use the partial_function command with the (option) flag, which makes it so that your function logically returns None in case of nontermination or Some x in case of termination with a result x. If your function definition is tail-recursive, you can use partial_function with the (tailrec) flag instead and do away with the option type; in that case, the result in nonterminating cases is simply unspecified.

Last updated: Jun 21 2025 at 01:46 UTC