diff options
Diffstat (limited to 'backends/hol4/divDefLib.sig')
-rw-r--r-- | backends/hol4/divDefLib.sig | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig new file mode 100644 index 00000000..d63d7771 --- /dev/null +++ b/backends/hol4/divDefLib.sig @@ -0,0 +1,93 @@ +signature divDefLib = +sig + include Abbrev + + (* Define a (group of mutually recursive) function(s) which uses an error + monad and is potentially divergent. + + We encode divergence in such a way that we don't have to prove that the + functions we define terminate *upon defining them*, and can do those proofs + in an extrinsic way later. It works as follows. + + Let's say you want to define the following “even” and “odd” functions + which operate on *integers*: + + {[ + even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\ + + odd (i : int) : bool result = if i = 0 then Return F else even (i - 1) + ]} + + It is easy to prove that the functions terminate provided the input is >= 0, + but it would require to be able to define those functions in the first place! + + {!DefineDev} consequently does the following. + + It first defines versions of “even” and “odd” which use fuel: + {[ + even___fuel (n : num) (i : int) : bool result = + case n of 0 => Diverge + | SUC m => if i = 0 then Return T else odd___fuel m (i - 1) /\ + + odd___fuel (n : num) (i : int) : bool result = + case n of 0 => Diverge + | SUC m => if i = 0 then Return F else even___fuel m (i - 1) + ]} + + Those functions trivially terminate. + + Then, provided we have the following auxiliary definition: + {[ + is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F + ]} + + we can define the following predicates, which tell us whether “even___fuel” + and “odd___fuel” terminate on some given inputs: + {[ + even___P i n = ~(is_diverge (even___fuel n i)) /\ + + odd___P i n = ~(is_diverge (odd___fuel n i)) + ]} + + We can finally define “even” and “odd” as follows. We use the excluded + middle to test whether there exists some fuel on which the function + terminates: if there exists such fuel, we call the "___fuel" versions + of “even” and “odd” with it (we use the least upper bound, to be more + precise). Otherwise, we simply return “Diverge”. + {[ + even i = + if (?n. even___P i n) then even___fuel ($LEAST (even___P i)) i + else Diverge /\ + + odd i = + if (?n. odd___P i n) then odd___fuel ($LEAST (odd___P i)) i + else Diverge + ]} + + The definitions above happen to satisfy the rewriting theorem we want: + {[ + even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\ + + odd (i : int) : bool result = if i = 0 then Return F else even (i - 1) + ]} + + Moreover, if we prove a lemma which states that they don't evaluate to + “Diverge” on some given inputs (trivial recursion if we take “i >= 0” + and reuse the rewriting theorem just above), then we effectively proved + that the functions terminate on those inputs. + + Remark: + ======= + {!DefineDiv} introduces all the auxiliary definitions we need and + automatically performs the proofs. A crucial intermediate lemma + we need in order to establish the last theorem is that the "___fuel" + versions of the functions are monotonic in the fuel. + More precisely: + {[ + !n m. n <= m ==> + (!ls i. even___P ls i n ==> even___fuel n ls i n = even___fuel m ls i n) /\ + (!ls i. odd___P ls i n ==> odd___fuel n ls i n = odd___fuel m ls i n) + ]} + *) + val DefineDiv : term quotation -> thm list +end |