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