1. Toshimi Sawada Avatar Toshimi Sawada
  2. Untitled project
  3. CafeOBJ

Wiki

Clone wiki

CafeOBJ / OSEK / contents / ceiling

View History

半順序集合の極

任意の半順序集合を（S,R）とする． Sの要素xが，任意のSの要素yに対して y R x とならないとき， x をRに関するSの極と呼ぶことにする． このとき，次の定理が成り立つ．

定理：Sが空でなければ，SにはRに関する極が存在する．

これを論理式で表現すると，S ≠ {} ⇒ ∃x∈S・（∀y∈S・¬（y R x））となる． これを証明しよう．

CafeOBJによる定理の表現

上の定理をCafeOBJで証明するためには，定理そのものをCafeOBJで表現する必要がある．

まず，関係Rを次のように集合上に拡張する．

#!python

module EXTEND
(
  X :: TRIV,
  C :: SET(X),
  R :: RELATION(X)
)
{
  signature
  {
    op  ___ : Set Relation Set -> Prop
  }
  axioms
  {
    vars X Y : Elt
    vars C D S : Set
    vars R : Relation
    eq X R nil = true .
    eq nil R C = false .
    eq X R (C,Y) = (X R C) and (X R Y) .
    eq (S,X) R C = (S R C) or (X R C) .
  }  
}

２つの集合SとTに対して，Tの全ての要素yに対して x R y が真となる要素xがSに存在するとき， S R T は真となる．

次に，２項関係の反転を次のように宣言する．

#!python
module REVERSE
(
  X :: TRIV,
  R :: RELATION(X)
)
{
  signature
  {
    op ~ : Relation -> Relation
  }
  axioms
  {
    vars X Y : Elt
    vars R : Relation
    eq X ~(R) Y = Y R X .
  }  
}

モジュールREVERSEでは，関係を反転させる演算~を宣言している． 任意の項xおよびyに対し，x ~(R) y が真になるのは y R x が真になるときである．

#!python
module NEGATE
(
  X :: TRIV,
  R :: RELATION(X)
)
{
  signature
  {
    op ! : Relation -> Relation
  }
  axioms
  {
    vars X Y : Elt
    vars R : Relation
    eq X !(R) Y = (not X R Y) .
  }  
}

モジュールNAGATEで宣言されている演算!は，いわば関係の否定を表す． 任意の項xとyに対し，x R y が偽となるとき，x !(R) y は真となる．

任意の集合CとC上の関係Rに対して， Cに関係Rに関する極が存在することはC !(~(R)) C で表現できる． 任意のCの要素yに対して，x !(~(R)) y が真となる要素xが存在することは C !(~(R)) C は真となることと等価であり， x !(~(R)) y が真であることは，not(x ~(R) y) が真，すなわち， not(y R x) が真であることと等価である．

補題

さて，上に挙げた性質を証明する前に，補題を１つ証明しておこう． CをソートSの項を要素とする任意の集合，RをS上の推移的関係，xとyをSの任意の項とし， x !(~R)) C が成り立つとする． このとき，y R x であれば，y !(~(R)) C が成り立つ． この補題は，次のモジュールで宣言される演算inheritを用いて表されるシーケント inherit(x,y,C,R)で表現される．

#!python
module INHERIT
(
  X :: TRIV,
  C :: SET(X),
  R :: RELATION(X),
  T :: TRANSITIVE(X,R),
  N :: NEGATE(X,R),
  V :: REVERSE(X,R),
  E :: EXTEND(X,C,R)
)
{
  imports 
  {
    pr(SEQUENT)
  }
  signature {
    op inherit : Elt Elt Set Transitive -> Sequent
  }
  axioms
  {
    vars X Y : Elt
    vars C : Set
    vars R : Transitive
    eq inherit(X,Y,C,R) = (Y R X), (X !(~(R)) C) |- (Y !(~(R)) C) .
  }
}

補題の証明

