16
$\begingroup$

We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A := \mu F$ to be the "inductive definition" of $A$. Moreover, monotonicity of $F$ allows us to reason with the "principle of induction" to determine when a set contains $A$ (i.e. when a property universally holds on $A$).

In Coq this corresponds to writing an $\mathtt{Inductive}$ definition of $A$ with explicit introduction terms. While this definition denotes a particular function $F$, that function is not necessarily monotonic. Coq therefore employs some syntactic checks to guarantee the "well-formedness" of the definition. To some approximation, it rejects occurrences of $A$ in negative positions in the types of the introduction terms.

(If my understanding up to this point is flawed, please correct me!)

First, some questions in the context of Coq:

1) Does the syntactic check in Coq merely serve to ensure that the definition of $A$ is predicative? (If so, is impredicativity the only way in which the definition would be ill-defined?) Or is it checking for monotonicity? (Correspondingly, is non-monotonicity what might kill it?)

2) Does such a negative occurrence of $A$ necessarily imply that $A$'s definition is impredicative/non-monotonic? Or is Coq simply unable to verify that it's well-defined in that case?

And more generally:

3) What is the relation between predicativity of an inductive definition and monotonicity of that definition's generating function? Are they two sides of the same coin? Are they unrelated? Informally, which one matters more?

$\endgroup$
14
$\begingroup$

No, in this case, predicativity and monotonicity are not closely related.

The positivity check in Coq/Adga serves to ensure that you are taking the least fixed point of a monotonic thing, roughly.

Here's how to think of inductive types in terms of lattices and monotone operators. Recall that the Knaster-Tarski theorem says that on a complete lattice $L$, every monotone operator $f : L \to L$ has a least fixed point $\mu(f)$. Next, we can think of the types in a type theory as forming a lattice under provability. That is, type $S$ is below $T$ if the truth of $S$ entails that of $T$. Now, what we would like to do is to take a monotone operator $F$ on types, and use Knaster-Tarski to get out an interpretation of the least fixed point of this operator $\mu(F)$.

However, types in type theory aren't just a lattice: they form a category. That is, given two types $S$ and $T$, there are potentially many ways for $S$ to be below $T$, with one way for each proof $e : S \to T$. So a type operator $F$ also has to do something sensible on these proofs. The appropriate generalization of monotonicity is functoriality. That is, we want $F$ to have an operator on types, and also to have an action on proofs, such that if $e : S \to T$, then $F(e) : F(S) \to F(T)$.

Now, functoriality is preserved by sums and products (ie., if $F$ and $G$ are endofunctors on types, then $F+G$ and $F\times G$ (acting pointwise) are also functors on types (assuming we have sums and products in our algebra of types). However, it is not preserved by the function space, since the exponential bifunctor $F \to G$ is contravariant in its left argument. So when you write an inductive type definition, you are defining a functor to take a least fixed point of. To ensure that it is indeed a functor, you need to rule out occurences of the recursive parameter on the left-hand-side of function spaces --- hence the positivity check.

Impredicativity (in the sense of System F) is generally avoided, because it is a principle that forces you to choose between classical logic and set-theoretic models. You can't interpret types as sets in classical set theory if you have F-style indexing. (See Reynolds' famous "Polymorphism is Not Set-Theoretic".)

Categorically, F-style impredicativity says that the category of types and terms forms a small complete category (that is, homs and objects are both sets, and limits of all small diagrams exist). Classically this forces a category to be a poset. Many constructivists are constructive because they want their theorems to hold in more systems than just classical logic, and so they don't want to prove anything that would be classically false. Hence they are leery of impredicative polymorphism.

However, polymorphism lets you say many conditions that are classically "large" internally to your type theory -- and positivity is one of them! A type operator $F$ is functorial, if you can produce a polymorphic term:

$$ \mathsf{Fmap} : \forall \alpha, \beta.\; (\alpha \to \beta) \to (F(\alpha) \to F(\beta)) $$

See how this corresponds to functoriality? IMO, this would be a very nice option to have in Coq, since it would let you do generic programming much more easily. The syntactic nature of the positivity check is a big hindrance to generic programming, and I would be happy to trade the possibility of classical axioms for more flexible functional programs.

EDIT: The question you are asking about the difference between Prop and Set arises from the fact that the Coq developers want to permit you think about Coq theorems in naive set-theoretic terms if you want, without forcing you to do so. Technically, they split Prop and Set, and then prohibit sets from depending on the computational content of Prop.

So you can interpret Prop as truth values in ZFC, which are the booleans true and false. In this world, all proofs of propositions are equal, and so obviously you should not be able to branch on the proof of a proposition. So the prohibition on sets depending on the computational content of proofs of Prop is totally sensible. Furthermore, the 2-element boolean lattice is obviously a complete lattice, so it should support impredicative indexing, since arbitrary set-valued meets exist. The predicativity restriction on Sets arises from the fact (mentioned above) that F-style indexing is degenerate in classical set-theoretic models.

