[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
@Jules: I think you're right and I was wrong. There's no need to define the eval ctxt typing *intensionally*, as I have been doing. I might as well define it *extensionally* (which is more my style anyway, but somehow I thought the extensional approach didn't work so well here). Ironically, what you end up then is just the old idea of the Replacement lemma. So never mind what I said about Decomposition/Composition being an improvement over Replacement. I think I'm gonna change my course notes to follow your approach. ;-) The case where I don't know how to do the "extensional" thing (or where there's no point in doing so?) is when proving preservation for an abstract machine semantics where the evaluation context is made explicit as the "stack" of the machine, and where the stack may contain frames that do not directly correspond to any language term. I have used such abstract machines in several papers. There, the only way I could see to set up preservation was to define (intensionally) a bespoke typing judgment on the continuation stacks (and their constituent frames). But also for that kind of semantics, since all the "search" steps are actually made explicit as steps of computation, there's no need to prove Decomposition or Replacement at all. In fact, in that semantics, the reduction relation is totally flat, so the preservation proof is just by case analysis, not induction. You can see an example of this in one of my earliest papers spelled out in full gory detail: https://urldefense.com/v3/__https://people.mpi-sws.org/*dreyer/papers/recursion/tr/main.pdf__;fg!!IBzWLUs!C9QBGWf7aqrcqMMM2YLscE0Hn5M6P29k6izHDlozBFllrQAv5GvXArITpyiOM3uNajQH42pexBo$ Thanks! Derek On Sat, Oct 9, 2021 at 11:29 PM Jules Jacobs <julesjac...@gmail.com> wrote: > > I had previously only addressed the first part of this only to Philip Wadler, > so I reproduce it here: > > Compcert uses evaluation contexts: > https://urldefense.com/v3/__https://compcert.org/doc/html/compcert.cfrontend.Csem.html*context__;Iw!!IBzWLUs!C9QBGWf7aqrcqMMM2YLscE0Hn5M6P29k6izHDlozBFllrQAv5GvXArITpyiOM3uNajQH2gnpDsc$ > > Iris does too: > https://urldefense.com/v3/__https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_heap_lang/lang.v*L412__;Iw!!IBzWLUs!C9QBGWf7aqrcqMMM2YLscE0Hn5M6P29k6izHDlozBFllrQAv5GvXArITpyiOM3uNajQHkGZ825c$ > > > This is slightly different than what you propose, because here the nesting is > handled in the definition of contexts rather than in the step relation. > Your approach works too: > https://urldefense.com/v3/__https://pastebin.com/raw/TQU9UrnS__;!!IBzWLUs!C9QBGWf7aqrcqMMM2YLscE0Hn5M6P29k6izHDlozBFllrQAv5GvXArITpyiOM3uNajQHGT19Rf4$ > > I have here represented the frame f directly as its f[_] function, but I > think that shouldn't make a difference. > > About decomposition/composition: > I have found it useful to define context typing as > > (K : A => B) := ∀ e, e : A => K[e] : B > > This means you don't need to give the inductive rules, and you get > composition for free. > In fact, I usually don't even give context typing a name in Coq, and instead > prove this lemma by induction on typing: > > K[e] : B <=> ∃ A, e : A ∧ ∀ e, e : A => K[e] : B. > > Jules > > > On Sat, Oct 9, 2021 at 11:14 PM Derek Dreyer <dre...@mpi-sws.org> wrote: >> >> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] >> >> Hi, Phil. >> >> Yes, there is a way to make the single congruence rule work. See for >> example the way I set things up in my Semantics course notes (see >> Section 1.2): >> https://urldefense.com/v3/__https://courses.ps.uni-saarland.de/sem_ws1920/dl/21/lecture_notes_2nd_half.pdf__;!!IBzWLUs!G2Y7fSLG9GkuFfn_pRKp5yvrMo1tv78em8j3kc4xuW-yBS3NZuhJ49Y6sdougc4yziUkPf0h6W8$ >> >> (Note: the general approach described below is not original, but my >> version may be easier to mechanize than others. Earlier work, such as >> Wright-Felleisen 94 and Harper-Stone 97, presents variations on this >> -- they use the term Replacement Lemma -- that I think are a bit >> clunkier and/or more annoying to mechanize. Wright-Felleisen cites >> Hindley-Seldin for this Replacement Lemma. In my version, the >> Replacement Lemma is broken into two lemmas -- Decomposition and >> Composition -- by defining a typing judgment for evaluation contexts.) >> >> Under this approach, you: >> >> 1. Divide the definition of reduction into two relations: let's call >> them "base reduction" and "full reduction". The base one has all the >> interesting basic reduction rules that actually do something (e.g. >> beta). The full one has just one rule, which handles all the "search" >> cases via eval ctxts: it says that K[e] reduces to K[e'] iff e >> base-reduces to e'. I believe it isn't strictly necessary to separate >> into two relations, but I've tried it without separating, and it makes >> the proof significantly cleaner to separate. >> >> 2. Define a notion of evaluation context typing K : A => B (signifying >> that K takes a hole of type A and returns a term of type B). This is >> the key part that many other accounts skip, but it makes things >> cleaner. >> >> With eval ctxt typing in hand, we can now prove the following two very >> easy lemmas (each requires like only 1 or 2 lines of Coq): >> >> 3. Decomposition Lemma: If K[e] : B, then there exists A such that K : >> A => B and e : A. >> >> 4. Composition Lemma, If K : A => B and e : A, then K[e] : B. >> >> (Without eval ctxt typing, you have to state and prove these lemmas as >> one joint Replacement lemma.) >> >> Then, to prove preservation, you first prove preservation for base >> reduction in the usual way. Then, the proof of preservation for full >> reduction follows immediately by wrapping the base-reduction >> preservation lemma with calls to Decomposition and Composition (again, >> just a few lines of Coq). >> >> My Semantics course notes just show this on pen and paper, but my >> students have also mechanized it in Coq, and we will be using that in >> the newest version of my course this fall. It is quite >> straightforward. The Coq source for the course is still in >> development at the moment, but I can share it with you if you're >> interested. I would be interested to know if for some reason this >> proof structure is harder to mechanize in Agda. >> >> Best wishes, >> Derek >> >> >> On Sat, Oct 9, 2021 at 8:55 PM Philip Wadler <wad...@inf.ed.ac.uk> wrote: >> > >> > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list >> > ] >> > >> > Most mechanised formulations of reduction systems, such as those found in >> > Software Foundations or in Programming Language Foundations in Agda, use >> > one congruence rule for each evaluation context: >> > >> > ξ-·₁ : ∀ {L L′ M} >> > → L —→ L′ >> > ----------------- >> > → L · M —→ L′ · M >> > >> > ξ-·₂ : ∀ {V M M′} >> > → Value V >> > → M —→ M′ >> > ----------------- >> > → V · M —→ V · M′ >> > >> > One might instead define frames that specify evaluation contexts and have a >> > single congruence rule. >> > >> > data Frame : Set where >> > □· : Term → Frame >> > ·□ : (V : Term) → Value V → Frame >> > >> > _[_] : Frame → Term → Term >> > (□· M) [ L ] = L · M >> > (·□ V _) [ M ] = V · M >> > >> > ξ : ∀ F {M M′} >> > → M —→ M′ >> > ------------------- >> > → F [ M ] —→ F [ M′ ] >> > >> > However, one rapidly gets into problems. For instance, consider the proof >> > that types are preserved by reduction. >> > >> > preserve : ∀ {M N A} >> > → ∅ ⊢ M ⦂ A >> > → M —→ N >> > ---------- >> > → ∅ ⊢ N ⦂ A >> > ... >> > preserve (⊢L · ⊢M) (ξ (□· _) L—→L′) = (preserve ⊢L L—→L′) · ⊢M >> > preserve (⊢L · ⊢M) (ξ (·□ _ _) M—→M′) = ⊢L · (preserve ⊢M M—→M′) >> > ... >> > >> > The first of these two lines gives an error message: >> > >> > I'm not sure if there should be a case for the constructor ξ, >> > because I get stuck when trying to solve the following unification >> > problems (inferred index ≟ expected index): >> > F [ M ] ≟ L · M₁ >> > F [ M′ ] ≟ N >> > when checking that the pattern ξ (□· _) L—→L′ has type L · M —→ N >> > >> > And the second provokes a similar error. >> > >> > This explains why so many formulations use one congruence rule for each >> > evaluation context. But is there a way to make the approach with a single >> > congruence rule work? Any citations to such approaches in the literature? >> > >> > Thank you for your help. Go well, -- P >> > >> > >> > >> > . \ Philip Wadler, Professor of Theoretical Computer Science, >> > . /\ School of Informatics, University of Edinburgh >> > . / \ and Senior Research Fellow, IOHK >> > . >> > https://urldefense.com/v3/__http://homepages.inf.ed.ac.uk/wadler/__;!!IBzWLUs!EIYnAk7pSQVJFwJaONabTO_JqymiXUpQnVqKBbbpFSiJ_flduU6cOIjOgNtqMC_UDbn50dUukp4$ >> > The University of Edinburgh is a charitable body, registered in >> > Scotland, with registration number SC005336.
