[TYPES] decidability vs completeness

[Paul Levy]

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, 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




--
Paul Blain Levy
School of Computer Science, University of Birmingham
+44 121 414 4792
http://www.cs.bham.ac.uk/~pbl