Mercurial > cpdt > repo

comparison src/Coinductive.v @ 68:943478e5a32d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Template markers for Coinductive
author Adam Chlipala <adamc@hcoop.net>
date Wed, 01 Oct 2008 10:07:14 -0400
parents 55199444e5e7
children f295a64bf9fd
comparison
equal deleted inserted replaced
67:55199444e5e7 68:943478e5a32d
81 :: false 81 :: false
82 :: true :: false :: true :: false :: true :: false :: nil 82 :: true :: false :: true :: false :: true :: false :: nil
83 : list bool 83 : list bool
84 ]] *) 84 ]] *)
85 85
86 (* begin thide *)
86 (** 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. 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.
87 88
88 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. 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.
89 90
90 [[ 91 [[
92 (* end thide *)
91 CoFixpoint looper : stream nat := looper. 93 CoFixpoint looper : stream nat := looper.
94 (* begin thide *)
92 [[ 95 [[
93 Error: 96 Error:
94 Recursive definition of looper is ill-formed. 97 Recursive definition of looper is ill-formed.
95 In environment 98 In environment
96 looper : stream nat 99 looper : stream nat
97 100
98 unguarded recursive call in "looper" 101 unguarded recursive call in "looper"
99 *) 102 *)
103 (* end thide *)
100 104
101 (** 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. 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.
102 106
103 The second rule of guardedness is easiest to see by first introducing a more complicated, but legal, co-fixpoint. *) 107 The second rule of guardedness is easiest to see by first introducing a more complicated, but legal, co-fixpoint. *)
104 108
129 133
130 Section map'. 134 Section map'.
131 Variables A B : Set. 135 Variables A B : Set.
132 Variable f : A -> B. 136 Variable f : A -> B.
133 137
134 (** [[ 138 (* begin thide *)
139 (** [[
140 (* end thide *)
135 141
136 CoFixpoint map' (s : stream A) : stream B := 142 CoFixpoint map' (s : stream A) : stream B :=
137 match s with 143 match s with
138 | Cons h t => interleave (Cons (f h) (map' s)) (Cons (f h) (map' s)) 144 | Cons h t => interleave (Cons (f h) (map' s)) (Cons (f h) (map' s))
139 end. *) 145 end.
146 (* begin thide *)
147 *)
140 148
141 (** 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. 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.
142 150
143 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]. *) 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 (* end thide *)
144 End map'. 153 End map'.
145 154
146 155
147 (** * Infinite Proofs *) 156 (** * Infinite Proofs *)
148 157
154 (** The obvious statement of the equality is this: *) 163 (** The obvious statement of the equality is this: *)
155 164
156 Theorem ones_eq : ones = ones'. 165 Theorem ones_eq : ones = ones'.
157 166
158 (** However, faced with the initial subgoal, it is not at all clear how this theorem can be proved. In fact, it is unprovable. The [eq] predicate that we use is fundamentally limited to equalities that can be demonstrated by finite, syntactic arguments. To prove this equivalence, we will need to introduce a new relation. *) 167 (** However, faced with the initial subgoal, it is not at all clear how this theorem can be proved. In fact, it is unprovable. The [eq] predicate that we use is fundamentally limited to equalities that can be demonstrated by finite, syntactic arguments. To prove this equivalence, we will need to introduce a new relation. *)
168 (* begin thide *)
159 Abort. 169 Abort.
160 170
161 (** Co-inductive datatypes make sense by analogy from Haskell. What we need now is a %\textit{%#<i>#co-inductive proposition#</i>#%}%. That is, we want to define a proposition whose proofs may be infinite, subject to the guardedness condition. The idea of infinite proofs does not show up in usual mathematics, but it can be very useful (unsurprisingly) for reasoning about infinite data structures. Besides examples from Haskell, infinite data and proofs will also turn out to be useful for modelling inherently infinite mathematical objects, like program executions. 171 (** Co-inductive datatypes make sense by analogy from Haskell. What we need now is a %\textit{%#<i>#co-inductive proposition#</i>#%}%. That is, we want to define a proposition whose proofs may be infinite, subject to the guardedness condition. The idea of infinite proofs does not show up in usual mathematics, but it can be very useful (unsurprisingly) for reasoning about infinite data structures. Besides examples from Haskell, infinite data and proofs will also turn out to be useful for modelling inherently infinite mathematical objects, like program executions.
162 172
163 We are ready for our first co-inductive predicate. *) 173 We are ready for our first co-inductive predicate. *)
301 cofix; crush. 311 cofix; crush.
302 (** [[ 312 (** [[
303 313
304 Guarded. *) 314 Guarded. *)
305 Abort. 315 Abort.
316 (* end thide *)
306 317
307 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case. Alternatively, there are tricks that can be played with "hiding" the co-inductive hypothesis. We will see examples of effective co-inductive proving in later chapters. *) 318 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case. Alternatively, there are tricks that can be played with "hiding" the co-inductive hypothesis. We will see examples of effective co-inductive proving in later chapters. *)
308 319
309 320
310 (** * Simple Modeling of Non-Terminating Programs *) 321 (** * Simple Modeling of Non-Terminating Programs *)