かじもとにっき

自分用メモ

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.