[TYPES] Congruence rules vs frames

[Gan Shen]

Hi Philip,

Here's a hacky (but simple!) way that works on my end, try defining _[_]
like this
```
_[_]′ : Frame → Term → Term × Term
(□· M)   [ L ]′ =  L , M
(·□ V _) [ M ]′ =  V , M

_[_] : Frame → Term → Term
F [ T ] = let M₁ , M₂ = F [ T ]′
          in _·_ M₁ M₂
```

Here's my explanation of why it works (disclaimer: I don't know too much
about Agda internals, this is purely based on my experience):
When doing unification, Agda will first evaluate terms to weak head normal
form (WHNF), the problem with your old _[_] is that the evaluation is
blocked by the pattern matching, even though it's very clear from the code
that it always returns a WHNF starting with _·_, unfortunately Agda doesn't
know that. The new _[_] fixes this by unconditionally returning a WHNF
starting with _·_.

Best,
Gan



On Sat, Oct 9, 2021 at 2:15 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.
>