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

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é

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: Sep 25 2021 at 08:21 UTC