[TYPES] Congruence rules vs frames

[Philip Wadler]

Thanks, Derek, and everyone else.

I am asking for a friend. (Literally!) The friend's situation is adapting
theory to a more realistic language with more constructs. As the number of
constructs grows, the disadvantage of one congruence rule for each
construct grows, and the advantages of contexts or frames become more
pronounced. In our informal developments the advantage of contexts or
frames is that they capture commonality in the rules, resulting in less ink
on the page.

However, if I read Derek's advice correctly, using contexts or frames
doesn't save much ink. The ink that would have been required from writing
down the congruence rules and the corresponding cases in the proofs now
goes into writing down the corresponding cases in the composition and
decomposition lemmas. Jules points out a neat trick that saves effort for a
proof of preservation, but that won't help elsewhere. For instance, I first
ran into the problem  when trying to prove something simpler than
preservation: that if a term is a value then no reduction applies.

Apparently, identifying a commonality in the statement of the rules doesn't
mean the properties of the rules get proved uniformly, they still require
the same work as if the congruence rules were given separately. Alas, there
is no free lunch.

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.

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!EfT_MPNP2SmpqfH1RBLPmmMMfLjinF1_UF0esLogHr7jl1XBZt4GF2s6Rc3wg7bZvbr7yZxAKwc$ 



On Sat, 9 Oct 2021 at 22:12, Derek Dreyer <dreyer at 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!EfT_MPNP2SmpqfH1RBLPmmMMfLjinF1_UF0esLogHr7jl1XBZt4GF2s6Rc3wg7bZvbr7W73gsBA$ 
>
> (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.
>