かじもとにっき

自分用メモ

pseudosemilatticeとcopseudosemilattice

数学

定義 (pseudosemilatticeとcopseudosemilattice)

\mathcal A \text{ is a pseudosemilattice } \overset{\text{def}}{\equiv} \mathcal A \text{ is a poset } \wedge \mathcal A \text{ is } \mathbf 2 \text{-complete } ,
\mathcal A \text{ is a copseudosemilattice } \overset{\text{def}}{\equiv} \mathcal A \text{ is a poset } \wedge \mathcal A \text{ is } \mathbf 2 \text{-cocomplete }
  where \mathbf 2 = (\{0,1\},=_{\{0,1\}}) .

\langle x,y \rangle \in A \leftarrow \{0,1\}に対し、\sqcap\langle x,y \rangleをx \sqcap y、\sqcup\langle x,y \rangleをx \sqcup yと書く。

定理 (idempotency)

(A,\sqsubseteq)\text{ is }(B,\preceq)\text{-complete} \wedge B \neq \emptyset \Rightarrow \sqcap \bullet K = I_A ,
(A,\sqsubseteq)\text{ is }(B,\preceq)\text{-cocomplete} \wedge B \neq \emptyset \Rightarrow \sqcup \bullet K = I_A .

証明

任意のx \in Aに対し:

  x \sqsubseteq \sqcap (K.a)
\Leftrightarrow  { \sqcap-definition }
  \langle\forall b \in B :: x \sqsubseteq K.a.b \rangle
\Leftrightarrow  { K-definition }
  \langle\forall b \in B :: x \sqsubseteq a \rangle
\Leftrightarrow  { B\neq\emptyset }
  x \sqsubseteq a .

従ってindirect equalityにより\langle\forall a \in A :: \sqcap (K.a) = a \rangle。

supremumに関しても同様。

∎

特に、x \in A \Rightarrow \langle x, x \rangle = K.x \in A \leftarrow \mathbf \{0,1\}なので、

\mathcal (A,\sqsubseteq) \text{ is a pseudosemilattice } \Rightarrow \langle\forall x \in A ::  x \sqcap x = x \rangle ,
\mathcal (A,\sqsubseteq) \text{ is a copseudosemilattice } \Rightarrow \langle\forall x \in A ::  x \sqcup x = x \rangle .

定理 (associativity)

\mathcal (A,\sqsubseteq) \text{ is a pseudosemilattice } \Rightarrow \langle\forall x,y,z \in A ::  (x \sqcap y) \sqcap z = x \sqcap (y \sqcap z) \rangle ,
\mathcal (A,\sqsubseteq) \text{ is a copseudosemilattice } \Rightarrow \langle\forall x,y,z \in A ::  (x \sqcup y) \sqcup z = x \sqcup (y \sqcup z) \rangle .

証明

x,y,z \in Aを仮定し、任意のa \in Aに対し:

  a \sqsubseteq (x \sqcap y) \sqcap z
\Leftrightarrow  { \sqcap-definition }
  a \sqsubseteq x \sqcap y \wedge a \sqsubseteq z
\Leftrightarrow  { \sqcap-definition }
  a \sqsubseteq x \wedge a \sqsubseteq y \wedge a \sqsubseteq z
\Leftrightarrow  { \sqcap-definition }
  a \sqsubseteq x \wedge a \sqsubseteq y \sqcap z
\Leftrightarrow  { \sqcap-definition }
  a \sqsubseteq x \sqcap (y \sqcap z) .

supremumに関しても同様。

∎

定理 (commutativity)

\mathcal (A,\sqsubseteq) \text{ is a pseudosemilattice } \Rightarrow \langle\forall x,y \in A ::  x \sqcap y = y \sqcap x \rangle ,
\mathcal (A,\sqsubseteq) \text{ is a copseudosemilattice } \Rightarrow \langle\forall x,y \in A ::  x \sqcup y = y \sqcup x \rangle .

証明

x,y \in Aを仮定し、任意のa \in Aに対し:

  a \sqsubseteq x \sqcap y
\Leftrightarrow  { \sqcap-definition }
  a \sqsubseteq x \wedge a \sqsubseteq y
\Leftrightarrow  { \wedge-commutativity }
  a \sqsubseteq y \wedge a \sqsubseteq x
\Leftrightarrow  { \sqcap-definition }
  a \sqsubseteq y \sqcap x

supremumに関しても同様。

∎

定理 (consistency)

\mathcal (A,\sqsubseteq) \text{ is a pseudosemilattice } \Rightarrow \langle\forall x,y \in A :: x \sqsubseteq y \equiv  x \sqcap y = x \rangle ,
\mathcal (A,\sqsubseteq) \text{ is a copseudosemilattice } \Rightarrow \langle\forall x,y \in A ::  x \sqsubseteq y \equiv x \sqcup y = y \rangle .

証明

x,y \in Aに対し:

  x \sqcap y = x
\Leftrightarrow  { indirect equality }
  \langle\forall a \in A :: a \sqsubseteq x \sqcap y \equiv a \sqsubseteq x \rangle
\Leftrightarrow  { \sqcap-definition }
  \langle\forall a \in A :: a \sqsubseteq x \wedge a \sqsubseteq y \equiv a \sqsubseteq x \rangle
\Leftrightarrow  { \Rightarrow-definition }
  \langle\forall a \in A : a \sqsubseteq x : a \sqsubseteq y \rangle
\Leftrightarrow  { indirect inequality }
  x \sqsubseteq y

supremumに関しても同様。

∎

参考文献

  • C.J. Aarts, R. C. Backhouse, P. Hoogendijk, T.S. Voermans, and J. van der Woude. A relational theory of datatypes. Unpublished.
  • R.C. Backhouse. Mathematics of Program Construction. Unpublished.
  • R. Bird and O. de Moor. Algebra of Programming. Series in Computer Science. Prentice-Hall, 1997.
  • B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002.
  • V.K. Garg. Introduction to lattice theory with computer science applications. John Wiley & Sons, 2015.
  • D. Gries. Foundations for Calculational Logic. In M. Broy, B. Schieder, eds., Mathematical Methods in Program Development. Springer, 1997.
  • D. Gries and F.B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.
  • S. Rudeanu. Sets and Ordered Structures. Bentham Science Publishers, 2012.
  • J.L.A. van de Snepscheut. On lattice theory and program semantics. Technical Report CS-TR-93-19, Caltech, Pasadena, California, USA, 1993.
  • G. Tourlakis. Lectures in Logic and Set Theory Vol. 1: Mathematical Logic. Cambridge University Press, 2003.
  • G. Tourlakis. Lectures in Logic and Set Theory Vol. 2: Set Theory. Cambridge University Press, 2003.
  • https://ncatlab.org/nlab/show/semilattice