任意の集合c，推移的関係r，並びにcの要素x，yに対して， シーケントinherit(x,y,c,r)が真となることをcに関する構造帰納法を用いて示そう．

まず，cが空である場合にinherit(x,y,c,r)が真になることを示す．

#!python
open INHERIT .
ops x y : -> Elt .
ops c : -> Set .
ops r : -> Transitive .
eq c = nil .
red hold(inherit(x,y,c,r)) = true .
close

これを実行すると次のようになる．

#!python

CafeOBJ> open INHERIT .
opening module INHERIT(X, C, R, T, N, V, E).. done.
%INHERIT(X, C, R, T, N, V, E)> ops x y : -> Elt .
%INHERIT(X, C, R, T, N, V, E)> ops c : -> Set .
%INHERIT(X, C, R, T, N, V, E)> ops r : -> Transitive .
%INHERIT(X, C, R, T, N, V, E)> eq c = nil .
_
%INHERIT(X, C, R, T, N, V, E)> red hold(inherit(x,y,c,r)) = true .
*
reduce in %INHERIT(X, C, R, T, N, V, E) : (hold(inherit(x,y,c,r)) = true):Bool
(true):Bool
(0.000 sec for parse, 7 rewrites(0.000 sec), 28 matches)
%INHERIT(X, C, R, T, N, V, E)> close
CafeOBJ>

次に，inherit(x,y,c,r)が真であると仮定しよう． このとき，cに新たに要素zを追加してできる集合nに対しても， inherit(x,y,n,r)が真になることを示す．

#!python

open INHERIT + LK .
ops x y z : -> Elt .
ops r : -> Transitive .
ops c n : -> Set .
eq n = (c,z) .

帰納法の仮定「inherit(x,y,n,r)が真」であることは次のように宣言される． 最初に，見やすさのため(x !(~(r)) c)と(y !(~(r)) c)を各々pxとpyに略記しておく．

#!python

ops px py : -> Prop .
eq (x !(~(r)) c) = px .
eq (y !(~(r)) c) = py .

演算holdには評価戦略を陽に与えていないため， 項hold(inherit(x,y,c,r))の簡約は引数inherit(x,y,c,r)の簡約から始まる． その場合，inherit(x,y,c,r) が真であることを直接等式

#!python

eq hold(inherit(x,y,c,r)) = true .

で宣言しても，この等式は簡約に適用されない． ここでは，inherit(x,y,c,r)を簡約した項((y r x), px |- py)が真であることを等式で宣言し， inherit(x,y,c,r)が真と評価されるようにしている．

#!python

eq hold((y r x), px |- py) = true .

実際にこれで帰納法の仮定が成り立つことは次の簡約で確かめられる．

#!python

red hold(inherit(x,y,c,r)) .

以下に示す簡約結果にあるように，帰納法の仮定は成り立っている．

#!python

-- reduce in %RULE + INHERIT + INFERENCE(X.INHERIT, C.INHERIT, R.INHERIT, T.INHERIT, N.INHERIT, V.INHERIT, E.INHERIT) : 
    (hold(inherit(x,y,c,r))):Bool
(true):Bool
(0.000 sec for parse, 4 rewrites(0.000 sec), 21 matches)
%RULE + INHERIT + INFERENCE(X.INHERIT, C.INHERIT, R.INHERIT, T.INHERIT, N.INHERIT, V.INHERIT, E.INHERIT)>

それでは，集合cに要素zを加えた集合nに対しても，inherit(x,y,n,r)が真となることを示そう． 次の推論iとjを考えCafeOBJで次のように記述する．

inference1.jpg

推論iは，次のように記述できる

#!python

ops i j : -> Inference .
eq antecedent(i) = ((y r x), (z r y), px |- (z r x)) .
trans ((y r x), (not z r x), px |- (not z r y)) => consequent(i) .
trans consequent(i) => ((y r x), (not z r x), px |- (not z r y)) .

