Timeline for Decidability of type inference and type checking in MLTT
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 15, 2021 at 19:02 | comment | added | cody | No; it's an untyped lambda term in the language of the system. | |
| Mar 15, 2021 at 18:27 | comment | added | user61651 | What's the definition of a preterm? Just a raw string? | |
| Sep 4, 2018 at 21:09 | vote | accept | Josh | ||
| Sep 3, 2018 at 23:21 | comment | added | cody | @JoshChen They don't clarify, but they may be referring to inferring types for "curry-style" terms, for which inference is undecidable. I go into more detail here: cs.stackexchange.com/a/12957/988 | |
| Aug 31, 2018 at 12:32 | comment | added | Josh | I apologize for adding question on question, but I am now not sure what to make of the statement in ncatlab.org/nlab/show/decidability#typability claiming that "dependent type theory has undecidable typeability", I wonder what is going on there.. | |
| Aug 30, 2018 at 14:50 | history | edited | cody | CC BY-SA 4.0 |
Add reference
|
| Aug 30, 2018 at 14:47 | comment | added | cody | @JoshChen the algorithms are at their core very general, as they involve a type-directed search, alternating with normalization steps on well-typed terms, as Andrej explained. I'm not aware of a generic description of the algorithm, unfortunately, though I'll add a partial reference to my answer. | |
| Aug 29, 2018 at 12:19 | comment | added | Josh | ...Or are the algorithms general enough to cover these differences? I am having trouble finding results in such generality; all I seem to be turning up in my literature search are very specific results, often particularly tailored to the underlying theory of some proof assistant. | |
| Aug 29, 2018 at 12:19 | comment | added | Josh | Thank you cody, are you referring to the type checking algorithms implemented by proof assistants like ALF and Coq? To my understanding those are algorithms for the specific variants of MLTT they are based on (CIC for Coq, something else for ALF), but it is unclear to me how these may be used to type check the specific MLTT of '73. In particular, if the universe hierarchy or other differences in detail there might change anything... | |
| Aug 29, 2018 at 9:09 | comment | added | Andrej Bauer | How about pretypes (terms allgedly denoting a type)? It might be worth clarifying their status as well. | |
| Aug 28, 2018 at 17:15 | history | answered | cody | CC BY-SA 4.0 |