Today: Trying to figure out what is really going on in common with the context manipulation in the multimodal and proof-irrelevant extensions of LF. It's conspicuous that hypotheses in the former seem to require being well-formed in a restriction of the context to the left of them (that is, assuming x valid at A means that A itself is "validly" not merely "truly" a type) and in the latter such type-level context shenanigans are forbidden — and this was precisely the source of the validity-lemma bug in Pfenning '01. This sort of evidence makes me feel that the mistake was a very understandable one to commit. I would conjecture that what might be required is to take a greatest lower bound of the munged and unmunged context, so that the modal situation demands the munged context (because the munged context is weaker than the original) and the irrelevant situation demands the unmunged context (because the munged context is stronger).
Today: Trying to figure out what is really going on in common with the context manipulation in the multimodal and proof-irrelevant extensions of LF. It's conspicuous that hypotheses in the former seem to require being well-formed in a restriction of the context to the left of them (that is, assuming x valid at A means that A itself is "validly" not merely "truly" a type) and in the latter such type-level context shenanigans are forbidden — and this was precisely the source of the validity-lemma bug in Pfenning '01. This sort of evidence makes me feel that the mistake was a very understandable one to commit. I would conjecture that what might be required is to take a greatest lower bound of the munged and unmunged context, so that the modal situation demands the munged context (because the munged context is weaker than the original) and the irrelevant situation demands the unmunged context (because the munged context is stronger).
- Post a new comment
- 1 comment
- Post a new comment
- 1 comment
