かじもとにっき

自分用メモ

圏論(1)

数学 圏論

定義 (quiver)

\mathcal Oと\mathcal Aを共にclassとする。

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom})\text{ is a quiver } \equivDef \mathrm{cod}\text{ and }\mathrm{dom}\text{ are functions into }\mathcal O\text{ over }\mathcal A\text{.}

また、x,y \in \mathcal Oに対し、

x \leftarrow y \eqDef \{ f \in \mathcal A : \mathrm{cod}.f = x \wedge \mathrm{dom}.f = y \}\text{.}

定義から明らかに、

\langle\cup x,y \in \mathcal O :: x \leftarrow y \rangle = \mathcal A

が成り立つ。

定義 (deductive system)

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a deductive system } \equivDef \\
\,(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom})\text{ is a quiver } \\
\;\wedge \mathrm{id}\text{ is a function over }\mathcal O \\
\;\wedge \langle\forall x \in \mathcal O :: \mathrm{id}_x \in x \leftarrow x \rangle \\
\;\wedge \circ\text{ is a function over }\mathcal O \times \mathcal O \times \mathcal O \\
\;\wedge \langle\forall x,y,z \in \mathcal O :: \circ_{x,y,z}\text{ is a function into }x \leftarrow z\text{ over }(x \leftarrow y) \times (y \leftarrow z) \rangle\text{.}

x,y,zが文脈から明らかな時、f \circ_{x,y,z} gをf \circ gのように省略して書く。

f,g \in \mathcal Aの時、定義から

\langle\forall x,y,z \in \mathcal O : f \in x \leftarrow y \wedge g \in y \leftarrow z : f \circ g \in x \leftarrow z\rangle

だが、これは1-point ruleによって

\mathrm{dom}.f=\mathrm{cod}.g \Rightarrow \mathrm{cod}(f \circ g) = \mathrm{cod}.f \wedge \mathrm{dom}(f \circ g) = \mathrm{dom}.g

と同値。

定義 (category)

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a category } \equivDef \\
\,(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a deductive system } \\
\;\wedge \langle\forall w,x \in \mathcal O, f \in w \leftarrow x :: \mathrm{id}_w \circ_{w,w,x} f = f = f \circ_{w,x,x} \mathrm{id}_x \rangle \\
\;\wedge \langle\forall w,x,y,z \in \mathcal O, f \in w \leftarrow x, g \in x \leftarrow y, h \in y \leftarrow z \\
\quad\quad :: (f \circ_{x,y,z} g) \circ_{x,z,w} h = f \circ_{x,y,w} (g \circ_{y,z,w} h) \rangle\text{.}

定義 (small category, locally small category)

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a small category } \equivDef \\
\,(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a category } \wedge \mathcal O\text{ is a set } \wedge \mathcal A\text{ is a set.}

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a locally small category } \equivDef \\
\,(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a category } \wedge \langle\forall x,y \in \mathcal O :: x \leftarrow y\text{ is a set } \rangle\text{.}

参考文献

  • M. Arbib and E. Manes. Arrows, Structures and Functors — The Categorical Imperative. Academic Press, 1975.
  • S. Awodey. Category Theory. 2d ed. Oxford University Press, 2010.
  • M. Barr and C. Wells. Category Theory for Computing Science. Prentice Hall, 1990.
  • R.C. Backhouse. Mathematics of Program Construction. Unpublished.
  • R. Bird and O. de Moor. Algebra of Programming. Series in Computer Science. Prentice-Hall, 1997.
  • D. Gries. Foundations for Calculational Logic. In M. Broy, B. Schieder, eds., Mathematical Methods in Program Development. Springer, 1997.
  • E.J. Lemmon. Introduction to Axiomatic Set Theory. Routledge & Kegan Paul, 1968.
  • D. Gries and F.B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.
  • S. Mac Lane. Categories for the Working Mathematician. 2d ed. Springer-Verlag, 1998.
  • 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.

