Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 14 of 14
Just wondering if there are relatively simple reasons why good computational qualities, like decidable type and equality checking, fail in extensional type theory. I’m just beginning to read some of this homotopy type theory stuff, but am relatively familiar with at least the bare bones of type theory. Is there some intuitive reason behind this, or is it sort of a technical result?
I’d like to understand this better myself, as I think it might have something to do with psychological hangups I’m having with the incomplete project on predicate logic on my web. Any relevant (free, online) references might be a big help, if anyone knows of some.
First of all, in type theory, judgmental equality is the congruence and equivalence closure of reduction, so decidable type checking requires terminating reduction.
Now, it’s quite easy to see that extensional equality (the rule that from infers ) gives non-terminating reduction, as follows:
In a context that includes , you can type the usual fixed point combinator of -calculus, and thus all untyped -terms. Now take a non-terminating -term.
Unfortunately, I don’t know of a good reference on this point.
The way I think about it is that
in dependent type theory, since types can depend on terms, type-checking (which always depends on judgmental equality of types) can also depend on judgmental equality of terms.
The extensionality rule makes propositional equality into judgmental equality, so that type-checking then also depends on propositional equality.
But propositional equality is expressive enough to encode basically all of mathematics. So clearly it cannot be computationally decidable. Hence neither can type-checking with extensionality.
Ulrik and others: please consider putting such information into the entry extensional type theory. Also, we still badly need the entry decidability.
Urs just put some stuff by Robert Harper at proof that goes a way to answering Jon’s question.
Actually, no: what Urs put there is not what answers the question, but the rest of the article from which it was taken does answer it. So let me link it directly: https://existentialtype.wordpress.com/2012/08/11/extensionality-intensionality-and-brouwers-dictum/.
I’ve added something to decidability. I’m not quite sure what to do about extensional type theory due to uneasiness about what the entry is really about. I feel it should refer to type theory with equality reflection, and then perhaps there should be another entry on attempts to approximate 0-dimensional type theory within intensional type theory?
Wow thanks, all of this is super helpful! Mike’s argument makes it really clear. Also, I’m especially interested in the notion of non-terminating terms that Ulrik mentions. I recall terms like or something, and , and then the -reduction of just goes on forever or something. Is the kind of the sort of thing we’re thinking about when we say “non-terminating” terms? Or, I guess, I’m wiki’ing “fixed-type-combinator” right now, which seems to be sort of the same idea.
I hate to bring this up again, since nobody seems to really like it…. but can we draw connections between this and G.S. Brown’s notion of “re-entry”? Is that a “baby” version of this very idea in some sense?
Additionally, do such non-terminating things lend themselves to the notion of infinity-categories in some nice way (lately I’ve been thinking about Aristotle’s Third Man Argument [http://en.wikipedia.org/wiki/Third_man_argument] in connection with simplicial sets or infinity categories, at least trying to think about that, and wondering about cases of infinite regress in categorical terms)? Or in another more specific sense, can we think about this kind of thing homotopically? What does it mean that a term is propositionally equal to a term that includes itself? Is this not an issue since in some sense the is the very definition of “infinite” (i.e. a set which contains a set isomorphic to itself)?
Sorry again for being poorly informed and naive!
:)
is exactly the kind of non-terminating term I had in mind.
Sorry, I don’t know about “reentry” so I can’t comment on that.
I also don’t see the connection with the Third Man Argument, but there certainly is a connection between the observational equality on untyped -terms, and -categories, in that both have a coinductive element: Böhm trees form the final coalgebra for -terms with respect to head-normal form, and -categories can be viewed coinductively as enriched in -categories (I’m sorry that both statements are a little vague: see exercise 4.3.4 in Bart Jacobs’ book, Introduction to Coalgebra for the precise statement on Böhm trees, and ask others around here for more on the coinductive view of -categories).
coinductive view of ∞-categories
Careful with this teminology. How about “strict -categories” or “strict -catgeories”, instead?
Thanks for stepping in, Urs! I tried to hedge my statement, but I think you’re right that the naïve way to coinductively define a notion of -category gives a strict notion. But isn’t there some hope that if done cleverly in homotopy type theory it might give something weaker?
I haven’t really thought about, but I guess it turns on how you define an -functor if you want composition to be a sufficiently weak Hom--functor?
Weak omega-categories are certainly morally coinductive, even if no one has written down a formal definition along these lines yet.
I don’t know anything about reetry or third men either.
And actually, there is at least one formal coinductive definition of weak omega category.
Okay, right. I take back my remark.
1 to 14 of 14