[TYPES] Congruence rules vs frames

Sun Oct 10 09:46:38 EDT 2021

> 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 <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!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 <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.