推論iの前提((y r x), (z r y), px├ (z r x))は関係rの推移律より正しい． 推論iの結論は，このシーケントから命題(z r y)と(z r x)を入れ替えて得られる． 因みに，結論の表現方法は，両方向の書換規則により表現される． これは，モジュールINFERENCEで表される推論を積み重ねる場合， 先の推論の結論を後の推論の前提として扱えるようにするためである． 一般に，書換論理では，両方向の書換規則は等式と等価になるので， この２つの書換規則で，書換の両辺は等しいことが表される．

推論jは次のように記述される．

#!python

op j : -> Inference .
eq antecedent(j) = (consequent(i), ((y r x), (not z r x), px |- py)) .
eq ((y r x), ((not z r x) and px) |- ((not z r y) and py)) = consequent(j) .

推論jの前提は，推論iの結論にシーケント((y r x), (not z r x), px |- py))を加えたものである． シーケントの左辺への∧導入規則により，この２つのシーケントから ((y r x), ((not z r x) and px) |- ((not z r y) and py))という， inherit(x,y,n,r)と等価なシーケントが導かれる． なお，ここでは，推論jの結論consequent(j)を等式で定めている． これは，jの結論を他の推論の前提として扱う必要がないからである．

ここで，シーケントinherit(x,y,n,r)が真になることを確かめよう．

#!python

red hold(inherit(x,y,n,r)) .

項hold(inherit(x,y,n,r))はtrueに書換えられる．

#!python

%LK + INHERIT(X.INHERIT, C.INHERIT, R.INHERIT, T.INHERIT, N.INHERIT, V.INHERIT, E.INHERIT)> red hold(inherit(x,y,n,r)) .
-- reduce in %LK + INHERIT(X.INHERIT, C.INHERIT, R.INHERIT, T.INHERIT, N.INHERIT, V.INHERIT, E.INHERIT) : 
    (hold(inherit(x,y,n,r))):Bool

** Found [state 265] (consequent(j)):Sequents
   {}
-- found required number of solutions 1.

** Found [state 95] (consequent(i)):Sequents
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 3477 rewrites(1.180 sec), 292338 matches, 1570 memo hits)

以上より，xとyをソートSの任意の項，CをソートSの項を要素に持つ任意の集合，RをS上の推移的関係とすると， シーケント (y R x), (x !(~(R)) C)├ (y !(~(R)) C)が真となることが証明されたので， モジュールINHERITを次のように書き換えよう．

#!python

module INHERIT
(
  X :: TRIV,
  C :: SET(X),
  R :: RELATION(X),
  T :: TRANSITIVE(X,R),
  N :: NEGATE(X,R),
  V :: REVERSE(X,R),
  E :: EXTEND(X,C,R)
)
{
  imports
  {
    pr(JUDGEMENT)
  }
  axioms
  {
    vars X Y : Elt
    vars C : Set
    vars R : Transitive
    eq hold((Y R X), (X !(~(R)) C) |- (Y !(~(R)) C)) = true .
  }
}

定理の証明

それでは，この補題を用いて冒頭に紹介した定理を証明しよう． 定理の主張を宣言するモジュールBOUNDEDを宣言する．

#!python

module BOUNDED
(
  X :: TRIV,
  C :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIAL-ORDER(X,R,I,A,T),
  N :: NEGATE(X,R),
  V :: REVERSE(X,R),
  E :: EXTEND(X,C,R),
  L :: INHERIT(X,C,R,T,N,V,E)
)
{
  imports
  {
    pr(SEQUENT)
  }
  signature
  {
    op bounded : Set PartialOrder -> Sequent
  }
  axioms
  {
    vars C : Set
    vars R : PartialOrder
    eq bounded(C,R) = (not C = nil) |- (C !(~(R)) C) .
  }
}

