diff options
author | Son Ho | 2023-05-15 10:32:46 +0200 |
---|---|---|
committer | Son HO | 2023-06-04 21:54:38 +0200 |
commit | c6e9e51197833a8685c63e6c40d8eabf4e64c22d (patch) | |
tree | 257138e643515e09874f8d7cf6b2e7942622d258 /backends/hol4 | |
parent | 7801bca412767c8b71256ad480ae0e91d3a9392b (diff) |
Make minor modifications
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/divDefLib.sig | 26 | ||||
-rw-r--r-- | backends/hol4/divDefScript.sml | 17 |
2 files changed, 35 insertions, 8 deletions
diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig index 51a09b9c..df879b4b 100644 --- a/backends/hol4/divDefLib.sig +++ b/backends/hol4/divDefLib.sig @@ -9,6 +9,32 @@ divDefExampleTheory. For examples of how to use DefiveDiv, see divDefLibExampleScript. + + Limitations: our encoding has limitations with regards to higher-order functions. More + precisely, the following definition wouldn't be accepted, because we don't know how + “MAP” would use ‘explore_tree’, meaning we can't prove the validity property required + by the fixed point upon defining ‘explore_tree’ and ‘explore_node’: + + {[ + Datatype tree: + | Leaf : int + | Node : tree list + + explore_tree (t : tree) : tree = + case t of + Leaf i => Leaf i + | Node ns => Node (explore_node ns) + + explore_node (ns : tree list) : tree list = + MAP explore_tree ns (* This is not supported *) + ]} + + *However*, our encoding does allow defining a function ‘f’ *then* giving it + as argument to a higher-order function such as ‘MAP’. + + Remark: "Partial recursive functions in higher-order logic", Alexander Krauss, + introduces an interesting approach by means of an inductive. It could be + interesting to try and compare. *) signature divDefLib = diff --git a/backends/hol4/divDefScript.sml b/backends/hol4/divDefScript.sml index c742fb1f..b80aa2bf 100644 --- a/backends/hol4/divDefScript.sml +++ b/backends/hol4/divDefScript.sml @@ -20,35 +20,36 @@ val _ = new_theory "divDef" *======================*) (* An auxiliary operator which uses some fuel *) -val fix_fuel_def = Define ‘ +Definition fix_fuel_def: (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧ (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x) -’ +End (* An auxiliary predicate *) -val fix_fuel_P_def = Define ‘ +Definition fix_fuel_P_def: fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x)) -’ +End (* The fixed point operator *) -val fix_def = Define ‘ +Definition fix_def: fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge -’ +End (* A validity condition. If a function body ‘f’ satisfies this condition, then we have the fixed point equation ‘fix f = f (fix f)’ (see [fix_fixed_eq]). *) -val is_valid_fp_body_def = Define ‘ +Definition is_valid_fp_body_def: (is_valid_fp_body (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) = F) ∧ (is_valid_fp_body (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) = ∀x. (∀g h. f g x = f h x) ∨ (∃ h y. is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od)) -’ +End + (*====================== * Lemmas *======================*) |