[TYPES] decidability vs completeness

[Jon Sterling]

Bob,

That was a wonderful answer; thank you for drawing the distinction
between H >> M:A and H >> M in A. Previously, I'd always considered
those just two notations for the same idea, and nuprl/ctt just had
additional axioms the judgement synthetic. But it is much more elegant
to just consider them two very different judgements.

After reading this, I have been thinking about what it would look like
to have a decidable type theory which keeps the cheap syntactic typing
judgement, but also has a notion of semantic membership. This could be
done by tweaking observational type theory (Altenkirch/McBride) to have
more interesting rules for its propositional equality, which could then
in its reflexive case represent membership.

Of course, the fact that the derivations of realizers get reified in the
terms means that this is no different from plain ott (a syntactic mere
approximation of the Truth), but in the same way that ott allows you to
express (with no small degree of difficulty) the true equality of things
propositionally, it might also allow you to express (with an equal
degree of difficulty) non-trivial membership for subset types,
intersection types, etc. In order for any of this to work, the equality
type has to be reformulated to be defined over untyped terms like in
nuprl, and if this were done, I think it might also be possible to
express something like the bar types in this setting, but I am not
certain of that.

Of course, the desire to do any of this syntactic stuff seems to derive
from a conflation of the logical framework with the type theory, but it
might work for those who have already agreed to pay the full price for
itt. 

Kind regards,
Jon

-- 
Jon Sterling
http://jonmsterling.com/

On Sat, Aug 23, 2014, at 12:34 PM, Prof Robert Harper wrote:
> [ 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
> rwh at cs.cmu.edu
> -----------------------------
> 
> 
> 
> On Aug 23, 2014, at 12:01, Paul Levy <P.B.Levy at 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
>