定理の主張は， 「（C,R）を任意の半集合とすると，Cが空でなければCはRに関する極を持つ」ことであった， これは，上のモジュールで宣言した演算を用いれば，bounded(C,R)と書ける． この主張が真であることを，Cに関する構造帰納法で示そう．

まず，Cが空集合の場合に主張が真であることを示す．

#!python


-- [base case] c = nil
open BOUNDED .
op c : -> Set .
op r : -> PartialOrder .
eq c = nil .
red hold(bounded(c,r)) .
close

この証明譜を実行すると，主張bounded(c,r)は真であることがわかる．

#!python

CafeOBJ> -- opening module BOUNDED(X, C, R, I, A, T, P, N, V, E, L).. done.
%BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> %BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> %BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> _
%BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> *
-- reduce in %BOUNDED(X, C, R, I, A, T, P, N, V, E, L) : 
    (hold(bounded(c,r))):Bool
(true):Bool
(0.000 sec for parse, 8 rewrites(0.000 sec), 29 matches)

次に，cに対して主張が真であることを仮定して， cに要素xを付け加えた集合nでも主張が真になることを示す．

ここで，cが空である場合と空でない場合に場合分けを行う．

【場合１】cが空である場合

この場合，証明譜は次のように書ける．

#!python

-- [induction step]
-- [case division]
-- [case1] c = nil
open BOUNDED .
ops c n : -> Set .
ops x : -> Elt .
ops r : -> PartialOrder .
eq n = (c,x) .
eq c = nil .
red hold(bounded(n,r)) .
close

この証明譜を実行すると，確かに主張は真になることがわかる．

#!python


-- opening module BOUNDED(X, C, R, I, A, T, P, N, V, E, L).. done.
%BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> %BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> %BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> %BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> _
%BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> %BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> *
-- reduce in %BOUNDED(X, C, R, I, A, T, P, N, V, E, L) : 
    (hold(bounded(n,r))):Bool
(true):Bool
(0.000 sec for parse, 12 rewrites(0.000 sec), 38 matches)

【場合２】cが空でない場合

帰納法の仮定より，cにはrに関する極yが存在する． cからyを取り除いた集合をsと置き，cをsとyの和で表現しよう．

#!python


-- [case2] not c = nil
open BOUNDED .
ops x y : -> Elt .
ops r : -> PartialOrder .
ops s c n : -> Set .
eq c = (s,y) .
eq n = (c,x) .

(y !(~(r)) c) は (y !(~(r)) s) に簡約されるので， yがrに関するcの極であることを次のように宣言する．

#!python

eq (y !(~(r)) s) = true .

そして，xとyに関して，次の２つの場合を考える．

【場合2a】(x r y)が真でない

【場合2b】(x r y)が真である

(x r y)が真でない場合は，次の証明譜により主張が成り立つことが容易に示せる．

#!python


-- [case division]
-- [case2a] (not x r y) = true
eq (not x r y) = true .
red hold(bounded(n,r)) .
close

この証明譜の実行結果は次のようになる．

#!python


%BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> %BOUNDED(X, C, R, I, A, T, P, N, V, E, L)> *
-- reduce in %BOUNDED(X, C, R, I, A, T, P, N, V, E, L) : 
    (hold(bounded(n,r))):Bool
(true):Bool
(0.000 sec for parse, 30 rewrites(0.000 sec), 444 matches)

(x r y)が真である場合は，LKに基く推論を用いて次のように証明される． (x r y)が真でない場合と同様に，要素x,y，半順序r，集合s,c,nを各々次のように宣言する．

#!python

-- [case2b] (x r y) = true
open BOUNDED + LK .
ops x y : -> Elt .
ops r : -> PartialOrder .
ops s c n : -> Set .
eq c = (s,y) .
eq n = (c,x) .

ここで，yがrに関するcの極であることや（x r y）が真であることをシーケントを用いて次のように表す．

#!python


eq hold(nil |- (y !(~(r)) s)) = true .
eq hold(nil |- x r y) = true .

