<div dir="ltr">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:<div><br></div><div>  ξ-·₁ : ∀ {L L′ M}<br>    → L —→ L′<br>      -----------------<br>    → L · M —→ L′ · M<br><br>  ξ-·₂ : ∀ {V M M′}<br>    → Value V<br>    → M —→ M′<br>      -----------------<br>    → V · M —→ V · M′<br></div><div><br></div><div>One might instead define frames that specify evaluation contexts and have a single congruence rule.</div><div><br></div><div>data Frame : Set where<br>  □·                   : Term → Frame<br>  ·□                   : (V : Term) → Value V → Frame<br></div><div><br></div><div>_[_] : Frame → Term → Term<br>(□· M) [ L ]                        =  L · M<br>(·□ V _) [ M ]                    =  V · M<br></div><div> </div><div> ξ : ∀ F {M M′}<br>    → M —→ M′<br>      -------------------<br>    → F [ M ] —→ F [ M′ ]<br></div><div><br></div><div>However, one rapidly gets into problems. For instance, consider the proof that types are preserved by reduction.</div><div><br></div><div>preserve : ∀ {M N A}<br>  → ∅ ⊢ M ⦂ A<br>  → M —→ N<br>    ----------<br>  → ∅ ⊢ N ⦂ A<br>...</div><div>preserve (⊢L · ⊢M)  (ξ (□· _) L—→L′)  =  (preserve ⊢L L—→L′) · ⊢M<br>preserve (⊢L · ⊢M)  (ξ (·□ _ _) M—→M′)  =  ⊢L · (preserve ⊢M M—→M′)<br></div><div>...</div><div><br></div><div>The first of these two lines gives an error message:</div><div><br></div><div>I'm not sure if there should be a case for the constructor ξ,<br>because I get stuck when trying to solve the following unification<br>problems (inferred index ≟ expected index):<br>  F [ M ] ≟ L · M₁<br>  F [ M′ ] ≟ N<br>when checking that the pattern ξ (□· _) L—→L′ has type L · M —→ N<br></div><div><br></div><div>And the second provokes a similar error.</div><div><br></div><div>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?</div><div><br></div><div>Thank you for your help. Go well, -- P</div><div><br></div><div><br></div><div><br></div><div><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div></div></div>