Coq has other models (it's constructive logic!) but the point is that off the shelf it will never prove anything that a classical mathematician would be puzzled by.

$\endgroup$
  • $\begingroup$ Thanks for your response, Neel. Your definition of "inductive definition" seems to correspond more to the "initial $F$-algebra" approach: instead of monotonic functions (which say nothing of proofs and computational content), we concern ourselves with (the more general notion of) functors. So rather than checking for monotonicity, Coq is really checking for functoriality. However, if predicativity is not in question, why does Coq distinguish between the positive-occurrence-check for defined objects in $\mathrm{Prop}$ and those in $\mathrm{Set}$ or $\mathrm{Type}$? $\endgroup$ – Scott Kilpatrick Apr 13 '11 at 14:22
  • $\begingroup$ I don't understand your question: Coq hates Inductive Blah : Prop := Foo : (Blah -> Blah) -> Blah same as anything else? $\endgroup$ – Neel Krishnaswami Apr 13 '11 at 14:56
  • 1
    $\begingroup$ Ah, perhaps I am mistaking the positivity check for another check related to impredicativity. Consider Inductive prop : Prop := prop_intro : Prop -> prop. vs. Inductive set : Set := set_intro: Set -> set.. Why the distinction if predicativity is of no concern to inductive definition? $\endgroup$ – Scott Kilpatrick Apr 13 '11 at 15:04
  • $\begingroup$ @ScottKilpatrick: that’s indeed a different check, and about (im)predicativity. Impredicative strong Sigma-types allow encoding Girard’s paradox, so a datatype storing a member of some universe, say Type@{i}, must live in a bigger universe, at least Type@{i+1}. $\endgroup$ – Blaisorblade Mar 31 at 17:14
6
$\begingroup$

There is a very deep connection between inductive definitions and impredicativity, but my understanding is that in the context of what you are talking about (im)predicativity is not particularly relevant and the test is purely to guarantee monotonicity, so that fixed point theory can be applied, namely, that the principle of induction is well-defined. (I'm willing to be corrected on this point.)

The relationship between impredicativity and inductive definitions is explored in this talk by Coquand. It goes back to some results from the 50s by G. Takeuti that impredicative definitions can be reduced to inductive definitions. The book

  • Proof Theory of Impredicative Subsystems of Analysis - Monographs and Textbooks in Physical Science 2 by W. Buchholz, K. Schutte

gives a good analysis of the topic, if you can get your hands on it. These slides give an overview.

$\endgroup$
4
$\begingroup$

Just to complete the excellent explanation by Neil, impredicativity has a "soft" sense: the definition of sets or collections by using a reference to themselves. In that sense:

Inductive Lam : Set :=
| Var : Nat -> Lam
| App : Lam -> Lam -> Lam
| Abs : (Lam -> Lam) -> Lam

is an impredicative definition, as it defines an inductive type, Lam using a function space (Lam -> Lam) which refers to the collection itself. In this situation, impredicativity is harmful: it is possible to use Cantor's theorem to prove False. In fact this is the same brand of impredicativity which discounts naive Set Theory as a consistent foundation for mathematics. It is therefore disallowed in Coq. Another form of impredicativity is allowed, as you are aware:

Definition Unit : Prop := forall X:Prop, X -> X

The definition of Unit as a proposition makes reference to the collection of all Propositions of which it is a member. However, for reasons somewhat obscure to me, this impredicativity is not harmful as it is present in ZFC (in the form of unbounded comprehension) which is not known to be inconsistent.

In conclusion, negative occurences of inductive types in definitions is a form of impredicativity, but not the one usually referred to when speaking of CoC as an impredicative framework.

$\endgroup$
  • $\begingroup$ I understand you're saying that ZFC has unbounded comprehension. But that sounds wrong — math.stackexchange.com/q/24507/79293. Chlipala discusses this when discussing -impredicative-set in his book: adam.chlipala.net/cpdt/html/Universes.html, and mentions some restrictions on elimination, but this is obscure to me as well. $\endgroup$ – Blaisorblade May 25 '14 at 9:37
  • 1
    $\begingroup$ You shouldn't confuse unrestricted comprehension and unbounded comprehension. The latter just means you can form subsets of a given set $A$ by taking the extension of any formula with one free variable, not just formulae with bounded quantifiers (quantifiers of the form $\forall x\in B$ or $\exists x\in B$). The bounded version is significantly weaker, as things like least upper bounds are hard/impossible to define. See this for example. $\endgroup$ – cody May 25 '14 at 15:38
  • $\begingroup$ Ah, thanks! I also see how the above impredicativity matches the one in ZFC (though the mapping I'm using is probably too naive). Can you add the link in the answer? $\endgroup$ – Blaisorblade May 26 '14 at 15:34
  • $\begingroup$ Unfortunately this seems hard to Google (or I don't know the right keywords). What's worse, both Wikipedia and nLab distinguish between "restricted comprehension" (in ZFC, en.wikipedia.org/wiki/Axiom_schema_of_specification) and "restricted/bounded separation" (what you linked to). See ncatlab.org/nlab/show/axiom+of+separation. But all this terminology looks like a misunderstanding waiting to happen — I usually reason that "separation ~ comprehension", like you and the author mathforum.org/kb/message.jspa?messageID=4492130 do, too. $\endgroup$ – Blaisorblade May 26 '14 at 15:38
  • $\begingroup$ Maybe the best keywords for these kinds of discussions are "Constructive Set Theory", see e.g. wikipedia, or this very nice article by Rathjen. $\endgroup$ – cody May 26 '14 at 20:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.