blob: d63d77719d84b3a27b7bd7aa8e43944c6e3532b0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
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
|
