bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

写像対象-型定理(続き)

7.8 具体例

指数対象\(A^{B+C} = A^B \times A^C\)は、Haskellの型シグネチャで表すと、
\begin{eqnarray}
Either \ b \ c \rightarrow a \sim (b \rightarrow a, c \rightarrow a)
\end{eqnarray}
となることを前回の記事で説明した。

それでは、この型シグネチャに基づいて具体例を提示することにしよう。

対象\(A,B,C\)をそれぞれ2個の文字の集まり\(\{A,B\}\)、3個の整数の集まり\(\{1,2,3\}\)、ブール値\(\{True,False\}\)としよう。

まず、左辺の
\begin{eqnarray}
Either \ b \ c \rightarrow a
\end{eqnarray}
を実現しよう。これは、\(A\)か\(B\)を入力し、\(C\)を出力する射の集まりを求めているので、次の32個の関数として実現することができる。

f1 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f2 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f3 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f4 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f5 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f6 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f7 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f8 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f9 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f10 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f11 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f12 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f13 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f14 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f15 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f16 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f17 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f18 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f19 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f20 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f21 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f22 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f23 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f24 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f25 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f26 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f27 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f28 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f29 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f30 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f31 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f32 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"

次に、右辺の
\begin{eqnarray}
(b \rightarrow a, c \rightarrow a)
\end{eqnarray}
を実現しよう。

まず、\(b \rightarrow a\)を実現しよう。これは次のようになる。

g1 a
  | a == 'A' = True
  | a == 'B' = True
  | otherwise = error "not assigned"
g2 a
  | a == 'A' = True
  | a == 'B' = False
  | otherwise = error "not assigned"
g3 a
  | a == 'A' = False
  | a == 'B' = True
  | otherwise = error "not assigned"
g4 a
  | a == 'A' = False
  | a == 'B' = False
  | otherwise = error "not assigned"

同様に、\(c \rightarrow a\)を実現すると、次のようになる。

h1 a
  | a == 1 = True
  | a == 2 = True
  | a == 3 = True
  | otherwise = error "not assigned"
h2 a
  | a == 1 = True
  | a == 2 = True
  | a == 3 = False
  | otherwise = error "not assigned"
h3 a
  | a == 1 = True
  | a == 2 = False
  | a == 3 = True
  | otherwise = error "not assigned"
h4 a
  | a == 1 = True
  | a == 2 = False
  | a == 3 = False
  | otherwise = error "not assigned"
h5 a
  | a == 1 = False
  | a == 2 = True
  | a == 3 = True
  | otherwise = error "not assigned"
h6 a
  | a == 1 = False
  | a == 2 = True
  | a == 3 = False
  | otherwise = error "not assigned"
h7 a
  | a == 1 = False
  | a == 2 = False
  | a == 3 = True
  | otherwise = error "not assigned"
h8 a
  | a == 1 = False
  | a == 2 = False
  | a == 3 = False
  | otherwise = error "not assigned"

右辺はこれらのデカルト積となるので、次の32個の関数として実現される。

p1 a b  = ((g1 a), (h1 b)) 
p2 a b  = ((g1 a), (h2 b)) 
p3 a b  = ((g1 a), (h3 b)) 
p4 a b  = ((g1 a), (h4 b)) 
p5 a b  = ((g1 a), (h5 b)) 
p6 a b  = ((g1 a), (h6 b)) 
p7 a b  = ((g1 a), (h7 b)) 
p8 a b  = ((g1 a), (h8 b)) 
p9 a b  = ((g2 a), (h1 b)) 
p10 a b = ((g2 a), (h2 b)) 
p11 a b = ((g2 a), (h3 b)) 
p12 a b = ((g2 a), (h4 b)) 
p13 a b = ((g2 a), (h5 b)) 
p14 a b = ((g2 a), (h6 b)) 
p15 a b = ((g2 a), (h7 b)) 
p16 a b = ((g2 a), (h8 b)) 
p17 a b = ((g3 a), (h1 b)) 
p18 a b = ((g3 a), (h2 b)) 
p19 a b = ((g3 a), (h3 b)) 
p20 a b = ((g3 a), (h4 b)) 
p21 a b = ((g3 a), (h5 b)) 
p22 a b = ((g3 a), (h6 b)) 
p23 a b = ((g3 a), (h7 b)) 
p24 a b = ((g3 a), (h8 b)) 
p25 a b = ((g4 a), (h1 b)) 
p26 a b = ((g4 a), (h2 b)) 
p27 a b = ((g4 a), (h3 b)) 
p28 a b = ((g4 a), (h4 b)) 
p29 a b = ((g4 a), (h5 b)) 
p30 a b = ((g4 a), (h6 b)) 
p31 a b = ((g4 a), (h7 b)) 
p32 a b = ((g4 a), (h8 b)) 

このように、左辺、右辺ともに32個の関数で実現され、これらの関数は1対1に対応させることができ、同型写像(Isomorphism)であることが分かる。

少しだけ、実行してみよう。

*Main> f27 (Left 'A')
False
*Main> f27 (Right 1)
True
*Main> p27 'A' 1
(False,True)