Skip to content

Commit

Permalink
induction non termination
Browse files Browse the repository at this point in the history
  • Loading branch information
@AlecsFerra
AlecsFerra committed May 26, 2023
1 parent aee9513 commit 0e80b44
Show file tree
Hide file tree
Showing 2 changed files with 57 additions and 28 deletions.
16 changes: 12 additions & 4 deletions src/FAlgebra.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,18 +5,26 @@ module FAlgebra where
open import GeneralizedPolynomial
using (Polynomial; ⟦_⟧; ⟦_⟧₀; ⟦_⟧₁; K_; ∅; _,_)
open import Relation.Binary.PropositionalEquality
open import Data.Product using (_,_)
open import Data.Sum using (inj₁; inj₂)
open import Data.Nat using (suc)

open Polynomial
open GeneralizedPolynomial.LeastFixpoint

Algebra : Polynomial 1 → Set → Set
Algebra F A = ⟦ F ⟧₁ A → A

-- lemma : (F : Polynomial) → ⟦ F ⟧₁ ⟦ μ F ⟧ₒ ≡ ⟦ F ⟧₁ (∅, μ F)

cata : {F : Polynomial 1} {A : Set} → Algebra F A → ⟦ μ F ⟧₀ → A
cata {F} ϕ μ⟨ x ⟩ = ϕ (mapCata F F ϕ x)
cata {F} ϕₒ μ⟨ x ⟩ = ϕₒ (mapCata F F ϕₒ x)
where
mapCata : {X : Set} → (F G : Polynomial 1) → Algebra G X → ⟦ F ⟧ (∅ , (μ G)) → ⟦ F ⟧₁ X
mapCata {X} F G ϕ x = {!!}
mapCata {X} (I 0) G ϕ μ⟨ x ⟩ = ϕ (mapCata G G ϕ x)
mapCata {X} (L ⊕ᵣ R) G ϕ (inj₁ xₗ) = inj₁ (mapCata L G ϕ xₗ)
mapCata {X} (L ⊕ᵣ R) G ϕ (inj₂ xᵣ) = inj₂ (mapCata R G ϕ xᵣ)
mapCata {X} (L ⊗ᵣ R) G ϕ (xₗ , xᵣ) = mapCata L G ϕ xₗ , mapCata R G ϕ xᵣ
mapCata {X} (μ F) G ϕ μ⟨ x ⟩ = μ⟨ ? ⟩
mapCata {X} (ν F) G ϕ x = {!!}
mapCata {X} (wk_ {0} P) G ϕ x = x
mapCata {X} (wk_ {1} P) G ϕ x = mapCata P G ϕ x

69 changes: 45 additions & 24 deletions src/GeneralizedPolynomial.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,11 @@ module GeneralizedPolynomial where
open import Data.Sum using (_⊎_)
open import Data.Product using (_×_; ∃-syntax; _,_)
open import Relation.Binary.PropositionalEquality
using (refl; ≢-sym)
using (refl; ≢-sym; _≡_)
open import Data.Nat
using (ℕ; suc; _<_; _≤_; _⊔_; s≤s; z≤n; _≟_; _≤?_; _<?_)
open import Data.Nat.Properties
using (≤-reflexive; ≤-trans; ≤-step; n≤1+n; ≤∧≢⇒<; ≤-pred)
using (≤-reflexive; ≤-trans; ≤-step; n≤1+n; ≤∧≢⇒<; ≤-pred; <⇒≤)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable
using (True; toWitness; fromWitness)
Expand All @@ -24,22 +24,32 @@ private module ℕExtra where
m≤n⊔m {0} {m} = ≤-reflexive refl
m≤n⊔m {suc n} {0} = z≤n
m≤n⊔m {suc n} {suc m} = s≤s m≤n⊔m


open ℕExtra

infixl 6 _⊕ᵣ_
infixl 7 _⊗ᵣ_
infixl 6 _⊕_
infixl 7 _⊗_
infixr 8 μ_
infixr 8 ν_

data Polynomial : ℕ → Set₁ where
I_ : {n : ℕ} → (m : ℕ) → {True (m <? n)} → Polynomial n
K_ : Set → Polynomial 0
_⊗_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
_⊕_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
μ_ : {n : ℕ} → Polynomial (suc n) → Polynomial n
ν_ : {n : ℕ} → Polynomial (suc n) → Polynomial n
I_ : {n : ℕ} → (m : ℕ) → {True (m <? n)} → Polynomial n
K_ : Set → Polynomial 0
μ_ : {n : ℕ} → Polynomial (suc n) → Polynomial n
ν_ : {n : ℕ} → Polynomial (suc n) → Polynomial n

