Timeline for Can strict propositions (Rocq's SProp, Agda's Prop) be used to show termination?
Current License: CC BY-SA 4.0
2 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 27 at 16:33 | comment | added | Dan Doel | Note that this is the sort of addition that causes technical problems, even if your intended model justifies it. If it's just an axiom, then you lose canonicity. And if you use the typical unbounded search that doesn't look at the proof term (since you have to treat every proof term as judgmentally equal), then in inconsistent contexts you can lie about the search actually being terminating. So open evaluation becomes undecidable. Unbounded search seems (to me) a better match to runtime-only computational irrelevance. | |
| Apr 26 at 11:23 | history | answered | aws | CC BY-SA 4.0 |