[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

## Advertising

hi paul, this sort of example well exemplifies the fundamental conceptual difference between nuprl and coq. the core of coq is martin-lof's itt. the system ett is, by definition, itt extended with equality reflection and uniqueness of identity proofs. it is often misrepresented that nuprl is ett, usually on passage to a "critique" of nuprl on the grounds that the typing judgment in nuprl is not decidable, and supposedly this is a cardinal principle that ought to hold for all type theories. but nuprl is not ett. say what you want about ett, but it has no bearing on nuprl. the reason is that the nuprl typing relation (written "in" in ascii, written "\in" in print) is not at all intended to be, and never was intended to be, the coq typing relation (written ":" in both ascii and in print). comparing the two to each other is not really sensible; each is trying to express a different thing. in nuprl it would be the case that t_m in (nat->bool), but as you mention it would not be the case that in coq t_m : (nat->bool). the reason is that the typing judgment in nuprl represents a statement about the a priori given execution behavior of a program, whereas in coq the analogous statement is about the grammar of programs themselves, before they ever get to be thought of as having execution behavior. put in other terms, nuprl is a theory of TRUTH, and is based on the semantic propositions-as-types principle; it can be seen as an attempt to formulate brouwer's notion of truth in intuitionistic mathematics. coq, on the other hand, is a theory of FORMAL PROOF, and is based on the syntactic propositions-as-types principle; it is an account of proof, not an account of truth. it can be seen as a full development of heyting's formalization of intuitionistic mathematics, which brouwer in fact rejected, but that's neither here nor there. you are saying, if i understood correctly, that certain facts are true, and these facts can be independent of a particular proof theory. eg, the goedel sentence is true, but is not provable in HA. (all the axioms of HA are true, and that fact cannot be doubted without simply doubting everything in mathematics.) if one starts with a partial structural (syntactic) type theory with general recursive types, then one can consider nuprl's types as relations over the terms of a particular recursive type, essentially mu t.(t->t) or elaborations thereof. but the syntactic type theory cannot be construed as a logic, or rather only as an inconsistent logic. in nuprl partiality is handled using "bar types", which predate the lifting monad, but which are essentially that concept phrased in an operational setting. there is a type of unevaluated computations of a type, so that partial functions A -` B are total functions A -> [B] (written \overline{B} in nuprl). hope this helps, and i hope i haven't misconstrued your question. bob ----------------------------- Prof Robert Harper Carnegie Mellon CSD r...@cs.cmu.edu ----------------------------- On Aug 23, 2014, at 12:01, Paul Levy <p.b.l...@cs.bham.ac.uk> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > > On 23 Aug 2014, at 00:42, Paul Levy wrote: > >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> Dear colleagues, >> >> I would like to present a polemic for your consideration. >> >> Let T : (nat * nat) -> bool be the primitive recursive predicate where >> T(m,n) means that Turing machine number m (with no arguments) executes for >> at least n steps. >> >> Say that a number m is "terminating" if for some n, not T(m,n), and >> "HA-divergent" if it is provable in Heyting arithmetic that for all n, >> T(m,n). >> >> (This happens to coincide with provability in Peano arithmetic but I am >> using a constructive system for the sake of the argument.) >> >> In a dependent type system with boolean type and natural number type, for >> every number m let t_m be the term >> >> lambda x:nat. if T(m,x) then true else 7 >> >> Say that a system is "typing HA-complete" if |- t_m : nat -> bool is >> provable for all HA-divergent m. >> >> Say that a system is "typing decidable" if the judgement |- t : A, where t >> is a closed term and A a closed term > > Sorry, that should be "where t is a closed term and A a closed type" > >> , is decidable. >> >> A system cannot be both typing decidable and typing HA-complete, because >> termination and HA-divergence are recursively inseparable properties. >> Martin-Löf's intensional type theory is typing decidable by design and >> therefore not typing HA-complete. >> >> Now the polemic: >> >> In my opinion typing HA-completeness is a very minimal completeness property >> to require of a dependently typed system (with nat), and I cannot see the >> interest of a system that lacks it. Advocates of typing decidability will >> of course disagree. A curious feature of this disagreement is the contrast >> with traditional arguments over the acceptability of individual judgements. >> (Is the Axiom of Choice valid? Is excluded middle valid? Is this large >> cardinal hypothesis valid? etc.) Here, typing decidability advocates are >> apparently comfortable with the judgement |- t_m : nat -> bool for any >> *particular* HA-divergent m, but object to including it for *all* >> HA-divergent m. >> >> If I am wrong, please enlighten me by providing a particular HA-divergent m >> and a philosophical or mathematical case why t_m should not have type nat -> >> bool. >> >> Best regards, >> Paul