constant combinatorとflip

数学

定義 (constant combinator)

集合AとBに対し、関数K_{A,B} \in (A \leftarrow B) \leftarrow Aを

K_{A,B}.a.b = a

で定義する。

定理

(A, \leqA)と(B, \leqB)が共にposetの時、

K_{A,B} \in ( (A, \leqA) \funcM (B, \leqB) ) \funcM (A, \leqA).

証明

a \in Aを固定すると、任意のx,y \in Bに対し:

  K.a.x \leqA K.a.y
\Leftrightarrow  { K-definition }
  a \leqA a
\Leftarrow  { right zero of \Rightarrow }
  x \leqB y.

よってK_{A,B} \in ( (A, \leqA) \funcM (B, \leqB) ) \leftarrow (A, \leqA).
さらに、任意のx,y \in Aに対し:

  K.x \dleqA K.y
\Leftrightarrow  { lifting + K-definition }
  \langle\forall b \in B :: x \leqA y \rangle
\Leftarrow  { \forall-introduction }
  x \leqA y.

よってK_{A,B} \in ( (A, \leqA) \funcM (B, \leqB) ) \funcM (A, \leqA).

∎

定義 (flip)

poset(A,\leqA)と(B,\leqB)と(C,\leqC)に対し、関数\mathrm{flip}_{A,B,C} \in ( (A \leftarrow B) \leftarrow C) \leftarrow ( ( (A,\leqA) \funcM (C,\leqC) ) \funcM (B,\leqB) )を

\mathrm{flip}_{A,B,C}.f.c.b = f.b.c

で定義する。

定理

\mathrm{flip}_{A,B,C} \in ( ( (A,\leqA) \funcM (B,\leqB) ) \funcM (C,\leqC) ) \leftarrow ( ( (A,\leqA) \funcM (C,\leqC) ) \funcM (B,\leqB) ).

証明

f \in ( (A,\leqA) \funcM (C,\leqC) ) \funcM (B,\leqB)とc \in Cを任意に1つずつとる。
任意のx,y \in Bに対し:

  \mathrm{flip}.f.c.x \leqA \mathrm{flip}.f.c.y
\Leftrightarrow  { \mathrm{flip}-definition }
  f.x.c \leqA f.y.c
\Leftarrow  { lifting }
  f.x \dleqA f.y
\Leftarrow { f is monotonic }
  x \leqB y.

また、任意のx,y \in Bに対し:

  \mathrm{flip}.f.x \dleqA \mathrm{flip}.f.y
\Leftrightarrow  { lifting + \mathrm{flip}-definition }
  \langle\forall b \in B :: f.b.x \leqA f.b.y \rangle
\Leftarrow { f.b is monotonic }
  x \leqC y.

∎

定理

\mathrm{flip}\text{ is an order-monomorphism}.

証明

任意のf,g \in ( (A,\leqA) \funcM (C,\leqC) ) \funcM (B,\leqB)に対し:

  \mathrm{flip}.f \ddleqA \mathrm{flip}.g
\Leftrightarrow  { lifting, twice }
  \langle\forall c \in C, b \in B :: \mathrm{flip}.f.c.b \leqA \mathrm{flip}.g.c.b \rangle
\Leftrightarrow  { \mathrm{flip}-definition }
  \langle\forall b \in B, c \in C :: f.b.c \leqA g.b.c \rangle
\Leftrightarrow  { lifting, twice }
  f \ddleqA g.

∎

定理

\mathrm{flip}\text{ is an order-isomorphism}.

証明

\mathrm{flip} \bullet \mathrm{flip} = Iより明らか。 ∎

定理

\mathrm{flip} \bullet K = (K\bullet).

証明

任意のb \in Bとc \in Cに対し:

  \mathrm{flip}.(K_{A \leftarrow B,C}.g).b.c
=  { \mathrm{flip}-definition }
  K_{A \leftarrow B,C}.g.c.b
