前回の記事 リストデータ型にのるモナド構造の単位射は a -> [a] だけ (1) の続きです。
本記事内で出てくる「性質2」「性質3」は前回の記事を参照してください。
複製ユニットモナドの性質(4) (r,n,...n)のn個形の join
前回の性質2と3のときは n * n形と r * n 形と綺麗な形の join を考察しましたが今度は (r,n,...n)のn個形というちょっとややっこしい形の join を考察します。
また 3複製ユニットモナドの具体的な例で考えましょう。
xs1 = [[1,1,1], [], []] -- (3,0,0)形
xs2 = [[0,0,0], [2,2,2], [0,0,0]] -- 3 * 3形
xs3 = [[0,0,0], [0,0,0], [3,3,3]] -- 3 * 3形
ys1 = join xs1 -- 長さ r
zs = [xs1, xs2, xs3]
{- = [
[[1,1,1], [], []],
[[0,0,0], [2,2,2], [0,0,0]],
[[0,0,0], [0,0,0], [3,3,3]]]
-}
として zs での join のモナド則
join (join zs) = join (map join zs)
を観察しましょう。
左辺 = join (join zs)
{- zs は 3 * 3形なので性質2より対角線要素を集めて -}
= join [[1,1,1], [2,2,2], [3,3,3]]
{- 3 * 3形なので性質2より対角線要素を集めて -}
= [1,2,3]
右辺 = join (map join zs)
= join [join xs1, join xs2, join xs3]
{- xs2 と xs3 については 3*3形なので性質2より対角線要素を集めて -}
= join [ys1, [0,2,0], [0,0,3]]
つまり
join [ys1, [0,2,0], [0,0,3]] = [1,2,3]
右辺の
1番目の要素 1 は左辺の ys1 の中から出てきて、
2番目の要素 2 は左辺の [0,2,0] の 2番目の要素が出てきて、
3番目の要素 3 は左辺の [0,0,3] の 3番目の要素が出てきて
いることがわかります。
また、右辺の 1番目の要素 1 が左辺の ys1 の中から出てくるためには ys1 が空リストであっては無理なので ys1 は空リストではない、つまり ys1 の長さ r は 0 でないということもわかります。
例えば ys1 の長さr が 2 だったとしましょう。
(2,3,3)形の join は
join [
[x11, x12],
[x21, x22, x23],
[x31, x32, x33]] = [x11かx12のどれか, x22, x33]
ということになります。
今は n = 3 で考えましたが一般の n で
zs = [
[[1,1..1], [], [], ..., []],
[[0,0..0], [2,2..2], [0,0..0], ... [0,0..0]],
[[0,0..0], [0,0..0], [3,3..3], ... [0,0..0]],
...
[[0,0..0], [0,0..0], ... [0,0..0], [n,n..n]]]
に対して上で書いたのと同様の考察をすると
性質4
r > 0 であり、
(r,n,...n) のn個形のリストの join は
join [
[x11, x21, ... x1r],
[x21, x22, x23, ... x2n],
[x31, x32, x33, ... x3n],
...
[xn1, xn2, xn3, ... xnn]] = [x11か...x1rのどれか, x22, x33, ... xnn]
{- 別の書き方だと -}
join xss = xss!0 の要素のうちのどれか : [xss!i!i | i <- [1..n-1]]
n も r も有限としての書き方をしていますが、n = ∞ や r = ∞ であったときでも成り立ちます。
複製ユニットモナドの性質(5) r = 1 と 1 * n形の join
さらにややっこしくなってきますがこのステップでゴールに一気に近づきます。
また3複製ユニットモナドの具体的な例で考察します。
今までどおり (3,0,0)形を join した結果のリストの長さを r で表します。
仮にr = 2 だったとして話を進めます。
xs1 = map return [1,2] = [[1,1,1], [2,2,2]] -- n(=3) * r(=2)形
xs2 = [[0,0], [-2,-2], [0,0]] -- r(=2) * n(=3)形
xs3 = [[0,0], [0,0], [-3,-3]] -- r(=2) * n(=3)形
ys1 = join xs1 = join (map return [1,2])
{- map return のモナド則より -}
= [1,2]
ys2 = join xs2
{- xs2 は r * n形なので性質3より最初の要素をとって -}
= [0,0]
ys3 = join xs3
{- xs3 は r * n形なので性質3より最初の要素をとって -}
= [0,0]
zs = [xs1, xs2, xs3]
{- = [
[[1,1,1], [2,2,2]],
[[0,0], [-2,-2], [0,0]],
[[0,0], [0,0], [-3,-3]]
-}
とします。
xs1 の長さは r である 2、 xs2 の長さは n である 3、 xs3 の長さは n である 3 なので zs は (r,n,n) である (2,3,3)形をしていることを覚えておきましょう。性質4が使える形です。
zs での join のモナド則
join (join zs) = join (map join zs)
を観察しましょう。
左辺 = join (join zs)
{- zs は (2,3,3)形なので性質4より -}
= join [[1,1,1] か [2,2,2] のどれか, [-2,-2], [-3,-3]]
右辺 = join (map join zs)
= join [join xs1, join xs2, join xs3]
= join [ys1, ys2, ys3]
{- ys1, ys2, ys3 は上ですでに具体的な値として求まっているので -}
= join [[1,2], [0,0], [0,0]]
{- 2 * 3形をしているので性質3より最初の要素を取って -}
= [1,2]
つまり
join [[1,1,1] か [2,2,2] のどれか, [-2,-2], [-3,-3]] = [1,2]
ということになります。
「[1,1,1] か [2,2,2] のどれか」が [1,1,1] の方だったとして考察を進めましょう。つまり
join [[1,1,1], [-2,-2], [-3,-3]] = [1,2]
左辺には 2 が現れないのに右辺には 2 が現れています。こういうことは起こりえません。
今度は「[1,1,1] か [2,2,2] のどれか」が [2,2,2] の方だったとすると
join [[2,2,2], [-2,-2], [-3,-3]] = [1,2]
となり今度は左辺には 1 が現れないのに右辺には 1 が現れています。これも起こりえません。
最初に r = 2 を仮定したうえでの矛盾ですから r = 2 はありえないということになります。
一般の r について同様に join のモナド則を考察すると、
join [[1,1,1] か [2,2,2] か ... か [r,r,r] のどれか, [-2,...-2], [-3,...-3]] = [1,2,..r]
が導かれます。
r > 1 のときは左辺に 1 から r までのすべて数が同時に現れることはできません。
また性質4から r > 0 でしたから、左辺と右辺のつじつまが合う可能性があるのは残る r = 1 のときだけです。このとき
join [[1,1,1], [-2], [-3]] = [1]
ですから、これなら左辺の3つの 1 のうちのどれかが右辺に現れたと考えれば盾は起きません。
つまり
3複製ユニットモナドの join に (3,0,0)形を適用した結果のリストの長さは 1 しかありえない
ということがわかります。
n = 3 の例で考えましたが一般の n に対して
xs1 = map return [1,2...r] -- n * r形
xs2 = [[0,...0], [-2,...-2], [0,...0], ... [0,...0]] -- r * n形
xs3 = [[0,...0], [0,...0], [-3,...-3], ... [0,...0]] -- r * n形
...
xsn = [[0,...0], [0,...0], [0,...0], ... [-n,...-n]] -- r * n形
zs = [xs1, xs2, xs3,... xsn]
として zs に対する join のモナド則を上と同じに考えると
n複製ユニットモナドの join に (n,0,...0)のn個形を適用した結果のリストの長さは 1 しかありえない。
ということがわかります。
r = 1 ということがわかったのでこれを性質3に当てはめると
性質5
1 * n形の join は
join [[x1], [x2], ... [xn]] = [x1]
ここまできたらゴールはもう少しです。
次の記事 リストデータ型にのるモナド構造の単位射は a -> [a] だけ (3) に続きます。
May Monad be with you