かじもとにっき

自分用メモ

semilatticeとcosemilattice

数学

定義 (semilatticeとcosemilattice)

\mathcal A \text{ is a semilattice } \equivDef \mathcal A \text{ is a pseudosemilattice } \wedge \mathcal A \text{ is } \emptyPoset\text{-complete } ,
\mathcal A \text{ is a cosemilattice } \equivDef \mathcal A \text{ is a copseudosemilattice } \wedge \mathcal A \text{ is } \emptyPoset\text{-cocomplete }.

定理 (topとbottom)

\mathcal A\text{ is }\emptyPoset\text{-complete } \equiv \mathcal A \text{ has the greatest element },
\mathcal A\text{ is }\emptyPoset\text{-cocomplete } \equiv \mathcal A \text{ has the least element }.

証明

  \mathcal A\text{ is }\emptyPoset\text{-complete }
\Leftrightarrow  { definition }
  \langle\forall f \in \mathcal A \funcM \emptyPoset :: \langle \exists y \in \mathcal A :: \langle\forall a \in \mathcal A :: K.a \dleqA f \equiv a \leqA y \rangle\rangle\rangle
\Leftrightarrow  { 1-point: f \in \mathcal A \funcM \emptyPoset \equiv f = \emptyset_{\mathcal A \funcM \emptyPoset} }
  \langle \exists y \in \mathcal A :: \langle\forall a \in \mathcal A :: K.a \dleqA \emptyset_{\mathcal A \funcM \emptyPoset} \equiv a \leqA y \rangle\rangle
\Leftrightarrow  { lifting + empty range }
  \langle \exists y \in \mathcal A :: \langle\forall a \in \mathcal A :: a \leqA y \rangle\rangle.

least elementに関しても同様。

∎

\mathcal A\text{ is }\emptyPoset\text{-complete }の時\mathcal Aのgreatest element \sqcap\emptyset_{\mathcal A \funcM \emptyPoset}を\top_{\mathcal A}、\mathcal A\text{ is }\emptyPoset\text{-cocomplete }の時\mathcal Aのleast element \sqcup\emptyset_{\mathcal A \funcM \emptyPoset}を\bot_{\mathcal A}と書き、それぞれtopとbottomと読む。

定理 (identity)

\mathcal A \text{ is a semilattice } \Rightarrow \langle\forall x \in \mathcal A :: x \sqcap \top = x \rangle,
\mathcal A \text{ is a cosemilattice } \Rightarrow \langle\forall x \in \mathcal A :: x \sqcup \bot = x \rangle.

証明

x \in \mathcal Aを仮定すると、任意のa \in \mathcal Aに対し:

  a \leqA x \sqcap \top
\Leftrightarrow  { \sqcap-definition }
  a \leqA x \wedge a \leqA \top
\Leftrightarrow  { \top-definition }
  a \leqA x.

supremumに関しても同様。

∎

定理

\mathcal A\text{ is }\mathcal B\text{-complete } \wedge \mathcal A\text{ is }\emptyPoset\text{-complete } \Rightarrow \sqcap K_{\mathcal A,\mathcal B}.\top_{\mathcal A} = \top_{\mathcal A},
\mathcal A\text{ is }\mathcal B\text{-cocomplete } \wedge \mathcal A\text{ is }\emptyPoset\text{-cocomplete } \Rightarrow \sqcup K_{\mathcal A,\mathcal B}.\bot_{\mathcal A} = \bot_{\mathcal A}.

証明

任意のa \in \mathcal Aに対し:

  a \leqA \sqcap K_{\mathcal A,\mathcal B}.\top
\Leftrightarrow  { \sqcap-definition }
  \langle\forall b \in B :: a \leqA \top \rangle
\Leftrightarrow  { term \mathrm{true} }
  \mathrm{true}
\Leftrightarrow  { \top-definition }
  a \leqA \top.

supremumに関しても同様。

∎

定理 (zero)

\mathcal A\text{ is an }\emptyPoset\text{-cocomplete pseudosemilattice} \Rightarrow \langle\forall x \in \mathcal A :: x \sqcap \bot = \bot \rangle,
\mathcal A\text{ is an }\emptyPoset\text{-complete copseudosemilattice} \Rightarrow \langle\forall x \in \mathcal A :: x \sqcup \top = \top \rangle.

証明

x \in \mathcal Aを仮定すると、任意のa \in \mathcal Aに対し:

  a \leqA x \sqcap \bot
\Leftrightarrow  { \sqcap-definition }
  a \leqA x \wedge a \leqA \bot
\Leftrightarrow  { a \leqA \bot \equiv a = \bot }
  a \leqA \bot.

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.
  • G. Tourlakis. Mathematical Logic. John Wiley & Sons, 2008.
  • https://ncatlab.org/nlab/show/semilattice