Mercurial > hg > Members > kono > Proof > FirstOrder

changeset 6:d4a148a4809f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Model version
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 13 Aug 2020 12:42:25 +0900
parents 5d1cb6ea2977
children abb61bee093a
files first-order.agda
diffstat 1 files changed, 79 insertions(+), 51 deletions(-) [+]
line wrap: on
line diff
--- a/first-order.agda	Thu Aug 13 11:55:49 2020 +0900
+++ b/first-order.agda	Thu Aug 13 12:42:25 2020 +0900
@@ -7,45 +7,42 @@
 
 module Logic (Atom : Set ) (Const Func Var Pred : Atom → Set)  where
 
-  data Term : Set where
-      *_      : Atom → Term
-      _⟨_⟩    : Atom → Term → Term
-      _,_     : Term → Term → Term
-      _/\_    : Term → Term → Term
-      _\/_    : Term → Term → Term
-      ¬       : Term → Term 
-      all_=>_ : Atom → Term → Term
-      ∃_=>_   : Atom → Term → Term
-
-  data Expr  : Term → Set  where
-     var   : {v : Atom } → Var v → Expr (* v)
-     func  : {x : Atom } { args : Term} → (f : Func x) → Expr args  → Expr ( x ⟨ args ⟩ )
-     const : {c : Atom } → Const c → Expr (* c)
-     args : {x y : Term} → (ex : Expr x) → (ey : Expr y) → Expr ( x , y )
+  data Expr  : Set  where
+     var   : {v : Atom } → Var v → Expr 
+     func  : {x : Atom }  → (f : Func x) → Expr → Expr 
+     const : {c : Atom } → Const c → Expr 
+     args : Expr → Expr  → Expr 
 
-  data Statement : Term → Set where
-     atom  :  {x : Atom } → Pred x → Statement ( * x )
-     predicate  :  {p : Atom } {args : Term } → Pred p → Expr args  → Statement ( p ⟨ args ⟩ )
-     and  :  {x y : Term } → Statement x → Statement y  → Statement ( x /\ y )
-     or   :  {x y : Term } → Statement x → Statement y  → Statement ( x \/ y )
-     not   :  {x : Term } → Statement x → Statement ( ¬ x  )
-     All    :  {x : Atom } { t : Term} → Var x → Statement t → Statement ( all x => t )
-     Exist  :  {x : Atom } { t : Term} → Var x → Statement t → Statement ( ∃ x => t )
+  data Statement : Set where
+     atom       : {x : Atom } → Pred x → Statement 
+     predicate  : {p : Atom }  → Pred p → Expr → Statement 
+     and        : Statement → Statement  → Statement 
+     or         : Statement → Statement  → Statement 
+     not        : Statement  → Statement 
+     All        : {x : Atom } → Var x → Statement → Statement 
+     Exist      : {x : Atom } → Var x → Statement → Statement 
 
