[Agda] Congruence rules vs frames

[Uma Zalakain (PGR)]

I believe the problem here is the use of function applications (_[_]) as indices of a data type (_—→_) by a constructor (ξ). Transforming the binary function into a ternary relation might solve the issue , and functionality can be recovered later, though the downside is that you will end up with two extra arguments in the constructor.

~uma


________________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Philip Wadler <wadler at inf.ed.ac.uk>
Sent: 09 October 2021 16:32
To: Types list; Agda mailing list
Subject: [Agda] Congruence rules vs frames

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
. http://homepages.inf.ed.ac.uk/wadler/