Timeline for Binding variables to terms involving later variables
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 1 at 20:51 | comment | added | Mike Shulman | Now reading more carefully, it looks like he doesn't specify it at all. The question is what the context of each branch in a case tree should be, which is the $\Phi$ in his labels $[\Phi]\bar{p}$ for case tree nodes. But he doesn't say how these are constructed; after defining a case tree (2.20) he just says "Most of the time we don't write down the telescope $[\Phi]$ because it can easily be reconstructed from $\bar{p}$ and $\Delta$." | |
| Mar 1 at 18:05 | comment | added | Mike Shulman | Thanks. It looks to me like p44 is defining a substitution to be used when evaluating a pattern-matching definition. My question is about what the codomain context of this substitution is. This seems like it ought to be somewhere in section 2.2 about type-checking, but on a first skim I cannot find where he specifies how to reorder the context. | |
| Mar 1 at 12:29 | comment | added | Meven Lennon-Bertrand♦ | You are right, things are hairier with indices. I think there is no easy solution there, you need to manipulate whole contexts and rely on a form of unification. The relevant reference is probably Jesper Cockx's PhD thesis. Skimming through, on p. 44 he gives a high level condition for the context in which each branch lives, which cannot be simply described from the one of the whole pattern-matching. Then a large part of the thesis is concerned with how to construct contexts (and case-trees) satisfying the criterion and being well-behaved. | |
| Mar 1 at 7:00 | comment | added | Mike Shulman | Heads up that I added a bit more to the question. In particular, it seems to me that in the presence of indexed datatypes, it isn't sufficient to just insert the all the new variables in any one place in the context. | |
| Feb 29 at 17:59 | comment | added | Mike Shulman |
Thanks! Cockx's talk is close to answering what I want to know. If I understand correctly, he's trying to introduce a version of well-scoped syntax that permits (among other things) modifying the scope by replacing x with new variables, for the purpose of a correct-by-construction implementation of core Agda. What he comes up with is interesting but doesn't quite do what he wants. But I would be content to know what Agda currently does! What sort of variables and contexts does it use that allow replacing x with new variables?
|
|
| Feb 29 at 15:21 | comment | added | James Wood |
I suppose the last two paragraphs, together with the pseudo-syntax of the question, lead one towards having with-abstraction expressions (like the generalize tactic, IIRC, in Coq).
|
|
| Feb 29 at 10:59 | history | answered | Meven Lennon-Bertrand♦ | CC BY-SA 4.0 |