split out reduction rules
This commit is contained in:
Jeremy Siek
parent
6d9999bb73
commit
62b9bc0a75
2 changed files with 101 additions and 85 deletions
|
|
@ -6,6 +6,7 @@ module extra.Confluence where
|
|||
|
||||
\begin{code}
|
||||
open import extra.Substitution
|
||||
open import extra.LambdaReduction
|
||||
open import plfa.Denotational using (Rename)
|
||||
open import plfa.Soundness using (Subst)
|
||||
open import plfa.Untyped
|
||||
|
|
@ -18,91 +19,6 @@ open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; p
|
|||
renaming (_,_ to ⟨_,_⟩)
|
||||
\end{code}
|
||||
|
||||
## Reduction without the restrictions
|
||||
|
||||
\begin{code}
|
||||
infix 2 _—→_
|
||||
|
||||
data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
ξ₁ : ∀ {Γ} {L L′ M : Γ ⊢ ★}
|
||||
→ L —→ L′
|
||||
----------------
|
||||
→ L · M —→ L′ · M
|
||||
|
||||
ξ₂ : ∀ {Γ} {L M M′ : Γ ⊢ ★}
|
||||
→ M —→ M′
|
||||
----------------
|
||||
→ L · M —→ L · M′
|
||||
|
||||
β : ∀ {Γ} {N : Γ , ★ ⊢ ★} {M : Γ ⊢ ★}
|
||||
---------------------------------
|
||||
→ (ƛ N) · M —→ N [ M ]
|
||||
|
||||
ζ : ∀ {Γ} {N N′ : Γ , ★ ⊢ ★}
|
||||
→ N —→ N′
|
||||
-----------
|
||||
→ ƛ N —→ ƛ N′
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
infix 2 _—↠_
|
||||
infix 1 start_
|
||||
infixr 2 _—→⟨_⟩_
|
||||
infix 3 _[]
|
||||
|
||||
data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
_[] : ∀ {Γ A} (M : Γ ⊢ A)
|
||||
--------
|
||||
→ M —↠ M
|
||||
|
||||
_—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
|
||||
→ L —→ M
|
||||
→ M —↠ N
|
||||
---------
|
||||
→ L —↠ N
|
||||
|
||||
start_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
|
||||
→ M —↠ N
|
||||
------
|
||||
→ M —↠ N
|
||||
start M—↠N = M—↠N
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
—↠-trans : ∀{Γ}{A}{L M N : Γ ⊢ A}
|
||||
→ L —↠ M
|
||||
→ M —↠ N
|
||||
→ L —↠ N
|
||||
—↠-trans (M []) mn = mn
|
||||
—↠-trans (L —→⟨ r ⟩ lm) mn = L —→⟨ r ⟩ (—↠-trans lm mn)
|
||||
\end{code}
|
||||
|
||||
## Congruences
|
||||
|
||||
\begin{code}
|
||||
abs-cong : ∀ {Γ} {N N' : Γ , ★ ⊢ ★}
|
||||
→ N —↠ N'
|
||||
----------
|
||||
→ ƛ N —↠ ƛ N'
|
||||
abs-cong (M []) = ƛ M []
|
||||
abs-cong (L —→⟨ r ⟩ rs) = ƛ L —→⟨ ζ r ⟩ abs-cong rs
|
||||
|
||||
appL-cong : ∀ {Γ} {L L' M : Γ ⊢ ★}
|
||||
→ L —↠ L'
|
||||
---------------
|
||||
→ L · M —↠ L' · M
|
||||
appL-cong {Γ}{L}{L'}{M} (L []) = L · M []
|
||||
appL-cong {Γ}{L}{L'}{M} (L —→⟨ r ⟩ rs) = L · M —→⟨ ξ₁ r ⟩ appL-cong rs
|
||||
|
||||
appR-cong : ∀ {Γ} {L M M' : Γ ⊢ ★}
|
||||
→ M —↠ M'
|
||||
---------------
|
||||
→ L · M —↠ L · M'
|
||||
appR-cong {Γ}{L}{M}{M'} (M []) = L · M []
|
||||
appR-cong {Γ}{L}{M}{M'} (M —→⟨ r ⟩ rs) = L · M —→⟨ ξ₂ r ⟩ appR-cong rs
|
||||
\end{code}
|
||||
|
||||
## Parallel Reduction
|
||||
|
||||
|
|
|
|||
100
extra/extra/LambdaReduction.lagda
Normal file
100
extra/extra/LambdaReduction.lagda
Normal file
|
|
@ -0,0 +1,100 @@
|
|||
\begin{code}
|
||||
module extra.LambdaReduction where
|
||||
\end{code}
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
open import extra.Substitution
|
||||
open import plfa.Untyped
|
||||
renaming (_—→_ to _——→_; _—↠_ to _——↠_; begin_ to commence_; _∎ to _fini)
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
\end{code}
|
||||
|
||||
## Full beta reduction
|
||||
|
||||
\begin{code}
|
||||
infix 2 _—→_
|
||||
|
||||
data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
ξ₁ : ∀ {Γ} {L L′ M : Γ ⊢ ★}
|
||||
→ L —→ L′
|
||||
----------------
|
||||
→ L · M —→ L′ · M
|
||||
|
||||
ξ₂ : ∀ {Γ} {L M M′ : Γ ⊢ ★}
|
||||
→ M —→ M′
|
||||
----------------
|
||||
→ L · M —→ L · M′
|
||||
|
||||
β : ∀ {Γ} {N : Γ , ★ ⊢ ★} {M : Γ ⊢ ★}
|
||||
---------------------------------
|
||||
→ (ƛ N) · M —→ N [ M ]
|
||||
|
||||
ζ : ∀ {Γ} {N N′ : Γ , ★ ⊢ ★}
|
||||
→ N —→ N′
|
||||
-----------
|
||||
→ ƛ N —→ ƛ N′
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
infix 2 _—↠_
|
||||
infix 1 start_
|
||||
infixr 2 _—→⟨_⟩_
|
||||
infix 3 _[]
|
||||
|
||||
data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
_[] : ∀ {Γ A} (M : Γ ⊢ A)
|
||||
--------
|
||||
→ M —↠ M
|
||||
|
||||
_—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
|
||||
→ L —→ M
|
||||
→ M —↠ N
|
||||
---------
|
||||
→ L —↠ N
|
||||
|
||||
start_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
|
||||
→ M —↠ N
|
||||
------
|
||||
→ M —↠ N
|
||||
start M—↠N = M—↠N
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
—↠-trans : ∀{Γ}{A}{L M N : Γ ⊢ A}
|
||||
→ L —↠ M
|
||||
→ M —↠ N
|
||||
→ L —↠ N
|
||||
—↠-trans (M []) mn = mn
|
||||
—↠-trans (L —→⟨ r ⟩ lm) mn = L —→⟨ r ⟩ (—↠-trans lm mn)
|
||||
\end{code}
|
||||
|
||||
## Multi-step reduction is a congruence
|
||||
|
||||
\begin{code}
|
||||
abs-cong : ∀ {Γ} {N N' : Γ , ★ ⊢ ★}
|
||||
→ N —↠ N'
|
||||
----------
|
||||
→ ƛ N —↠ ƛ N'
|
||||
abs-cong (M []) = ƛ M []
|
||||
abs-cong (L —→⟨ r ⟩ rs) = ƛ L —→⟨ ζ r ⟩ abs-cong rs
|
||||
|
||||
appL-cong : ∀ {Γ} {L L' M : Γ ⊢ ★}
|
||||
→ L —↠ L'
|
||||
---------------
|
||||
→ L · M —↠ L' · M
|
||||
appL-cong {Γ}{L}{L'}{M} (L []) = L · M []
|
||||
appL-cong {Γ}{L}{L'}{M} (L —→⟨ r ⟩ rs) = L · M —→⟨ ξ₁ r ⟩ appL-cong rs
|
||||
|
||||
appR-cong : ∀ {Γ} {L M M' : Γ ⊢ ★}
|
||||
→ M —↠ M'
|
||||
---------------
|
||||
→ L · M —↠ L · M'
|
||||
appR-cong {Γ}{L}{M}{M'} (M []) = L · M []
|
||||
appR-cong {Γ}{L}{M}{M'} (M —→⟨ r ⟩ rs) = L · M —→⟨ ξ₂ r ⟩ appR-cong rs
|
||||
\end{code}
|
||||
Loading…
Add table
Reference in a new issue