Timeline for Can a typing judgment admit essentially different derivations?
Current License: CC BY-SA 2.5
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 7, 2010 at 5:53 | comment | added | Mike Shulman | Maybe it would clarify my question if I say that I don't want to treat terms as having any semantic status independent of a typing judgment, but given a term with a typing judgment, I don't want its semantic status to depend on how the typing judgment was arrived at. More specifically, given a definition of a semantics which appears to depend on how a typing judgment was arrived at, I want a systematic way to verify that it doesn't actually depend on that, only on the judgment itself. | |
| Nov 7, 2010 at 5:32 | comment | added | Mike Shulman | That makes sense to me, although in my case (see Edit 2 above) it seems that the desired semantics (lccc's) is "known to be coherent," and the problem is rather how to reflect this coherence in the syntax in order to formally define the semantics. But how is that related to the answer you gave above, in which you talked about "rephrasing a typing system as a logic"? | |
| Oct 22, 2010 at 9:23 | comment | added | Noam Zeilberger | The basic question is what are typing judgments about? Do (typed/untyped) terms have any semantic status independent of typing derivations? If they do, good, then we can ask about the "coherence" property at the level of the intended semantics. If they don't, then the property can only be stated at the level of syntax...which to me is a sign of a mismatch: either we should change the syntax to eliminate the distinction between terms and typing derivations (e.g., rephrase simply-typed lambda calculus as intuitionistic natural deduction), or we should refine the semantics. | |
| Oct 22, 2010 at 0:14 | comment | added | Mike Shulman | FYI, I edited the question trying to clarify what I was asking and why. | |
| Oct 22, 2010 at 0:03 | comment | added | Mike Shulman | I'm ashamed to say I can't make heads or tails of what you're talking about here. I don't necessarily want to identify types with propositions (I like to think of types as sets and terms as elements, or more generally interpret them in some other lccc), but neither do I usually think of defining a syntax of untyped terms first. In what sense are those opposites? They seem to me orthogonal questions: the first is about the intended semantics, and the second is about a syntactical choice. | |
| Oct 21, 2010 at 23:14 | history | answered | Noam Zeilberger | CC BY-SA 2.5 |