[Agda] [TYPES] Congruence rules vs frames

[Siek, Jeremy]

The Decomposition / Composition Lemmas work for Frames too, provided they are typed analogously to how evaluation contexts are typed below.

-Jeremy

> On Oct 9, 2021, at 5:14 PM, Derek Dreyer <dreyer at 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 <wadler at 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.