Adámekの不動点定理を比較的わかりやすく解説してみる

nLabの記事(terminal coalgebra for an endofunctor in nLab)を読んでいたら、図式は読みづらいし行間は広いしで、読解にだいぶ時間を使った。せっかくなので、quiver(図式を簡単に描けるアプリケーション)の練習と埋め込み機能のテストを兼ねて1、大部分を参考にしながら自分なりにまとめ直すことにした。 自分用のメモみたいなもんなので、あんまりクオリティとか正確性に自信はない…… nLabの方ではterminal coalgebraについての定理だが、こっちではinitial algebraのバージョンについて書く。 Adámekの不動点定理 initial object \( 0 \) を持つ圏 \( C \)と、その上の自己関手 \( F \) を考える。\( F \) はcolimitを保つとし、以下のchainがcolimit \( T \) を持つとする。 このとき、射 \( \theta \colon FT \to T \) が存在して、\( (T, \theta) \) はinitial algebraとなる。 証明 まず、\( T \) がcolimitであったから、次のようなcoconeがとれる。 このcocone全体を \( F \) で送って \( 0 \) からの射を左下にくっつけると、次のようになる。 すると、\( F \) がcolimitを保つという条件から、このcoconeもchainのcolimitを与える。colimitの一意性より \( FT \cong T \) となるから、この同型射を \( \theta \colon FT \to T \) とする。...

11月 12, 2023 · 1 分 · zer0-star

高速ゼータ変換について学んだのでお気持ちを書く

一生懸命書いたつもりですが、嘘が書いてあるかもしれませんし、カスみたいなことを書いているかもしれません。すみません(保身) 競プロにおける一般的な高速ゼータ変換 競プロにおいて、“ゼータ変換"や"メビウス変換"という用語は以下の意味で使われることが多いようです。 有限集合 \(X\)、(可換)半群 \(G\) を考える。 関数 \(f : 2^X \to G\), \(g : 2^X \to G\) が次の\((1)\)式または\((2)\)式を満たすとき、\(f\) から \(g\) を求めることをゼータ変換、\(g\) から \(f\) を求めることをメビウス変換と呼ぶ。 \begin{align} g(S) &= \sum_{T \subseteq S} f(T) \\ g(S) &= \sum_{T \supseteq S} f(T) \end{align} このゼータ変換やメビウス変換を\(N\)次元累積和の手法を用いて高速化したのが、高速ゼータ変換や高速メビウス変換です。集合 \( X \) を \( |X| \) 次元の \( 2 \times 2 \times \dots \times 2 \) 格子とみなして、各次元ごとに累積和をとることでゼータ変換が成立するというのがこのアルゴリズムのキモなのです。(アルゴリズムの詳細には立ち入らないので、気になる方は記事末尾のリンクを参考にしてください) 本当は、ゼータ変換は集合の包含関係に限定されない一般的なかたちで定義されるものなのですが、そういった一般のゼータ変換に対して、高速化できるとは限りません。 畳み込み ゼータ変換とある種の畳み込みには深い関係があります。(適切なゼータ変換を持ってきたとき、)関数 \( f \), \( g \) の畳み込みを \( h \) 、\( f \), \( g \), \( h \) のゼータ変換をそれぞれ \( \hat{f} \), \( \hat{g} \), \( \hat{h} \) とおくと、\( \hat{h} = \hat{f} * \hat{g} \) が成立するのです1(ただし、\(*\)は各点積)。よって、畳み込みの種類によっては、ゼータ変換 → 各点積 → メビウス変換 という手順によって畳み込みを高速化できることがあります。...

3月 4, 2022 · 2 分 · zer0-star

First-Class Patterns を自作言語に導入したい話

