[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> I managed to carry out a proof along the lines described by Derek and Jules, > but it used more ink (and more think!) than my original proof using a > congruence rule for each constructor. In this, as in much else, I find myself > agreeing with Bob. I don't think there's likely to be a big difference one way or the other when proving syntactic properties. I personally like to use the evaluation context semantics because the idea of an evaluation context comes in extremely handy later on when you get to deeper semantic or Hoare-style reasoning (of the sort we do when formulating logical relations arguments in Iris). At that point, the "inductive" cases of the relation can be handled uniformly using a "Bind" lemma. In the case of unary logical relations, this lemma looks something like the following: e \in E[A] forall v:Val. (v \in V[A]) => (K[v] \in E[B]) ---------------------------------------------------- K[e] \in E[B] where E[B] is the logical relation on terms of type B, and V[A] is the logical relation on values of type A. Using the Bind Lemma, for example, you can take a proof goal like the following (this is the case of proving "compatibility" of the logical relation for function applications): e1 \in E[A -> B] e2 \in E[A] -------------------- e1 e2 \in E[B] and through two applications of Bind, you can reduce it to: v1 \in V[A -> B] v2 \in V[A] -------------------- v1 v2 \in E[B] This approach scales also to languages with a wide range of features (recursive types, state, concurrency), at least if you work in a logical framework like Iris. In fact, I used this very example to motivate the use of Iris in my POPL'18 keynote (see around 28:30, the Bind rule is then discussed a few minutes later: https://urldefense.com/v3/__https://www.youtube.com/watch?v=8Xyk_dGcAwk&ab_channel=POPL2018__;!!IBzWLUs!G2KhnZbuiPIsnAWmxp3nKsyAqqNkyiHo5kL0icZ3pru8QkU69To1o-Oz6FUAk52G_lp8ZPZSz5Q$ ). Without evaluation contexts, I don't know how to express such a lemma nicely. Cheers, Derek > > Have I got that right? Or is there a magic bullet that I'm missing? 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!G2KhnZbuiPIsnAWmxp3nKsyAqqNkyiHo5kL0icZ3pru8QkU69To1o-Oz6FUAk52G_lp8h6qNokQ$ > > > > > On Sat, 9 Oct 2021 at 22:12, Derek Dreyer <dre...@mpi-sws.org> wrote: >> >> This email was sent to you by someone outside the University. >> You should only click on links or attachments if you are certain that the >> email is genuine and the content is safe. >> >> 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!G2KhnZbuiPIsnAWmxp3nKsyAqqNkyiHo5kL0icZ3pru8QkU69To1o-Oz6FUAk52G_lp86DUCbU8$ >> >> >> (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.
