Timeline for Can a typing judgment admit essentially different derivations?
Current License: CC BY-SA 2.5
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 21, 2010 at 23:52 | comment | added | Mike Shulman | Okay, my first interpretation of your answer was correct, and it is in fact what I want. Thanks! The Schwinghammer paper doesn't help me much, though, because it is mostly about subtyping, but I'd like to see an explanation in the simple case of ordinary typed lambda-calculus, or even better for Martin-Lof DTT. | |
| Oct 21, 2010 at 23:32 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
added 400 characters in body
|
| Oct 21, 2010 at 23:16 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
added 922 characters in body
|
| Oct 21, 2010 at 19:55 | comment | added | Mike Shulman | If not all derivations are equivalent, can you give an example of two intrinsically different derivations of the same typing judgment (not using subtypes or anything fancy, just in ordinary type theory)? | |
| Oct 21, 2010 at 19:41 | comment | added | Mike Shulman | Wait a minute, so when you said "this property holds" you weren't actually referring to the property I was explicitly asking about, namely "all derivations become equivalent"? I thought that was what "cut-elimination guarantees that the addition of proof terms does make the typing derivations unique" meant. | |
| Oct 21, 2010 at 15:33 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
added some references
|
| Oct 20, 2010 at 21:41 | comment | added | Mike Shulman | Thank you very much, this is exactly the sort of thing I wanted. Where is a good reference to read about this? | |
| Oct 20, 2010 at 20:18 | vote | accept | Mike Shulman | ||
| Oct 20, 2010 at 18:30 | history | answered | Neel Krishnaswami | CC BY-SA 2.5 |