Ramune という言語を作ろうとしているんですが、そこに First-Class Patterns を導入することを妄想しているので、それについて書きます まだ妄想でしかないので、よく分からないようなことを口走っていると思います(すみません!) First-Class Patterns については、こういうの(slideshare)とかこういうの(hackage)とか見るといいかもしれない first-class patterns の入った言語作りてー — zer0-star (@0x_zer0star) February 19, 2021 こんな気の抜けたことも言っています(アホなので) Pattern as Function 要は、パターンというのは関数a -> Maybe bとみなせて、関数を適用してJustならマッチ成功、Nothingなら失敗とすればパターンマッチが実現できますよね、ということ 先ほど挙げた hackage のやつでは、マッチした結果を右辺の関数に渡すことで束縛の代用とされているが、Ramune では First-Class Patterns をネイティブにサポートして、レコード型(Haskell のようにデータ型の一部ではなく、PureScript のように単体で存在するもの)を介して識別子を束縛したい({ x :: Int }が返ってきたらxがInt型の値に束縛されるように) パターンの型は Haskell 風に書くとnewtype Pattern a r = Pattern { runPattern :: a -> Maybe r }(rはレコード型)と定義できる。例えば、座標平面上の点を受け取ってx座標をxに、y座標をyに束縛するパターンpointは、疑似 Haskell でpoint = Pattern $ \(x, y) -> Just { x = x, y = y }と書ける。このときpointはPattern (a, b) { x :: a, y :: b }というような型を持つ値になるだろう。...

8月 26, 2021 · 3 分 · zer0-star

くBC012 参戦記

開始20秒くらい HackerRank がバグってて焦った A問題 呼ばれて返事をしている臓器ってなーんだ? 返事といえば「はい」で、肺なのではい B問題 一流のものさしってなーんだ? 普通に難しくない?F より難しい気がしなくもない。“ものさし 類語” でググり、“メジャー” を得た。そういえば「メジャー」には「一流」という意味もあった気がするので、めじゃー C問題 どちらか一方を選ぶ首都ってなーんだ? めちゃくちゃ難しかった。Wikipedia の首都の一覧のページを眺めたが、全然わからず。答はもしくわ(モスクワ、もしくは)らしい D問題 気体でありすぎている神の使いってなーんだ? これも難しかったが、良問だと思う(答がわかったときにとても興奮した)。 Wikipedia の神使のページを眺めていたら、“八咫烏” というワードを発見した。なんとなく言葉の響きが “ガス” に似ていたのでちょっと考えてみたところ、“やたがらす” は “やたらがす” (やたらガス)に並び替えられることに気付いた。あまりにも焦ってしまい答の入力に手間取った。答はやたらがす E問題 狭いけど凄い人ってなーんだ? これは本当に難しい。なろう系関連のワードを入れてみてもだめそうだったので、“狭い 類語” “凄い 類語” などでググっていた。最終的には “狭い 英語” でググりだし、このページにたどり着く。下の方に以下の記述があるのを発見: tight 「ピンと張っている」 「しっかり固定されている」 という意味合いですが、 スラングとして cool と同様、 「すごくかっこいい」 といった意味合いで用いられます。 また、tight には 「ケチ(財布のヒモがきつい)野郎」 という意味もあります。 終了まで1分くらいだったこともあり、めちゃくちゃ焦っていたため「tight……『狭い』『凄い』の2つの意味があるな、これだ!!!」と思い提出して AC を得たのだが、冷静に考えてくそなぞなぞコンテストに英語に2つの意味があるやつを出題するはずがないし、運が良かったと言わざるを得ない。実際の答は tight と泰斗(凄い人という意味らしい)とをかけてたいとらしい(泰斗という言葉は知らなかった) F問題 晩ごはんを心待ちにする軍隊ってなーんだ? これは結構簡単だったと思う(他の問題に比べれば)(あと良問だったとも思う(D くらいだったら))。とりあえず「晩ごはん」→「夕餉」の言い換えはすぐにできて、Google Chrome の検索バーに “軍隊 ゆうげ” と入力したところ “軍隊 遊撃” とサジェストされるので、「遊撃隊」という言葉を思いつく。これは「夕餉期待」とも解釈でき、答はゆうげきたい 全体 全体的に難易度が崩壊していた回だったと思う(正答率が A B F D C E の順であったことを考えるとコンテストそのものの難易度調整も失敗していそう)。とはいえ良問もあってとても楽しいコンテストでした...

2月 12, 2021 · 1 分 · zer0-star