viercc @monoid_patchwork@fedibird.com

https://arxiv.org/pdf/1308.6548.pdf

http://pantodon.jp/index.rb?body=sheaf#cite.0@1308.6548

一月も今日で終わりか

https://gist.github.com/viercc/5b79efc5c3593a1b487a51f04c2bffca

Distributivityは(2)から(1)が導ける、OK!

では余剰な法則は無いのか？
Zip単独、Align単独の法則は余剰なものは無いだろう。

Absorption lawを入れるならばべき等律は省けるかもしれない（が、Zip/Align単独でも使えるようにしたいため、省略はしないでよいだろう）

Distributivityは、束論としてはどちらか片方のみでよいはずだが…

... これらの等式はE xがそれぞれE 1のある部分集合と見做せて、inclusionがその部分集合の包含写像と見做せると言える。

これがZip/Align則の"想定している"振る舞いなので、Zip/Align則はこれで完全であると言っても良い！

mention送りまくってしまいました申し訳ありません
QT: https://fedibird.com/@monoid_patchwork/109767373737263013 [参照]

ここでtoTheseは同型

toThese :: (Maybe a, Maybe b) -> Maybe (These a b)

法則を使えばinclusion, subsetについて以下の等式が得られる。

inclusion . inclusion = inclusion
inclusion @X @X = id

subset <=< subset = subset
subset @X @X = Just

subset @X @y . include @y @X = Just

inclusion @(x∨y) @X . inclusion @X @(x ∧ y) = inclusion @(x∨y) @y . inclusion @y @(x ∧ y)

Fを多項式Functorとする。

F a = Σ_{x ∈ M} (E x -> a)

F aの要素は(x :: M, f :: E x -> a)と書く。

FがZip (+Align)でもあるとき、それらの法則から

- Mは(Bounded) Distributive Lattice (0,1,∨,∧,≤)
- E(0) ~ Void

であって、2つの関数

inclusion :: (x ≤ y) => E x -> E y
subset :: (x ≤ y) => E y -> Maybe (E x)

から

zip (x,f) (y,g) = (x ∧ y, \i -> (f (inclusion i), g (inclusion i)))
Just <$> align (x,f) (y,g) = (x ∨ y, \i -> toThese (f <$> subset i, g <$> subset i))

とzip, alignが定義される

Distributivity'1

align (zip xs ys) zs ≡ undistrThesePair <$> zip (align xs zs) (align ys zs)

これもxs, ysの要素だけ見ることができて、

expand :: forall a b. f a -> f b -> f (Maybe a)
expand as bs = justHere <$> align as bs

を使って

expand (zip xs ys) zs ≡ zipWith zip (expand xs zs) (expand ys zs)

Distributivity'2

distrPairThese <$> zip (align xs ys) zs ≡ align (zip xs zs) (zip ys zs)

これはxs, ysの要素だけ見たほうがよくて、

restrict :: forall a b. f a -> f b -> f a
restrict = zipWith const

を使って

restrict (align xs ys) zs ≡ align (restrict xs zs) (restrict ys zs)

Distributivity'3は不要、なぜなら
undistrPairThese . distrPairThese = id
なので、'2から直ちに導かれるから。

Zip(+Align)はDistributive Latticeが望ましい性質なんですねぇ！

出来た
やったぁぁ！！！！

（Distributivity'1-'3より少し弱いバージョンで十分そうではある）

Distributivityがあれば、大体うまく行ってそうな雰囲気だな

それとも、こう考えればいいのか？
Q False :: [a1][a2]
Q True :: [ b1 ][b2]
という部分関数をzipしている

このStranzに"普通"にRepeat, Semialign, Alignのインスタンスを定義すると、Distributivity以外は満たす

いや、Distributivityからどうにかできるか・・・？