[ 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
