Hoare 順序 と Smyth 順序について

Hoare 順序と Smyth 順序についてまとめましょう。

(1) Hoare の場合
定義: X =<h Y   <=>  ∀x∈X, ∃y∈Y, x=<y

- 標準系
	S | ∀s1,s2∈X, s1=/=s2, s1 not=< s2
	(相異なるどの2要素も、互いのsubsumptionでない)

	Sと等価な集合Xは、 S =<h X, X =<h S より
	少なくとも、Sの全要素を含んでおり、かつSの要素にsubsumeされる
	要素は含んでいても良い( X =<h Sに反しない )

	(例)  {1,int} と {int} は等価

- MがXとYのmeet
	M =<h X, M =<h Y
 	∀m∈M, ∃x∈X, ∃y∈Y, m=<x, m=<y (つまり、 m=<meet(x,y))

	ですから、XとYの要素の全組合せのmeetからなる集合がM

- JがXとYのjoin
	X =<h J, Y =<h J
 	∀x∈X, ∃j∈J, x=<j,
 	∀y∈Y, ∃j'∈J, y=<j'

	ですから、XとYの集合のunion がJ

(2) Smyth の場合
定義: X =<s Y   <=>  ∀y∈Y, ∃x∈X, x=<y
- 標準系
	S | ∀s1,s2∈X, s1=/=s2, s1 not=< s2
	(相異なるどの2要素も、互いのsubsumptionでない)

	Sと等価な集合Xは、 S =<s X, X =<s S より
	少なくとも、Sの全要素を含んでおり、かつSの要素をsubsumeする
	要素は含んでいても良い( S =<s Xに反しない )

	(例)  {1,int} と {1} は等価

- MがXとYのmeet
	M =<s X, M =<s Y
 	∀x∈X, ∃m∈M, m=<x,
 	∀y∈Y, ∃m'∈M, m'=<y
	ですから、XとYの集合のunionがM	

- JがXとYのjoin
	X =<h J, Y =<h J
 	∀j∈J, ∃x∈X, ∃y∈Y, x=<j, y=<j (つまり、 join(x,y)=<j)
	ですから、XとYの要素の全組合せのjoinからなる集合がJ