Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorJon Beardsley
    • CommentTimeSep 6th 2012

    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?

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 6th 2012

    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.

    • CommentRowNumber3.
    • CommentAuthorUlrik
    • CommentTimeSep 6th 2012

    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 p:(a=b)p:(a=b) infers aba\equiv b) gives non-terminating reduction, as follows:

    In a context that includes D:Type,p:(D=DD)D:\mathrm{Type}, p:(D = D \to D), you can type the usual fixed point combinator of λ\lambda-calculus, and thus all untyped λ\lambda-terms. Now take a non-terminating λ\lambda-term.

    Unfortunately, I don’t know of a good reference on this point.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2012

    The way I think about it is that

    1. 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.

    2. The extensionality rule makes propositional equality into judgmental equality, so that type-checking then also depends on propositional equality.

    3. 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.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeSep 7th 2012

    Ulrik and others: please consider putting such information into the entry extensional type theory. Also, we still badly need the entry decidability.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeSep 7th 2012
    • (edited Sep 7th 2012)

    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/.

    • CommentRowNumber7.
    • CommentAuthorUlrik
    • CommentTimeSep 7th 2012

    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?

    • CommentRowNumber8.
    • CommentAuthorJon Beardsley
    • CommentTimeSep 7th 2012

    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 ω=λx.xx\omega=\lambda x.xx or something, and Ω=ωω\Omega=\omega\omega, and then the β\beta-reduction of Ω\Omega 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!

    :)

    • CommentRowNumber9.
    • CommentAuthorUlrik
    • CommentTimeSep 7th 2012

    Ω\Omega 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 λ\lambda-terms, and \infty-categories, in that both have a coinductive element: Böhm trees form the final coalgebra for λ\lambda-terms with respect to head-normal form, and \infty-categories can be viewed coinductively as enriched in \infty-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 \infty-categories).

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 7th 2012

    coinductive view of ∞-categories

    Careful with this teminology. How about “strict \infty-categories” or “strict ω\omega-catgeories”, instead?

    • CommentRowNumber11.
    • CommentAuthorUlrik
    • CommentTimeSep 8th 2012
    • (edited Sep 8th 2012)

    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 \infty-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 \infty-functor if you want composition to be a sufficiently weak Hom-\infty-functor?

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeSep 8th 2012

    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.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeSep 8th 2012

    And actually, there is at least one formal coinductive definition of weak omega category.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeSep 8th 2012

    Okay, right. I take back my remark.