=  { K-definition }
  g.b
=  { K-definition }
  K_{A,C}.(g.b).c
=  { \bullet-definition }
  (K_{A,C} \bullet g).b.c.

∎

参考文献

  • 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.

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

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

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

infとsup

数学

定義 (infimumとsupremum)

\mathcal Aと\mathcal Bを共にposetとする。
Binary relation \operatorname{\underline{=\sqcap}} \in \mathcal A \sim (\mathcal A \funcM \mathcal B)と\operatorname{\underline{=\sqcup}} \in \mathcal A \sim (\mathcal A \funcM \mathcal B)をそれぞれ

x \operatorname{\underline{=\sqcap}} f \equivDef \langle \forall a \in \mathcal A :: a \sqsubseteq x \equiv K.a \operatorname{\dot\sqsubseteq} f \rangle, 
x \operatorname{\underline{=\sqcup}} f \equivDef \langle \forall a \in \mathcal A :: x \sqsubseteq a \equiv f \operatorname{\dot\sqsubseteq} K.a \rangle
  where K = \langle a :: \langle b :: a \rangle \rangle \in (\mathcal A \leftarrow \mathcal B) \leftarrow \mathcal A

で定義し、x \operatorname{\underline{=\sqcap}} fをx \text{ is the infimum of } f、x \operatorname{\underline{=\sqcup}} fをx \text{ is the supremum of } fと読む。

定理 (infimumとsupremumの一意性)

\operatorname{\underline{=\sqcap}} \text{ and } \operatorname{\underline{=\sqcup}} \text{ are coinjective } .

証明

x \operatorname{\underline{=\sqcap}} f \wedge y \operatorname{\underline{=\sqcap}} fを仮定する。

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

   a \leqA x
\Leftrightarrow  { \operatorname{\underline{=\sqcap}}-definition }
   K.a \dleqA f
\Leftrightarrow  { \operatorname{\underline{=\sqcap}}-definition }
   a \leqA y .

よって、indirect equalityによりx=y。
supremumに関しても同様。

∎

定理 (infimumとsupremumの伝統的定義)

x \in \mathcal A、f \in \mathcal A \funcM \mathcal Bとすると、

x \operatorname{\underline{=\sqcap}} f \equiv K.x \operatorname{\dot\sqsubseteq} f \wedge \langle \forall a \in \mathcal A : K.a \operatorname{\dot\sqsubseteq} f : a \sqsubseteq x \rangle , 
x \operatorname{\underline{=\sqcup}} f \equiv f \operatorname{\dot\sqsubseteq} K.x \wedge \langle \forall a \in \mathcal A : f \operatorname{\dot\sqsubseteq} K.a : x \sqsubseteq a \rangle .

証明

(\Rightarrow):

infimumとsupremumの定義におけるaとしてxを取れば直ちに導かれる。

(\Leftarrow):

任意のa \in Aに対し:

  K.a \operatorname{\dot\sqsubseteq} f
\Leftarrow  { assumption:K.x \operatorname{\dot\sqsubseteq} f + \operatorname{\dot\sqsubseteq}-transitivity }
  K.a \operatorname{\dot\sqsubseteq} K.x
\Leftarrow  { K \text{ is monotonic } }
  a \sqsubseteq x .

supremumに関しても同様。

∎

定義 (completenessとcocompleteness)

\mathcal Aと\mathcal Bを共にposetとする。

