99 lines
2.7 KiB
Agda
99 lines
2.7 KiB
Agda
|
{-# OPTIONS --guardedness #-}
|
|||
|
|
{-# OPTIONS --allow-unsolved-metas #-}
|
|||
|
|
|
|||
|
|
open import Data.Unit
|
|||
|
|
open import Data.Bool using (Bool)
|
|||
|
|
import Data.Bool as Bool
|
|||
|
|
open import Data.Fin using (Fin)
|
|||
|
|
import Data.Fin as Fin
|
|||
|
|
open import Data.Nat
|
|||
|
|
open import Relation.Nullary.Decidable using (Dec)
|
|||
|
|
|
|||
|
|
module Owen where
|
|||
|
|
|
|||
|
|
data Con (S : Set) : Set where
|
|||
|
|
• : Con S
|
|||
|
|
_▷_ : Con S -> S -> Con S
|
|||
|
|
|
|||
|
|
data Var {S : Set} : Con S -> S -> Set where
|
|||
|
|
q : {A : S} -> {Γ : Con S} -> Var (Γ ▷ A) A
|
|||
|
|
p_ : {A B : S} -> {Γ : Con S} -> Var Γ A -> Var (Γ ▷ B) A
|
|||
|
|
|
|||
|
|
module RegularLogic (Sort : Set) (Rel : Con Sort -> Set) where
|
|||
|
|
variable Γ Δ : Con Sort
|
|||
|
|
variable A B : Sort
|
|||
|
|
Tm = Var
|
|||
|
|
Sub : Con Sort -> Con Sort -> Set
|
|||
|
|
Sub Γ Δ = (A : Sort) -> Tm Δ A -> Tm Γ A
|
|||
|
|
|
|||
|
|
data Prop : Con Sort -> Set where
|
|||
|
|
true : Prop Γ
|
|||
|
|
_$_ : Rel Δ -> Sub Γ Δ -> Prop Γ
|
|||
|
|
_∧_ : Prop Γ -> Prop Γ -> Prop Γ
|
|||
|
|
_===_ : Tm Γ A -> Tm Γ A -> Prop Γ
|
|||
|
|
∃ : Prop (Γ ▷ A) -> Prop Γ
|
|||
|
|
|
|||
|
|
record Axiom : Set where
|
|||
|
|
field
|
|||
|
|
con : Con Sort
|
|||
|
|
ante : Prop con
|
|||
|
|
cons : Prop con
|
|||
|
|
|
|||
|
|
record Sig : Set where
|
|||
|
|
field
|
|||
|
|
sorts : Con ⊤
|
|||
|
|
rels : Con (Con (Var sorts tt))
|
|||
|
|
|
|||
|
|
Sort : (S : Sig) -> Set
|
|||
|
|
Sort S = Var (Sig.sorts S) tt
|
|||
|
|
|
|||
|
|
Rel : (S : Sig) -> Con (Sort S) -> Set
|
|||
|
|
Rel S = Var (Sig.rels S)
|
|||
|
|
|
|||
|
|
record Theory : Set where
|
|||
|
|
field
|
|||
|
|
sig : Sig
|
|||
|
|
axioms : Con (RegularLogic.Axiom (Sort sig) (Rel sig))
|
|||
|
|
|
|||
|
|
Tuple : (S : Sig) -> (Sort S -> ℕ) -> Con (Sort S) -> Set
|
|||
|
|
Tuple S elts Γ = (A : Sort S) -> Var Γ A -> Fin (elts A)
|
|||
|
|
|
|||
|
|
record ModelData (S : Sig) : Set where
|
|||
|
|
field
|
|||
|
|
elts : Sort S -> ℕ
|
|||
|
|
sat : {Γ : Con (Sort S)} -> Rel S Γ -> Tuple S elts Γ -> Bool
|
|||
|
|
|
|||
|
|
module Interp (S : Sig) (M : ModelData S) where
|
|||
|
|
open RegularLogic (Sort S) (Rel S)
|
|||
|
|
t = Tuple S (ModelData.elts M)
|
|||
|
|
|
|||
|
|
Elt : Sort S -> Set
|
|||
|
|
Elt A = Fin (ModelData.elts M A)
|
|||
|
|
|
|||
|
|
extend : (Γ : Con (Sort S)) -> t Γ -> (A : Sort S) -> Elt A -> t (Γ ▷ A)
|
|||
|
|
extend = {!!}
|
|||
|
|
|
|||
|
|
any : {n : ℕ} -> (Fin n -> Bool) -> Bool
|
|||
|
|
any = {!!}
|
|||
|
|
|
|||
|
|
allTuples : (Γ : Con (Sort S)) -> (t Γ -> Bool) -> Bool
|
|||
|
|
allTuples = {!!}
|
|||
|
|
|
|||
|
|
eval : {Γ : Con (Sort S)} -> {A : Sort S} -> Tm Γ A -> t Γ -> Elt A
|
|||
|
|
eval {Γ} {A} v f = f A v
|
|||
|
|
|
|||
|
|
evalSub : {Γ Δ : Con (Sort S)} -> Sub Γ Δ -> t Γ -> t Δ
|
|||
|
|
evalSub s f A v = f A (s A v)
|
|||
|
|
|
|||
|
|
interp : {Γ : Con (Sort S)} -> Prop Γ -> t Γ -> Bool
|
|||
|
|
interp true _ = Bool.true
|
|||
|
|
interp (r $ xs) f = ModelData.sat M r (evalSub xs f)
|
|||
|
|
interp (ϕ ∧ ψ) f = interp ϕ f Bool.∧ interp ψ f
|
|||
|
|
interp (x₁ === x₂) f = Dec.does (eval x₁ f Fin.≟ eval x₂ f)
|
|||
|
|
interp (∃ {Γ} {A} ϕ) f = any (λ i -> interp ϕ (extend Γ f A i))
|
|||
|
|
|
|||
|
|
satisfies : Axiom -> Bool
|
|||
|
|
satisfies a = allTuples
|
|||
|
|
(Axiom.con a)
|
|||
|
|
(λ f -> Dec.does (interp (Axiom.ante a) f Bool.≤? interp (Axiom.cons a) f))
|