-- Shouldn't be used explicitly by users of the lib
_⊕ᵣ_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
_⊗ᵣ_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
wk_ : {n m : ℕ} → Polynomial n → {True (n ≤? m)} → Polynomial m

-- Versions that infer weakening
_⊗_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
L ⊗ R = (wk_ L {fromWitness n≤n⊔m}) ⊗ᵣ (wk_ R {fromWitness m≤n⊔m})

_⊕_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
L ⊕ R = (wk_ L {fromWitness n≤n⊔m}) ⊕ᵣ (wk_ R {fromWitness m≤n⊔m})

data Context : ℕ → Set₁ where
∅ : Context 0
Expand All @@ -59,24 +69,33 @@ lookup (ctx , _) (suc m) {s≤s p} with lookup ctx m {p}
-- A = I 0 ⊕ I 1
-- B = I 0
-- A ⊗ B
weaken : ∀ {n m : ℕ} → (m ≤ n) → Context n → Context m
weaken {0} {0} z≤z ∅ = ∅
weaken {suc n} {m} m≤n ctx@(rest , _) with suc n ≟ m
weaken-context : ∀ {n m : ℕ} → (m ≤ n) → Context n → Context m
weaken-context {0} {0} z≤z ∅ = ∅
weaken-context {suc n} {m} m≤n ctx@(rest , _) with suc n ≟ m
... | yes refl = ctx
... | no n≢m = weaken (≤-pred (≤∧≢⇒< m≤n (≢-sym n≢m))) rest
... | no n≢m = weaken-context (≤-pred (≤∧≢⇒< m≤n (≢-sym n≢m))) rest

open import Data.Nat.Induction

mutual
{-# TERMINATING #-}
eval-impl : _
eval-impl 0 rec (K x) ctx = x
eval-impl (suc n) rec (I_ m {m<n}) ctx with lookup ctx m {toWitness m<n}
... | p , X , p<n = rec p p<n X
(weaken-context (≤-trans (≤-pred p<n)
(n≤1+n _)) ctx)
eval-impl n rec (wk_ {f} {m} P {f≤m}) ctx with f ≟ m
... | yes refl = eval-impl _ rec P ctx
... | no f≢m = rec f (≤∧≢⇒< (toWitness f≤m) f≢m) P
(weaken-context (toWitness f≤m) ctx)
eval-impl n rec (μ P) ctx = LeastFixpoint P ctx
eval-impl n rec (ν P) ctx = GreatestFixpoint P ctx
eval-impl n rec (L ⊕ᵣ R) ctx = eval-impl _ rec L ctx ⊎ eval-impl _ rec R ctx
eval-impl n rec (L ⊗ᵣ R) ctx = eval-impl _ rec L ctx × eval-impl _ rec R ctx


eval : {n : ℕ} → Polynomial n → Context n → Set
eval ((I m) {m<n}) ctx with lookup ctx m {toWitness m<n}
... | p , X , s≤s p<n = eval X (weaken (≤-trans p<n (n≤1+n _)) ctx)
eval (K x) ctx = x
eval (L ⊗ R) ctx = eval L (weaken n≤n⊔m ctx) × eval R (weaken m≤n⊔m ctx)
eval (L ⊕ R) ctx = eval L (weaken n≤n⊔m ctx) ⊎ eval R (weaken m≤n⊔m ctx)
eval (μ P) ctx = LeastFixpoint P ctx
eval (ν P) ctx = GreatestFixpoint P ctx
eval {n} = <-rec _ eval-impl n

data LeastFixpoint {n : ℕ} (P : Polynomial (suc n)) (ctx : Context n) : Set where
μ⟨_⟩ : eval P (_,_ ctx {fromWitness (≤-reflexive refl)} (μ P)) → LeastFixpoint P ctx
Expand All @@ -85,11 +104,13 @@ mutual
coinductive
field rest : eval P (_,_ ctx {fromWitness (≤-reflexive refl)} (ν P))

⟦_⟧ : ∀ {n m : ℕ} → {n≤m : True (n ≤? m)} → Polynomial n → Context m → Set
⟦_⟧ {_} {_} {n≤m} F ctx = eval F (weaken (toWitness n≤m) ctx)

⟦_⟧ : {n m : ℕ} → {n≤m : True (n ≤? m)} → Polynomial n → Context m → Set
⟦_⟧ {_} {_} {n≤m} F ctx = eval F (weaken-context (toWitness n≤m) ctx)

⟦_⟧₁ : Polynomial 1 → Set → Set
⟦ P ⟧₁ X = ⟦ P ⟧ (∅ , K X)

⟦_⟧₀ : Polynomial 0 → Set
⟦ P ⟧₀ = ⟦ P ⟧ ∅

0 comments on commit 0e80b44

Please sign in to comment.