Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation for non-terminating functions

Email Gateway (Nov 17 2020 at 18:12):

From: David Kretzmer <david.k@posteo.de>
Dear all,

is it possible to generate code for a potentially non-terminating
function f :: A => B if I ensure that whenever I actually call f a,
then f_dom a?

I sometimes have functions that are non-terminating in general but that
are only actually called with "safe" arguments. However, since I have to
prove termination in order for code generation to work (at least as far
as I know), I have to augment the function with additional checks that
ensure termination. This feels unsatisfactory, since I could
theoretically prove that these checks are never exercised during execution.

A silly example:

(* Does not terminate for n < 0 *)
function(domintros) factorial :: "int ⇒ int" where
  "factorial n = (if n = 0 then 1 else n * (factorial (n-1)))"
  by pat_completeness auto

lemma factorial_termination: "n ≥ 0 ⟹ factorial_dom n"
  by (metis add.commute add_diff_cancel_left' factorial.domintros
int_ge_induct)

(* A safe (i.e., terminating) wrapper around `factorial` *)
fun factorial_safe :: "int ⇒ int option" where
  "factorial_safe n = (if n ≥ 0 then Some (factorial n) else None)"

(* Does not work because there are no code equations for `factorial` *)
export_code factorial_safe in SML

Here, factorial_safe checks the preconditions of factorial and only
actually makes the call if it is guaranteed to terminate. Unfortunately,
code generation for factorial_safe fails because there are no code
equations for factorial.

Best regards,
David

Email Gateway (Nov 17 2020 at 18:47):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear David,

I know at least two possibilities:

(* potential solution via typedef: specify separate type for domain of function *)

typedef fun_input = "{n :: int. n ≥ 0}" by auto

setup_lifting type_definition_fun_input

lift_definition num :: "fun_input ⇒ int" is "λ x. x" .

lift_definition sub1 :: "fun_input ⇒ fun_input”
is "λ x. if x = 0 then 0 else x - 1"
by auto

function factorial :: "fun_input ⇒ int" where
"factorial n = (if num n = 0 then 1 else num n * factorial (sub1 n))"
by pat_completeness auto

termination by (relation "measure (λ n. nat (num n))", auto; transfer, auto)

lift_definition create_input :: "int ⇒ fun_input" is
"λ n. if n ≥ 0 then n else 0" by auto

definition factorial_safe :: "int ⇒ int option" where
"factorial_safe n = (if n ≥ 0 then Some (factorial (create_input n)) else None)”

(* during runtime you don’t execute the invariant “n >= 0” in every iteration,
but you repeat the abort-condition in the sub1 function *)

export_code factorial_safe in Haskell

(* or use partial_function and put everything into option-type *)

lemma map_option_mono [partial_function_mono]:
shows "mono_option (λf. map_option X (f y))"
by (smt flat_ord_def fun_ord_def map_option_is_None monotoneI)

partial_function (option) fact_option :: "int ⇒ int option" where
[code]: "fact_option n = (if n = 0 then Some 1 else map_option ((*) n) (fact_option (n - 1)))"

export_code fact_option in Haskell

I hope this helps,
René

Email Gateway (Nov 17 2020 at 19:57):

From: David Kretzmer <david.k@posteo.de>
Dear René,

thank you very much! I especially like the typedef-approach, as it
allows one to nicely specify the preconditions directly in the type,
which are then available to all users of that type. This is pretty much
exactly what I was looking for.

Best regards,
David

Last updated: Jan 04 2025 at 20:18 UTC