+  {-# TERMINATING #-} 
   Model : (ampa :  {x : Atom } → (px :  Pred x ) → Bool )
-       →  (pmap : {p : Atom } { args : Term } → (px :  Pred p ) → Expr args  → Bool )
-       →  (all0   :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool )
-       →  (exist :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool )
-       → {t : Term } → Statement t  → Bool
-  Model amap pmap all0 exist s = model s where
-      model : {t : Term} → Statement t → Bool
+       →  (pmap : {p : Atom }  → (px :  Pred p ) → Expr → Bool )
+       →  (all-const   : List Expr )
+       → ( subst-prop :  {x : Atom } (e : Statement  ) → Var x → (value : Expr ) → Statement  )
+       → Statement  → Bool
+  Model amap pmap all0 sbst s = model s where
+      model :  Statement  → Bool
       model (atom x) = amap x
       model (predicate x x₁) = pmap x x₁
       model (and s s₁) = model s  ∧ model s₁ 
       model (or s s₁) = model s ∨ model s₁ 
       model (not s) = Data.Bool.not (model s )
-      model (All x s) = all0 x s
-      model (Exist x s) = exist x s
+      model (All x s) = model-all all0 x s  where
+          model-all :  List Expr → {x : Atom } → Var x → Statement → Bool
+          model-all [] vx s = true
+          model-all (x ∷ t) vx s = model (sbst s vx x ) ∧ model-all t vx s
+      model (Exist x s) = model-exist all0 x s  where
+          model-exist :  List Expr → {x : Atom } → Var x → Statement → Bool
+          model-exist [] vx s = false
+          model-exist (x ∷ t) vx s = model (sbst s vx x ) ∨ model-exist t vx s
 
 data Atom : Set where
       X : Atom
@@ -99,10 +96,20 @@
 
 open Logic Atom Const Func Var Pred 
 
+data Term : Set where
+      *_      : Atom → Term
+      _⟨_⟩    : Atom → Term → Term
+      _,_     : Term → Term → Term
+      _/\_    : Term → Term → Term
+      _\/_    : Term → Term → Term
+      ¬       : Term → Term 
+      all_=>_ : Atom → Term → Term
+      ∃_=>_   : Atom → Term → Term
+
 ex1 : Term
 ex1 = ¬ ( (* p ) /\ ( all X => ( p ⟨ f ⟨ * X ⟩ ⟩ )))
 
-parse-arg : (t : Term ) → Maybe (Expr t )
+parse-arg : (t : Term ) → Maybe Expr 
 parse-arg (* X) = just (var kX)
 parse-arg (* Y) = just (var kY)
 parse-arg (* Z) = just (var kZ)
@@ -124,7 +131,7 @@
 ... | _ | _ = nothing
 parse-arg _ = nothing
 
-parse : (t : Term ) → Maybe (Statement t )
+parse : (t : Term ) → Maybe Statement 
 parse (* p) = just ( atom kp )
 parse (* q) = just ( atom kq )
 parse (* r) = just ( atom kr )
@@ -169,23 +176,44 @@
 
 ex2 = parse ex1
 
-subst-expr : {e xv : Term } { x : Atom } → Expr e → Var x → (value : Expr xv ) → Expr {!!}
-subst-expr = {!!}
-
-subst-prop : {xv t : Term } {x : Atom } (orig : Statement t ) → Var x → (value : Expr xv ) → Statement {!!}
-subst-prop = {!!}
+subst-expr :  { x : Atom } → Expr  → Var x → (value : Expr ) → Expr 
+subst-expr  (var kX) kX v = v
+subst-expr  (var kY) kX v = var kY
+subst-expr  (var kZ) kX v = var kZ
+subst-expr  (var kX) kY v = var kX
+subst-expr  (var kY) kY v = v
+subst-expr  (var kZ) kY v = var kZ
+subst-expr  (var kX) kZ v = var kX
+subst-expr  (var kY) kZ v = var kY
+subst-expr  (var kZ) kZ v = v
+subst-expr  (func f₁ e) xv v = func f₁ ( subst-expr e xv v ) 
+subst-expr  (const x₁) xv v = (const x₁)
+subst-expr  (args e e₁) xv v = args ( subst-expr e xv v ) ( subst-expr e₁ xv v ) 
 
-ampa :  {x : Atom } → (px :  Pred x ) → Bool 
-ampa {p} px = false
-ampa {q} px = true
-ampa {r} px = false
-pmap : {p : Atom } { args : Term } → (px :  Pred p ) → Expr args  → Bool 
-pmap {p} px (Logic.func kf (Logic.const x)) = true
-pmap {p} px (Logic.func kf _) = false
+subst-prop :  {x : Atom } (e : Statement  ) → Var x → (value : Expr ) → Statement 
+subst-prop (atom x) xv v = atom x
+subst-prop (predicate x x₁) xv v = predicate x ( subst-expr x₁ xv v )
+subst-prop (and e e₁) xv v = and ( subst-prop e xv v ) ( subst-prop e₁ xv v )
+subst-prop (or e e₁) xv v =  or ( subst-prop e xv v ) ( subst-prop e₁ xv v )
+subst-prop (not e) xv v = not ( subst-prop e xv v )
+subst-prop (All x e) xv v = All x ( subst-prop e xv v )
+subst-prop (Exist x e) xv v = Exist x ( subst-prop e xv v )
+
+amap :  {x : Atom } → (px :  Pred x ) → Bool 
+amap {p} px = false
+amap {q} px = true
+amap {r} px = false
+pmap : {p : Atom } → (px :  Pred p ) → Expr → Bool 
+pmap {p} px (Logic.const kc) = true
 pmap {p}  px _ = false
-pmap {q} {y} px _ = false
-pmap {r} {y} px _ = false
-all0   :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool 
-all0   = {!!}
-exist :  {x : Atom } → (px :  Var x ) → { t : Term } → Statement t → Bool 
-exist = {!!}
+pmap {q}  px _ = false
+pmap {r}  px _ = false
+
+all0   :  List Expr
+all0 =  const ka ∷ const kb ∷ const kc ∷ []
+
+test003 : Bool 
+test003 with parse ( ∃ X => ( p  ⟨ * X ⟩ ) )
+test003 | just x = Model amap pmap all0 subst-prop x
+test003 | nothing = false
+