月報 2020/09

Tue Sep 01 2020 call/cc の型と排中律

\(\def\rewrite{\color{blue}{\iff}}\)

call/cc の概要

Scheme には call/cc (call-with-current-continuaion; 現在継続) というプリミティブな手続きがある. Lisp は計算モデルを最小で構成する理論から生まれ Scheme はその流れを汲んだ由緒正しいプログラミング言語だが, call/cc に関しては理論ありきではなく, その真逆で, 実装できたから実装したという言語機能だという.

call/cc は関数に対しての return だと言える. return という文はすごくて, 大域脱出をしつつ値を返すというすごい機能をサポートしている.

何ともつかない擬似言語で書くと return というのは次のようなものだろう.

function f() {
    do1();
    return 42;
    do2();
}

これは関数 f を定義している. f を呼び出すとこれはおそらく do1 という手続きを実行し, そして 42 を返して即座に終了する. すなわち, 後続する do2 という手続きは実行 されない . すなわち return はその一行でだけの効果ではなくて, それに続く後ろをスキップするという信じられない効果を持っている. これを 大域脱出 という. for 文に対する break も同じような効果を持っている. return は関数の中ならどこでも呼ぶことが出来て, for 文の中からでも脱出することが出来る.

function f() {
    do1();
    for (var i = 0; i < 10; ++i) {
        return i;
    }
    do2();
}

この return はたぶん i=0 の時点で return 0 を実行するから, i=1 以降は実行すらされない. すごい.

また break との違いとして, 値を返す効果も持っている. return x とすると, f の値が x になる.

call/cc はこの return という手続き自体を値としてプリミティブに扱うことのできる機能である. Scheme には return というキーワード自体が無いわけだが, 次のようなことができる.