そして，証明に不要な項を纏めてpと略記することにする．

#!python

ops p : -> Prop .
eq ((s !(~(r)) (s , (y , x))) or ((y !(~(r)) s) and (not (x r y)))) = p .

このとき，主張が真であることは下の推論で示せる．

inference2.jpg

各推論i,j,kをCafeOBJで証明譜として記述すると以下のようになる．

#!python

ops s1 s2 s3 s4 : -> Sequent .
eq s1 = ((x r y),(y !(~(r)) s) |- ((x !(~(r)) s), p)) .
eq s2 = (nil |- x r y) .
eq s3 = (nil |- (y !(~(r)) s)) .
eq s4 = (((x r y), (y r x)) |- nil) .
ops i j k : -> Inference .
eq antecedent(i) = (s1,s2,s3) .
trans (nil |- ((x !(~(r)) s), p)) => consequent(i) .
trans consequent(i) => (nil |- ((x !(~(r)) s), p)) .
eq antecedent(j) = (s2,s4) .
trans (nil |- (not y r x)) => consequent(j) .
trans consequent(j) => (nil |- (not y r x)) .
eq antecedent(k) = (consequent(i),consequent(j)) .
eq (nil |- (((x !(~(r)) s) and (not y r x)) or p)) = consequent(k) .

ここで，consequent(k)はbounded(n,r)と等しい

#!python

red bounded(n,r) == consequent(k) .

%LK + BOUNDED(X.BOUNDED, C.BOUNDED, R.BOUNDED, I.BOUNDED, A.BOUNDED, T.BOUNDED, P.BOUNDED, N.BOUNDED, V.BOUNDED, E.BOUNDED, L.BOUNDED)> red bounded(n,r) == consequent(k) .
-- reduce in %LK + BOUNDED(X.BOUNDED, C.BOUNDED, R.BOUNDED, I.BOUNDED, A.BOUNDED, T.BOUNDED, P.BOUNDED, N.BOUNDED, V.BOUNDED, E.BOUNDED, L.BOUNDED) : 
    (bounded(n,r) == consequent(k)):Bool
(true):Bool
(0.000 sec for parse, 28 rewrites(0.000 sec), 819 matches)

主張が正しいことを示すには，次の簡約を実行すればよい．

#!python

red hold(bounded(n,r)) .
close

%LK + BOUNDED(X.BOUNDED, C.BOUNDED, R.BOUNDED, I.BOUNDED, A.BOUNDED, T.BOUNDED, P.BOUNDED, N.BOUNDED, V.BOUNDED, E.BOUNDED, L.BOUNDED)> red hold(bounded(n,r)) .
-- reduce in %LK + BOUNDED(X.BOUNDED, C.BOUNDED, R.BOUNDED, I.BOUNDED, A.BOUNDED, T.BOUNDED, P.BOUNDED, N.BOUNDED, V.BOUNDED, E.BOUNDED, L.BOUNDED) : 
    (hold(bounded(n,r))):Bool

** Found [state 35] (consequent(k)):Sequents
   {}
-- found required number of solutions 1.

** Found [state 27] (consequent(j)):Sequents
   {}
-- found required number of solutions 1.

** Found [state 1925] (consequent(i)):Sequents
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 6639 rewrites(7.130 sec), 1040611 matches, 3944 memo hits)

この定理に基き，任意の半順序集合を（C,R）とすると， CからRに関する極を１つ取り出す演算を定義しても構わないことが保証される．

#!python

module CEILING
(
  X :: TRIV,
  C :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIAL-ORDER(X,R,I,A,T)
)
{
  signature
  {
    op  ceiling : Set PartialOrder -> Elt
  }
  axioms
  {
    vars X : Elt
    vars C : Set
    vars R : PartialOrder
    cq ceiling(C,R) @ C = true
       if not(C = nil) .
    cq not(X R ceiling(C,R)) = true
       if not(C = nil) and X @ C .
  }
}

Updated