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

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

Reply via email to