(define (f)
  (call/cc (lambda (return)
    (print 'do1)
    (return 42)
    (print 'do2)
    )))

この手続き f を呼び出すと do1 を表示したら 42 を f の値として返して即座に終了する. ここでこの return というのはいわゆる return 的な操作をする手続きが入った変数であり, 親しみのために return という名前をつけているだけで何でもいい.

ここで return はユーザーが定義した手続きと同様に使えるので, その値をそのまま他の式に渡せる. 例えば次は 2 * (return 42) みたいなことをしている.

(define (f)
  (call/cc (lambda (return)
    (print 'do1)
    (*
      2
      (return 42))
    (print 'do2)
    )))

この f を呼ぶと何が返ってくるのかというと 2 * 42 ではなく, 42 そのものが返ってくる. return は式の中の部分であっても間違いなく大域脱出をしてくれる.

call/cc の型

実際には Scheme は動的型付けなので何でもいいんだけど, （静的に）型を与えることを考える.

仮に x の型を T とする. return は T を受け取る. 返り値は無いし return の値自体が使われるこはない. これは先程 (* 2 (return 42)) と書いたときに (* 2 ...) 部分が実行されなかったことから分かる通り.

仮に何も無いことを表す型を Nothing と書く. 例えば Scala だとずばり Nothing という型がある. 型理論だと \(\bot\) と書いたほうが馴染みがあるかもしれない.

多くの言語にある Null とは全く別物なので注意. Null は null とか nil という値を取得することが出来る. 一方で Nothing は値を持つことが出来ない.

return : T -> Nothing

次に call/cc の第一引数 (lambda (return) ...) の型だが ... が分からないので仮にここを ? にすると

(lambda (return) ...) : (T -> Nothing) -> ?

となる. 最後にこれらを組み合わせて call/cc の型が付く. call/cc の最後の値は (return x) していれば x なので,

call/cc : ((T -> Nothing) -> ?) -> T

さて ? だが, これは ... の中で return を使わない場合を考えると自然に決まる.

(call/cc (lambda (return)
  42))

このような場合は call/cc 全体の値は 42 になるのが自然でそのためには (lambda (return) 42) の値が 42 である必要がある. 従って, ? には x の型が入るべきで

call/cc : ((T -> Nothing) -> T) -> T

となる.

カリーハワード対応

ご存知のように（純粋関数言語の）プログラムの型は論理式に対応する. 特に Nothing という型は矛盾を表す命題 \(\bot\) に対応して

論理式 call/cc :

\[((T \implies \bot) \implies T) \implies T\]

を得る.

また NOT 演算 \(\lnot T \iff (T \implies \bot)\) を使うと call/cc は

\[(\lnot T \implies T) \implies T\]

とすっきり書ける.

排中律との対比

白状すればこの議論は直観論理もしくは古典論理で行っている. このどちらでも次の2つは成立する.

• 含意の展開
  • \((X \implies Y) \rewrite \lnot X \lor Y\)
• ド・モルガン
  • \(\lnot (X \lor Y) \rewrite \lnot X \land \lnot Y\)

命題の中における \(\iff\) と区別してよりメタな意味での書き換えを表すのに \(\rewrite\) を使ってみる. 単に読みやすさのために.

これらを使うと,

\[\begin{align*} \mathrm{call/cc} & ~~ \colon ~ (\lnot T \implies T) \implies T \\ & \rewrite \lnot (\lnot T \implies T) \lor T \\ & \rewrite \lnot (\lnot \lnot T \lor T) \lor T \\ & \rewrite (\lnot \lnot \lnot T \land \lnot T) \lor T \\ \end{align*}\]

古典論理なら二重否定除去 \(\lnot \lnot T \rewrite T\) を使って即座に \(\mathrm{call/cc} \rewrite \lnot T \lor T\) を得る. 直観論理では二重否定除去は使えないが, \(\lnot \lnot \lnot T \land \lnot T \iff \lnot T\) が, というかもっと一般に, \(\lnot \lnot X \land X \iff X\) が言えるので, やはり \(\lnot T \lor T\) を得る.

以上から call/cc の型はカリーハワード対応によって排中律に対応していることが分かった.

補足: \(\lnot \lnot X \land X \iff X\)

直観論理の体系でこれを確認する.

\(\implies\) は自明で \(\land\) の右を取ればよい. \(\impliedby\) を確認する.

\(X \implies X\) と \(X \implies \lnot \lnot X\) が同時に成り立てば, これらを組み合わせて \(X \implies \lnot \lnot X \land X\) を得る. 1つ目は自明なので \(X \implies \lnot \lnot X\) を証明すればよい.

\(\lnot\) の糖衣構文を展開すると,

\[\begin{align*} & X \implies \lnot \lnot X \\ \rewrite & X \implies \lnot X \implies \bot \\ \rewrite & X \implies (X \implies \bot) \implies \bot & \text{ 三段論法}\\ \rewrite & X \land (X \implies \bot) \implies \bot \\ \rewrite & \bot \implies \bot \\ \rewrite & \top \\ \end{align*}\]

と確認できた.

以上より \(\lnot \lnot X \land X \iff X\) である.

涼宮ハルヒの直観楽しみ～2020

Wed Sep 09 2020 遅延セグメントツリーを学んだ

2020 年になってようやく遅延（伝播）セグメントツリーを知ったので解ける問題が増えて今嬉しい.

遅延セグメントツリーは一言で言えばこのようなもの. モノイド \(X\) と, それに対するモノイド作用 \(M\) があるときにこんなことが出来る. \(X\) の要素からなる長さ \(N\) の数列 \(x\) について,

1. 任意の添字区間 \(I\) に対して \(\prod_{i \in I} x_i\) を \(O(\log N)\) 程度で計算する
2. 任意の添字区間 \(I\) と（左）作用 \(m \in M\) について \(x_i \leftarrow m(x) ~(i \in I)\) という更新を \(O(\log N)\) 程度で行う

という2つの計算をサポートする. 特に2つ目の更新は区間に対して行えるのがただのセグメントツリーとの違い.

• プロコン用ライブラリ:
  • procon/seq.lazy_segment_tree

私が書いたライブラリは一般にモノイド作用つきモノイドについて定義できるようになっているので, 今の説明で言うところの \(X\) と \(M\) だけ問題に合わせたものを定義すればいつの間にか完成する.

• ちゃんとした説明:
  • aiura/monoidic-act-and-lazy-segment-tree

Range Maximum (Minimum) Query

整数の列 \(x\) について

• 区間取得: \(\sum_{i \in I} x_i\)
• 区間更新: \(x_i \leftarrow z\)

というタイプの問題を考える. 更新は区間と代入する値 \(z\) を決めたらその区間の中の値を \(z\) で上書きしてしまうタイプ.

まず \(X\) とその積は区間取得の方法をそのまま実装するだけ. 更新というのが作用に相当する. 作用の積は少し非自明だけど, 作用の合成を注意深く追えばいい.

• \(X = \mathbb Z\)
  • 積
    • \(x_1 \times x_2 := x_1 + x_2\)
  • 単位元
    • \(0 \times x = x \times 0 = x\)
• \(M = \mathbb Z + 1\)
  • 積
    • \(\ast \times n = n\)
    • \(m \times n = m\) (if \(m \ne \ast\) )
  • 単位元
    • \(\ast \times m = m \times \ast = m\)

ここで \(M\) は左作用として定義している. また \(\mathbb Z + 1\) は整数集合と単集合 \(\{ \ast \}\) との直和のこと.

\(M\) の \(X\) に対する作用は \(m \in M, x \in X\) について

• \(\ast(x) = x\)
• \(m(x) = m\) (if \(m \ne \ast\) )

この作用が数列の値の上書きを意味している. 特に \(\ast \in M\) は何も上書きしないということを表していて, 単位元としての役割を与えている. \(M\) の積だが, \(m(n(x)) = (m \times n)(x)\) を満たすような \(m \times n\) が定義できていれば正しい. 今回は値の上書きなので, 後から適用したものを優先していればいい.

区間への加算

先程は区間へ定数を代入するタイプだったが, それぞれに値を加算するタイプのものも見かける.

• 区間取得: \(\sum_{i \in I} x_i\)
• 区間更新: \(x_i \leftarrow x_i + z\)

すぐ思いつくのは次のようなものだ. \(X\) は先程と全く同じで良さそう. それから \(M\) は \(M=\mathbb Z\) で \(m(x) = m+x\) とでもしておけば動きそう. これは実は間違えている.

なぜなら, \(m(x_1 \times x_2) = m(x_1) \times m(x_2)\) というモノイド作用が満たすべき準同型を満たしていない.

例えば \(m\) が \(+1\) することを表してるとき, 各子ノードに \(+1\) したのに親ノードにも \(+1\) してるようなものだからだ. 親ノードは子ノードの値全ての和を表してるはずだから, 各子ノードに \(+1\) したなら, ノード数分だけ, 加算する必要が生じる.

じゃあ \(X\) にそのノード数まで情報として持たせればいい. つまり \(X\) はカバーする区間に含まれる値の和と区間の長さのペアにする.

• \(X = \mathbb Z \times \mathbb N\)
  • (和, 長さ)
  • 積
    • \((x_1, \ell_1) \times (x_2, \ell_2) := (x_1 + x_2, \ell_1 + \ell_2)\)
  • 単位元
    • \((0, 0)\)
• \(M = \mathbb Z\)
  • \(m \in M\) は \(+m\) することを表す
  • 積
    • \(m \times n = m + n\)
  • 単位元
    • \(0\)
  • 作用
    • \(m(x, \ell) = x + m \ell\)
      • ここが重要

長さ \(\ell\) の区間があって今そこの和が \(x\) のとき, この各値に \(m\) を足すと, 和は \(x + m \ell\) . 当たり前ですね.

例題

• 区間取得: \(\sum_{i \in I} x_i\)
• 区間更新: \(x_i \leftarrow b x_i + c\)

今度は足すだけじゃなくて掛け算も入ってる. でもさっきのとほとんど同じ.

作用 \(m = (b, c) \in \mathbb Z \times \mathbb Z\) について,

• \(m(x, \ell) = bx + c\)

というのが実際の作用だし, \(M\) の積はこれを満たすように適切に定めるだけ.

どんな情報があれば転倒数がマージできるか考えればおのずと \(X\) が決まる.

区間 \(I_1\) を左に, \(I_2\) を右にしてマージするとき, 出来上がった区間の転倒数は, それぞれの転倒数はそのまま足して, 新たに出来る転倒というのは \(I_1\) に含まれる \(1\) の数と \(0\) の数との積, これを加える. 従って, まず \(0,1\) それぞれの個数と, 転倒数を情報として持っておけば良さそう.

さてこの問題における区間に対する更新というのが 0/1 のフリップ操作. フリップしたときに出来る転倒数は今述べた3つの情報だけからは分から無さそう. しかし, 「フリップしたら転倒する」数というのも転倒数と同じ計算量で計算できるに決まってるので, これも持っておけばいい. つまり, \(X\) はその区間における

• \(z =~\) \(0\) の個数
• \(o =~\) \(1\) の個数
• \(i =~\) 転倒数
• \(p =~\) 逆転倒数 (0/1 をフリップした場合の転倒数)

の組 \(x = (z,o,i,p)\) . そして積は

\[x_1 \times x_2 = (z_1, o_1, i_1, p_1) \times (z_2, o_2, i_2, p_2) = (z_1 + z_2, o_1 + o_2, i_1 + i_2 + o_1 z_2, p_1+p_2+o_2z_1)\]

で定義される.

更新操作は簡単で, フリップするかしないかの2状態しかない. 「スリップする」をちょうど2回適用したときはもとに戻って「フリップしない」と等しいことに注意しよう.

\(\def\true{\mathrm{true}}\def\false{\mathrm{false}}\) \(M = \{\true, \false\}\) としておいて,

• 作用
  • \(\true(z,o,i,p) = (o,z,p,i)\) (交換する)
  • \(\false(x) = x\) (交換しない)

を定める.