13
$\begingroup$

Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term will reduce to its canonical normal form, e.g. if $n : \mathbb{N}$ is true, then $n$ must reduce to a term of the form $(succ ... (succ (0)))$. But when postulating an axiom - say the function extensionality axiom funext - we just add a new constant to the system

$$ funext : \Pi_{x : A} f (x) = g (x) \to f = g$$

that will just "magically" produces a proof of $f = g$ from any proof of $\Pi_{x : A} f (x) = g (x)$, without any computational meaning at all (in the sense that we cannot extract any code from them?)

But why is this "bad"?

For funext, I read in this coq entry and this mathoverflow question that it will cause the system to either loose canonicity or decidable checking. The coq entry seems to present a good example, but I still would like some more references on that - and somehow I can't find any.

How is that adding extra axioms could cause CIC to have a worse behavior? Any practical examples would be great. (For example, the Univalence Axiom?) I am afraid in this question is too soft, but if anyone could shed some light on those issues or give me some references would be great!

PS: The coq entry mentions that "Thierry Coquand already observed that pattern matching over intensional families is inconsistent with extensionality in the mid 90ies." Does anyone know in which paper or something?

|cite|improve this question
$\endgroup$
7
$\begingroup$

One first reason to reject axioms is that they might be inconsistent. Even for the axioms that are proved consistent, some of them have a computational interpretation (we know how to extend definitional equality with a reduction principle for them) and some do not -- those break canonicity. This is "bad" for different reasons:

  • In theory, canonicity lets you prove things about the values of your language, without having to go to a specific model. This is a very satisfying property to have thinking about your system; in particular, it supports claims about the real world -- we can think of the nat type as formalized in the system as really "natural numbers" because we can prove that its closed normal inhabitants really are natural numbers. Otherwise it's easy to think that you modelled something correctly in your system, but actually be working with different objects.

  • In practice, reduction is a major asset of dependent type theories, because it makes proof easy. Proving a propositional equality can be arbitrarily difficult, while proving a definitional equality is (less often possible) but much easier, as the proof term is trivial. More generally, computation is a core aspect of the user experience of a proof assistant, and it is common to define things just so they reduce correctly as you expect. (You don't need axioms to make computation difficult; for example, using the conversion principle on propositional equalities can already block reductions). The entire business of proof by reflection is based on the use of computation to help proofs. This is a major difference in power and convenience with respect to other logics-based proof assistant (eg. HOL-light, which only supports equality reasoning; or see Zombie for a different approach), and using unchecked axioms, or other programming styles, can get you out of this comfort zone.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ +1 Thanks for your answer! Could you give me some examples of axioms that have a computational interpretation (or maybe any reference for the subject)? $\endgroup$ – StudentType Dec 30 '15 at 9:02
  • $\begingroup$ One example of axiom that has a computational interpretation is Prop-Irrelevance: claiming that all inhabitants of some family of types (in this precise case, those of the kind Prop in the Coq proof assistants, that correspond to purely logical statements; Prop-Irrelevance corresponds to ignoring the internal structure of the proofs of those statements) are equal can be done mostly by not caring about them anymore, it need not affect computation -- but it needs to be done carefully to not make the system inconsistent either. $\endgroup$ – gasche Jan 2 '16 at 19:19
  • $\begingroup$ Another family of computational intepretation comes from correspondences between classical reasoning and control effect. The better-known part of this is that the excluded middle can be given a computational semantics by continuation capture, but there are restricted forms of control (exceptions at positive types) that give finer-grained logical principles (eg. Markov's Principle). See Hugo Herbelin's An intuitionistic logic that proves Markov's principle, 2010. $\endgroup$ – gasche Jan 2 '16 at 19:25
5
$\begingroup$

To understand why extending a theorem prover with some axioms can cause problems, it is also interesting to see when it is benign to do so. Two cases come to mind and they both have to do with the fact that we do not care about the computational behaviour of the postulates.

  • In Observational Type Theory, it is possible to postulate a proof of any consistent Prop without losing canonicity. Indeed, all the proofs are considered equal and the system enforces this by completely refusing to look at the terms. As a consequence, the fact that a proof was built by hand or simply postulated bears no consequence. A typical example would be the proof of "cohesion": if we have a proof eq that A = B : Type then for any t of type A, t == coerce A B eq t where coerce simply transports a term along an equality proof.

  • In MLTT, one can postulate any Negative consistent axiom without loss of canonicity. The intuition behind this is that negative axioms (axioms of the form A -> False) are only ever used to dismiss irrelevant branches. If the axiom is consistent, then it can only be used in branches which are indeed irrelevant and will therefore never be taken when evaluating the terms.

|cite|improve this answer
$\endgroup$
4
$\begingroup$

A practical example of an axiom behaving badly you ask, what about this?

 0 = 1

The Coquand paper referred to might be [ 1 ], where he shows that dependent ITT (Martin-Löf's intuitionistic type theory) extended with pattern matching allows you to prove UIP (axiom of uniqueness of identity proofs). Later Streicher and Hoffmann [ 2 ] present a model of in ITT that falsifies UIP. Hence pattern matching is not a conservative extension of ITT.

  1. T. Coquand, Pattern matching with dependent types.

  2. M. Hofmann, T. Streicher, The groupoid interpretation of type theory.

|cite|improve this answer
$\endgroup$

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.