\mathcal A \text{ is } \mathcal B \text{-complete } \equivDef \langle \forall f \in \mathcal A \underset{M}{\leftarrow} \mathcal B :: \langle \exists x \in \mathcal A :: x \operatorname{\underline{=\sqcap}} f \rangle \rangle  ,
\mathcal A \text{ is } \mathcal B \text{-cocomplete } \equivDef \langle \forall f \in \mathcal A \underset{M}{\leftarrow} \mathcal B :: \langle \exists x \in \mathcal A :: x \operatorname{\underline{=\sqcup}} f \rangle \rangle  ,
\mathcal A \text{ is complete } \equivDef \langle \forall \mathcal B : \mathcal B \text{ is a poset } : \mathcal A \text{ is } \mathcal B \text{-complete } \rangle  ,
\mathcal A \text{ is cocomplete } \equivDef \langle \forall \mathcal B : \mathcal B \text{ is a poset } : \mathcal A \text{ is } \mathcal B \text{-cocomplete } \rangle  .

定理 (completenessとcocompleteness)

\mathcal Aと\mathcal Bを共にposetとする。

\mathcal A \text{ is } \mathcal B \text{-complete} \equiv \langle \exists \sqcap :: (K, \sqcap) \text{ is a Galois connection between } \mathcal A \funcM \mathcal B \text{ and } \mathcal A \rangle,
\mathcal A \text{ is } \mathcal B \text{-cocomplete} \equiv \langle \exists \sqcup :: (\sqcup, K) \text{ is a Galois connection between } \mathcal A \text{ and } \mathcal A \funcM \mathcal B \rangle.

証明

  \mathcal A \text{ is } \mathcal B \text{-complete}
\Leftrightarrow  { definition }
  \langle \forall f \in \mathcal A \funcM \mathcal B :: \langle \exists x \in \mathcal A :: x \operatorname{\underline{=\sqcap}} f \rangle \rangle
\Leftrightarrow  { axiom of choice }
   \langle \exists \sqcap \in \mathcal A \leftarrow (\mathcal A \funcM \mathcal B) :: \langle \forall f \in \mathcal A \funcM \mathcal B :: \sqcap f \operatorname{\underline{=\sqcap}} f \rangle \rangle
\Leftrightarrow  { \operatorname{\underline{=\sqcap}}-definition }
   \langle \exists \sqcap \in \mathcal A \leftarrow (\mathcal A \funcM \mathcal B) :: \langle \forall f \in \mathcal A \funcM \mathcal B, a \in \mathcal A :: a \leqA \sqcap f \equiv K.a \dleqA f \rangle \rangle
\Leftrightarrow  { definition }
  \langle \exists \sqcap :: (K, \sqcap) \text{ is a Galois connection between } \mathcal A \funcM \mathcal B \text{ and } \mathcal A \rangle .

cocompletenessに関しても同様。

∎

参考文献

  • 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.
  • 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.
  • 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.

Galois connectionのいくつかの同値な定義

数学

以下、(A,\leqA)と(B,\leqB)を共にposetとする。

定義 (Galois connection)

(F,G) \text{ is a Galois connection between } (A,\leqA) \text{ and } (B,\leqB)
  \equivDef F \in A \leftarrow B \wedge G \in B \leftarrow A \wedge \langle \forall x \in B, y \in A :: F.x \leqA y \equiv x \leqB G.y \rangle

定理 (Cancellation)

(F, G) \text{ is a Galois connection between } (A,\leqA) \text{ and } (B,\leqB) \Rightarrow F \bullet G \dleqA I_A \wedge I_B \dleqB G \bullet F

証明

定義内のxとyとしてそれぞれG.yとF.xを取れば直ちに導かれる。∎

定義 (Poset of monotonic functions)

(A,\leqA) \funcM (B,\leqB) \overset{\text{def}}{=} (\{ f \in A \leftarrow B : \langle \forall x,y \in B : x \leqB y : f.x \leqA f.y \rangle : f \}, \dleqA)

定理 (Galois connectionの別の定義)

(F, G) \text{ is a Galois connection between } (A,\leqA) \text{ and } (B,\leqB)
  \equiv F \in (A,\leqA) \funcM (B,\leqB) \wedge G \in (B,\leqB) \funcM (A,\leqA) \wedge F \bullet G \leqA I_A \wedge I_B \leqB G \bullet F

証明

(\Rightarrow):

