Mercurial > cpdt > repo

comparison src/Coinductive.v @ 202:8caa3b3f8fc0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Feedback from Peter Gammie
author Adam Chlipala <adamc@hcoop.net>
date Sat, 03 Jan 2009 19:57:02 -0500
parents df289eb8ef76
children f05514cc6c0d
comparison
equal deleted inserted replaced
201:a2b14ba218a7 202:8caa3b3f8fc0
20 20
21 (** In lazy functional programming languages like Haskell, infinite data structures are everywhere. Infinite lists and more exotic datatypes provide convenient abstractions for communication between parts of a program. Achieving similar convenience without infinite lazy structures would, in many cases, require acrobatic inversions of control flow. 21 (** In lazy functional programming languages like Haskell, infinite data structures are everywhere. Infinite lists and more exotic datatypes provide convenient abstractions for communication between parts of a program. Achieving similar convenience without infinite lazy structures would, in many cases, require acrobatic inversions of control flow.
22 22
23 Laziness is easy to implement in Haskell, where all the definitions in a program may be thought of as mutually recursive. In such an unconstrained setting, it is easy to implement an infinite loop when you really meant to build an infinite list, where any finite prefix of the list should be forceable in finite time. Haskell programmers learn how to avoid such slip-ups. In Coq, such a laissez-faire policy is not good enough. 23 Laziness is easy to implement in Haskell, where all the definitions in a program may be thought of as mutually recursive. In such an unconstrained setting, it is easy to implement an infinite loop when you really meant to build an infinite list, where any finite prefix of the list should be forceable in finite time. Haskell programmers learn how to avoid such slip-ups. In Coq, such a laissez-faire policy is not good enough.
24 24
25 We spent some time in the last chapter discussing the Curry-Howard isomorphism, where proofs are identified with functional programs. In such a setting, infinite loops, intended or otherwise, are disastrous. If Coq allowed the full breadth of definitions that Haskell did, we could code up an infinite loop and use it to prove any proposition vacuously. That is, the addition of general recursion would make CIC %\textit{%#<i>#inconsistent#</i>#%}%. 25 We spent some time in the last chapter discussing the Curry-Howard isomorphism, where proofs are identified with functional programs. In such a setting, infinite loops, intended or otherwise, are disastrous. If Coq allowed the full breadth of definitions that Haskell did, we could code up an infinite loop and use it to prove any proposition vacuously. That is, the addition of general recursion would make CIC %\textit{%#<i>#inconsistent#</i>#%}%. For an arbitrary proposition [P], we could write:
26
27 [[
28
29 Fixpoint bad (u : unit) : P := bad u.
30
31 This would leave us with [bad tt] as a proof of [P].
26 32
27 There are also algorithmic considerations that make universal termination very desirable. We have seen how tactics like [reflexivity] compare terms up to equivalence under computational rules. Calls to recursive, pattern-matching functions are simplified automatically, with no need for explicit proof steps. It would be very hard to hold onto that kind of benefit if it became possible to write non-terminating programs; we would be running smack into the halting problem. 33 There are also algorithmic considerations that make universal termination very desirable. We have seen how tactics like [reflexivity] compare terms up to equivalence under computational rules. Calls to recursive, pattern-matching functions are simplified automatically, with no need for explicit proof steps. It would be very hard to hold onto that kind of benefit if it became possible to write non-terminating programs; we would be running smack into the halting problem.
28 34
29 One solution is to use types to contain the possibility of non-termination. For instance, we can create a "non-termination monad," inside which we must write all of our general-recursive programs. In later chapters, we will spend some time on this idea and its applications. For now, we will just say that it is a heavyweight solution, and so we would like to avoid it whenever possible. 35 One solution is to use types to contain the possibility of non-termination. For instance, we can create a "non-termination monad," inside which we must write all of our general-recursive programs. In later chapters, we will spend some time on this idea and its applications. For now, we will just say that it is a heavyweight solution, and so we would like to avoid it whenever possible.
30 36
81 :: false 87 :: false
82 :: true :: false :: true :: false :: true :: false :: nil 88 :: true :: false :: true :: false :: true :: false :: nil
83 : list bool 89 : list bool
84 ]] *) 90 ]] *)
85 91
86 (* begin thide *)
87 (** So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks. However, there are important restrictions that are dual to the restrictions on the use of inductive types. Fixpoints %\textit{%#<i>#consume#</i>#%}% values of inductive types, with restrictions on which %\textit{%#<i>#arguments#</i>#%}% may be passed in recursive calls. Dually, co-fixpoints %\textit{%#<i>#produce#</i>#%}% values of co-inductive types, with restrictions on what may be done with the %\textit{%#<i>#results#</i>#%}% of co-recursive calls. 92 (** So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks. However, there are important restrictions that are dual to the restrictions on the use of inductive types. Fixpoints %\textit{%#<i>#consume#</i>#%}% values of inductive types, with restrictions on which %\textit{%#<i>#arguments#</i>#%}% may be passed in recursive calls. Dually, co-fixpoints %\textit{%#<i>#produce#</i>#%}% values of co-inductive types, with restrictions on what may be done with the %\textit{%#<i>#results#</i>#%}% of co-recursive calls.
88 93
89 The restriction for co-inductive types shows up as the %\textit{%#<i>#guardedness condition#</i>#%}%, and it can be broken into two parts. First, consider this stream definition, which would be legal in Haskell. 94 The restriction for co-inductive types shows up as the %\textit{%#<i>#guardedness condition#</i>#%}%, and it can be broken into two parts. First, consider this stream definition, which would be legal in Haskell.
90 95
91 [[ 96 [[
92 (* end thide *)
93 CoFixpoint looper : stream nat := looper. 97 CoFixpoint looper : stream nat := looper.
94 (* begin thide *)
95 [[ 98 [[
96 Error: 99 Error:
97 Recursive definition of looper is ill-formed. 100 Recursive definition of looper is ill-formed.
98 In environment 101 In environment
99 looper : stream nat 102 looper : stream nat
100 103
101 unguarded recursive call in "looper" 104 unguarded recursive call in "looper"
102 *) 105 *)
103 (* end thide *) 106
104 107
105 (** The rule we have run afoul of here is that %\textit{%#<i>#every co-recursive call must be guarded by a constructor#</i>#%}%; that is, every co-recursive call must be a direct argument to a constructor of the co-inductive type we are generating. It is a good thing that this rule is enforced. If the definition of [looper] were accepted, our [approx] function would run forever when passed [looper], and we would have fallen into inconsistency. 108 (** The rule we have run afoul of here is that %\textit{%#<i>#every co-recursive call must be guarded by a constructor#</i>#%}%; that is, every co-recursive call must be a direct argument to a constructor of the co-inductive type we are generating. It is a good thing that this rule is enforced. If the definition of [looper] were accepted, our [approx] function would run forever when passed [looper], and we would have fallen into inconsistency.
106 109
107 The second rule of guardedness is easiest to see by first introducing a more complicated, but legal, co-fixpoint. *) 110 The second rule of guardedness is easiest to see by first introducing a more complicated, but legal, co-fixpoint. *)
108 111
135 Variables A B : Set. 138 Variables A B : Set.
136 Variable f : A -> B. 139 Variable f : A -> B.
137 140
138 (* begin thide *) 141 (* begin thide *)
139 (** [[ 142 (** [[
140 (* end thide *)
141 143
142 CoFixpoint map' (s : stream A) : stream B := 144 CoFixpoint map' (s : stream A) : stream B :=
143 match s with 145 match s with
144 | Cons h t => interleave (Cons (f h) (map' s)) (Cons (f h) (map' s)) 146 | Cons h t => interleave (Cons (f h) (map' s)) (Cons (f h) (map' s))
145 end. 147 end.
146 (* begin thide *)
147 *) 148 *)
148 149
149 (** We get another error message about an unguarded recursive call. This is because we are violating the second guardedness condition, which says that, not only must co-recursive calls be arguments to constructors, there must also %\textit{%#<i>#not be anything but [match]es and calls to constructors of the same co-inductive type#</i>#%}% wrapped around these immediate uses of co-recursive calls. The actual implemented rule for guardedness is a little more lenient than what we have just stated, but you can count on the illegality of any exception that would enhance the expressive power of co-recursion. 150 (** We get another error message about an unguarded recursive call. This is because we are violating the second guardedness condition, which says that, not only must co-recursive calls be arguments to constructors, there must also %\textit{%#<i>#not be anything but [match]es and calls to constructors of the same co-inductive type#</i>#%}% wrapped around these immediate uses of co-recursive calls. The actual implemented rule for guardedness is a little more lenient than what we have just stated, but you can count on the illegality of any exception that would enhance the expressive power of co-recursion.
150 151
151 Why enforce a rule like this? Imagine that, instead of [interleave], we had called some other, less well-behaved function on streams. Perhaps this other function might be defined mutually with [map']. It might deconstruct its first argument, retrieving [map' s] from within [Cons (f h) (map' s)]. Next it might try a [match] on this retrieved value, which amounts to deconstructing [map' s]. To figure out how this [match] turns out, we need to know the top-level structure of [map' s], but this is exactly what we started out trying to determine! We run into a loop in the evaluation process, and we have reached a witness of inconsistency if we are evaluating [approx (map' s) 1] for any [s]. *) 152 Why enforce a rule like this? Imagine that, instead of [interleave], we had called some other, less well-behaved function on streams. Perhaps this other function might be defined mutually with [map']. It might deconstruct its first argument, retrieving [map' s] from within [Cons (f h) (map' s)]. Next it might try a [match] on this retrieved value, which amounts to deconstructing [map' s]. To figure out how this [match] turns out, we need to know the top-level structure of [map' s], but this is exactly what we started out trying to determine! We run into a loop in the evaluation process, and we have reached a witness of inconsistency if we are evaluating [approx (map' s) 1] for any [s]. *)
357 | R1 => Regmap v (VR2 rm) 358 | R1 => Regmap v (VR2 rm)
358 | R2 => Regmap (VR1 rm) v 359 | R2 => Regmap (VR1 rm) v
359 end. 360 end.
360 End regmap. 361 End regmap.
361 362
362 (** Now comes the interesting part. We define a co-inductive semantics for programs. The definition itself is not surprising. We could change [CoInductive] to [Inductive] and arrive at a valid semantics that only covers terminating program executions. Using [CoInductive] admits infinite derivations for infinite executions. *) 363 (** Now comes the interesting part. We define a co-inductive semantics for programs. The definition itself is not surprising. We could change [CoInductive] to [Inductive] and arrive at a valid semantics that only covers terminating program executions. Using [CoInductive] admits infinite derivations for infinite executions. An application [run rm is v] means that, when we run the instructions [is] starting with register map [rm], either execution terminates with result [v] or execution runs safely forever. (That is, the choice of [v] is immaterial for non-terminating executions.) *)
363 364
364 Section run. 365 Section run.
365 Variable prog : program. 366 Variable prog : program.
366 367
367 CoInductive run : regmap nat -> instrs -> nat -> Prop := 368 CoInductive run : regmap nat -> instrs -> nat -> Prop :=