------------------------------------------------------------------------
-- The Agda standard library
--
-- Concepts from rewriting theory
-- Definitions are based on "Term Rewriting Systems" by J.W. Klop
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Rewriting where
open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Data.Product.Base using (_×_ ; ∃ ; -,_; _,_ ; proj₁ ; proj₂)
open import Function.Base using (flip)
open import Induction.WellFounded using (WellFounded; Acc; acc)
open import Relation.Binary.Core using (REL; Rel)
open import Relation.Binary.Construct.Closure.Equivalence using (EqClosure)
open import Relation.Binary.Construct.Closure.Equivalence.Properties
using (a—↠b&a—↠c⇒b↔c)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
using (Star; _◅_; ε; _◅◅_)
open import Relation.Binary.Construct.Closure.Symmetric using (fwd; bwd)
open import Relation.Binary.Construct.Closure.Transitive
using (Plus; [_]; _∼⁺⟨_⟩_)
open import Relation.Nullary.Negation.Core using (¬_; contradiction)
-- The following definitions are taken from Klop [5]
module _ {a ℓ} {A : Set a} (_⟶_ : Rel A ℓ) where
private
_⟵_ = flip _⟶_
_—↠_ = Star _⟶_
_↔_ = EqClosure _⟶_
IsNormalForm : A → Set _
IsNormalForm a = ¬ ∃ λ b → (a ⟶ b)
HasNormalForm : A → Set _
HasNormalForm b = ∃ λ a → IsNormalForm a × (b —↠ a)
NormalForm : Set _
NormalForm = ∀ {a b} → IsNormalForm a → b ↔ a → b —↠ a
WeaklyNormalizing : Set _
WeaklyNormalizing = ∀ a → HasNormalForm a
StronglyNormalizing : Set _
StronglyNormalizing = WellFounded _⟵_
UniqueNormalForm : Set _
UniqueNormalForm = ∀ {a b} → IsNormalForm a → IsNormalForm b → a ↔ b → a ≡ b
Confluent : Set _
Confluent = ∀ {A B C} → A —↠ B → A —↠ C → ∃ λ D → (B —↠ D) × (C —↠ D)
WeaklyConfluent : Set _
WeaklyConfluent = ∀ {A B C} → A ⟶ B → A ⟶ C → ∃ λ D → (B —↠ D) × (C —↠ D)
Deterministic : ∀ {a b ℓ₁ ℓ₂} → {A : Set a} → {B : Set b} → Rel B ℓ₁ → REL A B ℓ₂ → Set _
Deterministic _≈_ _—→_ = ∀ {x y z} → x —→ y → x —→ z → y ≈ z
module _ {a ℓ} {A : Set a} {_⟶_ : Rel A ℓ} where
private
_—↠_ = Star _⟶_
_↔_ = EqClosure _⟶_
_⟶₊_ = Plus _⟶_
det⇒conf : Deterministic _≡_ _⟶_ → Confluent _⟶_
det⇒conf det ε rs₂ = -, rs₂ , ε
det⇒conf det rs₁ ε = -, ε , rs₁
det⇒conf det (r₁ ◅ rs₁) (r₂ ◅ rs₂)
rewrite det r₁ r₂ = det⇒conf det rs₁ rs₂
conf⇒wcr : Confluent _⟶_ → WeaklyConfluent _⟶_
conf⇒wcr c fst snd = c (fst ◅ ε) (snd ◅ ε)
conf⇒nf : Confluent _⟶_ → NormalForm _⟶_
conf⇒nf c aIsNF ε = ε
conf⇒nf c aIsNF (fwd x ◅ rest) = x ◅ conf⇒nf c aIsNF rest
conf⇒nf c aIsNF (bwd y ◅ rest) with c (y ◅ ε) (conf⇒nf c aIsNF rest)
... | _ , _ , x ◅ _ = contradiction (_ , x) aIsNF
... | _ , left , ε = left
conf⇒unf : Confluent _⟶_ → UniqueNormalForm _⟶_
conf⇒unf _ _ _ ε = refl
conf⇒unf _ aIsNF _ (fwd x ◅ _) = contradiction (_ , x) aIsNF
conf⇒unf c aIsNF bIsNF (bwd y ◅ r) with c (y ◅ ε) (conf⇒nf c bIsNF r)
... | _ , ε , x ◅ _ = contradiction (_ , x) bIsNF
... | _ , x ◅ _ , _ = contradiction (_ , x) aIsNF
... | _ , ε , ε = refl
un&wn⇒cr : UniqueNormalForm _⟶_ → WeaklyNormalizing _⟶_ → Confluent _⟶_
un&wn⇒cr un wn {a} {b} {c} aToB aToC with wn b | wn c
... | (d , (d-nf , bToD)) | (e , (e-nf , cToE))
with un d-nf e-nf (a—↠b&a—↠c⇒b↔c (aToB ◅◅ bToD) (aToC ◅◅ cToE))
... | refl = d , bToD , cToE
-- Newman's lemma
sn&wcr⇒cr : StronglyNormalizing _⟶₊_ → WeaklyConfluent _⟶_ → Confluent _⟶_
sn&wcr⇒cr sn wcr = helper (sn _) where
starToPlus : ∀ {a b c} → (a ⟶ b) → b —↠ c → a ⟶₊ c
starToPlus aToB ε = [ aToB ]
starToPlus {a} aToB (e ◅ bToC) = a ∼⁺⟨ [ aToB ] ⟩ (starToPlus e bToC)
helper : ∀ {a b c} → (acc : Acc (flip _⟶₊_) a) →
a —↠ b → a —↠ c → ∃ λ d → (b —↠ d) × (c —↠ d)
helper _ ε snd = -, snd , ε
helper _ fst ε = -, ε , fst
helper (acc g) (toJ ◅ fst) (toK ◅ snd) = result where
wcrProof = wcr toJ toK
innerPoint = proj₁ wcrProof
jToInner = proj₁ (proj₂ wcrProof)
kToInner = proj₂ (proj₂ wcrProof)
lhs = helper (g [ toJ ]) fst jToInner
rhs = helper (g [ toK ]) snd kToInner
fromAB = proj₁ (proj₂ lhs)
fromInnerB = proj₂ (proj₂ lhs)
fromAC = proj₁ (proj₂ rhs)
fromInnerC = proj₂ (proj₂ rhs)
aToInner : _ ⟶₊ innerPoint
aToInner = starToPlus toJ jToInner
finalRecursion = helper (g aToInner) fromInnerB fromInnerC
bMidToDest = proj₁ (proj₂ finalRecursion)
cMidToDest = proj₂ (proj₂ finalRecursion)
result : ∃ λ d → (_ —↠ d) × (_ —↠ d)
result = _ , fromAB ◅◅ bMidToDest , fromAC ◅◅ cMidToDest
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4