[TYPES] Congruence rules vs frames

[Derek Dreyer]

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.