Mercurial > cpdt > repo

comparison src/Coinductive.v @ 442:89c67796754e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Undo some overzealous vspace tweaks
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Aug 2012 16:09:37 -0400
parents f923024bd284
children f28bdd8414e0
comparison
equal deleted inserted replaced
441:cbfd23b4364d 442:89c67796754e
27 We spent some time in the last chapter discussing the %\index{Curry-Howard correspondence}%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 _inconsistent_. For an arbitrary proposition [P], we could write: 27 We spent some time in the last chapter discussing the %\index{Curry-Howard correspondence}%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 _inconsistent_. For an arbitrary proposition [P], we could write:
28 [[ 28 [[
29 Fixpoint bad (u : unit) : P := bad u. 29 Fixpoint bad (u : unit) : P := bad u.
30 ]] 30 ]]
31 31
32 %\smallskip{}%This would leave us with [bad tt] as a proof of [P]. 32 This would leave us with [bad tt] as a proof of [P].
33 33
34 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. 34 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.
35 35
36 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; several such approaches are surveyed in Chapter 7. This is a heavyweight solution, and so we would like to avoid it whenever possible. 36 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; several such approaches are surveyed in Chapter 7. This is a heavyweight solution, and so we would like to avoid it whenever possible.
37 37