[TYPES] decidability vs completeness
Paul Levy
P.B.Levy at cs.bham.ac.uk
Fri Aug 22 19:42:10 EDT 2014
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
More information about the Types-list
mailing list