CancellationによりF \bullet G \dleqA I_AとI_B \dleqB G \bullet Fが成り立つので、後はFとGが共にmonotonicであることを言えば良い。
任意のx,y \in Bに対し:

  F.x \leqA F.y
\Leftrightarrow  { (F, G) \text{ is a Galois connection } }
  x \leqB G(F.y)
\Leftarrow  { cancellation: I_B \dleqB G \bullet F + \leqB-transitivity }
  x \leqB y

同様に、任意のx,y \in Aに対し:

  G.x \leqB G.y
\Leftrightarrow  { (F, G) \text{ is a Galois connection } }
  F(G.x) \leqA y
\Leftarrow  { cancellation: F \bullet G \dleqA I_A + \leqA-transitivity }
  x \leqA y

(\Leftarrow):

任意のx \in Bとy \in Aに対し:

  F.x \leqA y
\Rightarrow  { G \text{ is monotonic} }
  G(F.x) \leqB G.y
\Rightarrow  { cancellation + \leqB-transitivity }
  x \leqB G.y
\Rightarrow  { F \text{ is monotonic} }
  F.x \leqA F(G.y)
\Rightarrow  { cancellation + \leqA-transitivity }
  F.x \leqA y

∎

定理 (Galois connectionの別の定義)

(F, G) \text{ is a Galois connection between } (A,\sqsubseteq) \text{ and } (B,\preceq)
  \equiv F \in (A,\leqA) \funcM (B,\leqB) \wedge G \in B \leftarrow A \wedge F \bullet G \dleqA I_A \wedge \langle \forall x \in B, y \in A : F.x \leqA y : x \leqB G.y \rangle

証明

\text{LHS} \equiv \text{RHS} \wedge \langle \forall x \in B, y \in A : x \leqB G.y : F.x \leqA y \rangleなので、
\text{RHS} \Rightarrow \langle \forall x \in B, y \in A : x \leqB G.y : F.x \leqA y \rangleを示せば良い。

任意のx \in Bとy \in Aに対し:

  x \leqB G.y
\Rightarrow  { assumption: F \text{ is monotonic } }
  F.x \leqA F(G.y)
\Rightarrow  { assumption: F \bullet G \dleqA I_A + \leqA-transitivity }
  F.x \leqA y

∎

補足

RHS*1において、

  F \bullet G \dleqA I_A \wedge \langle \forall x \in B, y \in A : F.x \leqA y : x \leqB G.y \rangle
\Leftrightarrow  { lifting }
  \langle \forall y \in A :: F(G.y) \leqA y \rangle \wedge \langle \forall x \in B, y \in A : F.x \leqA y : x \leqB G.y \rangle
\Leftrightarrow  { (\forall/\wedge)-distributivity }
  \langle \forall y \in A :: F(G.y) \leqA y \wedge \langle \forall x \in B : F.x \leqA y : x \leqB G.y \rangle
\Leftrightarrow  { informally }
  \langle \forall y \in A :: G.y \text{ is the greatest } x \in B \text{ s.t. } F.x \leqA y \rangle

定理 (Galois connectionの別の定義)

(F, G) \text{ is a Galois connection between } (A,\leqA) \text{ and } (B,\leqB)
  \equiv F \in A \leftarrow B \wedge G \in (B,\leqB) \funcM (A,\leqA) \wedge I_B \dleqB G \bullet F \wedge \langle \forall x \in B, y \in A : x \leqB G.y : F.x \leqA y \rangle

証明

先の定理と同様。∎

補足

RHSにおいて、

  I_B \dleqB G \bullet F \wedge \langle \forall x \in B, y \in A : x \leqB G.y : F.x \leqA y  \rangle
\Leftrightarrow  { informally }
  \langle \forall x \in B :: F.x \text{ is the least } y \in A \text{ s.t }  x \leqB G.y \rangle

参考文献

  • 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.
  • 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.

*1:right hand side