Mercurial > cpdt > repo
comparison src/GeneralRec.v @ 496:88688402dc82
Pass through Chapter 7
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 20 Jan 2013 07:35:35 -0500 |
| parents | f38a3af9dd17 |
| children | 3b21f4395178 |
comparison
equal
deleted
inserted
replaced
| 495:b7419a10e52e | 496:88688402dc82 |
|---|---|
| 899 | 899 |
| 900 << | 900 << |
| 901 Error: Universe inconsistency. | 901 Error: Universe inconsistency. |
| 902 >> | 902 >> |
| 903 | 903 |
| 904 The problem has to do with rules for inductive definitions that we still study in more detail in Chapter 12. Briefly, recall that the type of the constructor [Bnd] quantifies over a type [B]. To make [testCurriedAdd] work, we would need to instantiate [B] as [nat -> comp nat]. However, Coq enforces a %\emph{predicativity restriction}% that (roughly) no quantifier in an inductive or co-inductive type's definition may ever be instantiated with a term that contains the type being defined. Chapter 12 presents the exact mechanism by which this restriction is enforced, but for now our conclusion is that [comp] is fatally flawed as a way of encoding interesting higher-order functional programs that use general recursion. *) | 904 The problem has to do with rules for inductive definitions that we will study in more detail in Chapter 12. Briefly, recall that the type of the constructor [Bnd] quantifies over a type [B]. To make [testCurriedAdd] work, we would need to instantiate [B] as [nat -> comp nat]. However, Coq enforces a %\emph{predicativity restriction}% that (roughly) no quantifier in an inductive or co-inductive type's definition may ever be instantiated with a term that contains the type being defined. Chapter 12 presents the exact mechanism by which this restriction is enforced, but for now our conclusion is that [comp] is fatally flawed as a way of encoding interesting higher-order functional programs that use general recursion. *) |
| 905 | 905 |
| 906 | 906 |
| 907 (** * Comparing the Alternatives *) | 907 (** * Comparing the Alternatives *) |
| 908 | 908 |
| 909 (** We have seen four different approaches to encoding general recursive definitions in Coq. Among them there is no clear champion that dominates the others in every important way. Instead, we close the chapter by comparing the techniques along a number of dimensions. Every technique allows recursive definitions with termination arguments that go beyond Coq's built-in termination checking, so we must turn to subtler points to highlight differences. | 909 (** We have seen four different approaches to encoding general recursive definitions in Coq. Among them there is no clear champion that dominates the others in every important way. Instead, we close the chapter by comparing the techniques along a number of dimensions. Every technique allows recursive definitions with termination arguments that go beyond Coq's built-in termination checking, so we must turn to subtler points to highlight differences. |