かじもとにっき

自分用メモ

parameterized infimumとparameterized supremum

数学

定理 (parameterized infimumとparameterized supremum)

\mathcal Aと\mathcal Bと\mathcal Cを全てposetとする。

\mathcal A\text{ is }\mathcal B\text{-complete } \Rightarrow \mathcal A \funcM \mathcal C\text{ is }\mathcal B\text{-complete },
\mathcal A\text{ is }\mathcal B\text{-cocomplete } \Rightarrow \mathcal A \funcM \mathcal C\text{ is }\mathcal B\text{-cocomplete }.

\mathcal A \operatorname{\underset{M}{\leftarrow}} \mathcal Bに対するinfimum operatorを\sqcapと書くとき、(\mathcal A \funcM \mathcal C) \funcM \mathcal Bに対するinfimum operatorを\dot\sqcapと書く。
また、\mathcal A \operatorname{\underset{M}{\leftarrow}} \mathcal Bに対するsupremum operatorを\sqcupと書くとき、(\mathcal A \funcM \mathcal C) \funcM \mathcal Bに対するsupremum operatorを\dot\sqcupと書く。

証明

任意のf \in \mathcal A \funcM \mathcal Cと\otimes \in (\mathcal A \funcM \mathcal C) \funcM \mathcal Bに対し:

  K.f \ddleqA \otimes
\Leftrightarrow  { lifting, twice }
  \langle\forall b \in \mathcal B, c \in \mathcal C :: f.c \leqA b \otimes c \rangle
\Leftrightarrow  { \mathrm{flip}-definition }
  \langle\forall b \in \mathcal B, c \in \mathcal C :: f.c \leqA \mathrm{flip}.\otimes.c.b \rangle
\Leftrightarrow  { lifting, twice }
  K \bullet f \ddleqA \mathrm{flip}.\otimes
\Leftrightarrow  { (K\bullet,\sqcap\bullet) is a Galois connection + \mathrm{flip}.\otimes \in (\mathcal A \funcM \mathcal B) \funcM \mathcal C }
  f \dleqA \sqcap \bullet \mathrm{flip}.\otimes
\Leftrightarrow  { ● \dot\sqcap = (\sqcap\bullet)\bullet\mathrm{flip} }
  f \dleqA \dot\sqcap \otimes.

supremumに関しても同様。

∎

また、\otimes,\oplus \in (\mathcal A \funcM \mathcal C) \funcM \mathcal Bとすれば、\dot\sqcap = (\sqcap\bullet)\bullet\mathrm{flip}並びに\dot\sqcup = (\sqcup\bullet)\bullet\mathrm{flip}より、

\langle\dot\sqcap b :: \langle c :: b \otimes c \rangle\rangle = \langle c :: \langle \sqcap b :: b \otimes c \rangle\rangle,
\langle\dot\sqcup b :: \langle c :: b \oplus c \rangle\rangle = \langle c :: \langle \sqcup b :: b \oplus c \rangle\rangle.

定理 (distributivity)

\mathcal A\text{ is a }\mathcal C\text{-complete pseudosemilattice} \Rightarrow \langle\forall f, g \in \mathcal A \funcM \mathcal C :: \sqcap(f \operatorname{\dot\sqcap}g) = (\sqcap f) \operatorname\sqcap (\sqcap g) \rangle,
\mathcal A\text{ is a }\mathcal C\text{-cocomplete copseudosemilattice} \Rightarrow \langle\forall f, g \in \mathcal A \funcM \mathcal C :: \sqcup(f \operatorname{\dot\sqcup}g) = (\sqcup f) \operatorname\sqcup (\sqcup g) \rangle.

証明

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

  a \leqA \sqcap(f \operatorname{\dot\sqcap}g)
\Leftrightarrow  { \sqcap-definition }
  \langle\forall c \in \mathcal C :: a \leqA (f \operatorname{\dot\sqcap}g).c \rangle
\Leftrightarrow  { \dot\sqcap-definition }
  \langle\forall c \in \mathcal C :: a \leqA f.c \operatorname{\sqcap} g.c \rangle
\Leftrightarrow  { \sqcap-definition }
  \langle\forall c \in \mathcal C :: a \leqA f.c \wedge a \leqA g.c \rangle
\Leftrightarrow  { (\forall/\wedge)-distributivity }
  \langle\forall c \in \mathcal C :: a \leqA f.c \rangle \wedge \langle\forall c \in \mathcal C :: a \leqA g.c \rangle
\Leftrightarrow  { \sqcap-definition, twice }
  a \leqA \sqcap f \wedge a \leqA \sqcap g
\Leftrightarrow  { \sqcap-definition }
  a \leqA (\sqcap f) \operatorname\sqcap (\sqcap g).

supremumに関しても同様。

∎

特に\mathcal C \neq \boldsymbol\emptysetの時、idempotencyにより、

\langle\forall a \in A, f \in \mathcal A \funcM \mathcal C ::  a \operatorname\sqcap (\sqcap f) = \sqcap(K.a \operatorname{\dot\sqcap} f) \rangle,
\langle\forall a \in A, f \in \mathcal A \funcM \mathcal C ::  a \operatorname\sqcup (\sqcup f) = \sqcup(K.a \operatorname{\dot\sqcup} f) \rangle.

参考文献

  • 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