帰納法と余帰納法にまつわる伝承

これはAmusement Creators Advent Calendar 2017の14日目の記事です.

adventar.org

最小不動点と最大不動点のよく知られた話とか時相論理に絡めた話をゆるゆるっとするつもりです.
分かりにくかったり変なことを言っていれば気軽にご指摘ください.
記事を書き終わった後に見返してみるとかなりぐだぐだしてます.

先に記号の説明をしておきます.

  • [] ... 空の列
  • [e1, e2, e3] ... 先頭から順に要素がe1, e2, e3であるような列
  • e :: l ... 列lの先頭に要素eを付け加えてできる列

例えば[1, 2, 3]1 :: 2 :: 3 :: []は同じものです.

それと,出てくる関数 Fはすべて単調であると思ってください.

帰納法(最小不動点

次のような列の集合を受け取って列の集合を返すような帰納的な関数を考えましょう.
帰納的というのは「もしxが性質Pを満たすならxをもとにして作ったものもPを満たす」という性質のことです.

 {\begin{align}
F(X) = \{[\;]\} \cup \{ 1:: x \mid x \in X \}
\end{align}}

ここで関数 Fについて閉じている(つまり F(X) \subseteq Xである)ような集合のうち 最小 のものを Fについての最小不動点といって\mu Fと書きます.
関数 Fについて閉じている集合としては例えば

 {\begin{align}
\cdot\quad & \{[\;], [1], [2], [1, 1], [1, 2], [1,1,1], [1,1,2], \cdots\} \\
\cdot\quad & \{[\;], [1], [1, 1], [1,1,1], [1,1,2], [1,2,3], [1, 1, 1, 1], [1,1,1,2], [1,1,2,3], \cdots\}
\end{align}}

などがあり,その中でも最小のもの,つまり最小不動点は直観的にはすべての要素が1であるような列すべてからのみなる集合です.

一般的に最小不動点の近似解を求めるにはKnaster-TarskiとCousot-Cousotという二つの手法が知られています.

Knaster-Tarski

こちらの手法はかなり定義通りで, F(X) \subseteq Xをみたすような集合 Xすべてを計算してそのintersectionを取ります.
しかし現実的には F(X) \subseteq Xを満たす集合 Xすべてを計算するのは難しいので見つかった範囲でのすべての集合のintersectionをとることになります.
見つかった集合が多ければ多いほど近似で得られる集合は小さくなって最後には \mu Fそのものになるので,この近似で得られる集合を Sとすると \mu F \subseteq Sが成り立ちます.
つまりこれは \mu Fの過大近似を求める手法です.

Cousot-Cousot

こちらの手法でのアイデアは「余分なものを含まずに必要なものだけを集めたら最小のものになるはず」です.空集合を初期状態として集合が Fについて閉じたものになるまで必要な要素を追加していきます.
先ほどの例だと

 {\begin{align}
S_0 &= \emptyset \\
S_1 &= F(S_0) = \{[\;]\} \\
S_2 &= F(S_1) = \{[\;], [1]\} \\
S_3 &= F(S_2) = \{ [\;], [1], [1, 1] \} \\
S_4 &= F(S_3) = \{ [\;], [1], [1, 1], [1, 1, 1] \} \\
\end{align}}

と展開していって S_{n+1} = S_nとなるようなnがあれば \mu F = S_nだ,ということです.
もちろんそんなnがいつも見つかるわけでなく,どこか上限を決めて打ち切らないといけません.
無限回繰り返していれば追加されるような要素がこの近似で得られた集合Sには含まれていないかもしれないので, S \subseteq \mu Fであることがわかります.
つまりこれは \mu Fの過小近似を求める手法です.

帰納法(最大不動点

次のような列の集合を受け取って列の集合を返すような余帰納的な関数を考えましょう
帰納的というのは「もしxが性質Pを満たすならxの部品もPを満たす」といったような性質のことです.

 {\begin{align}
F(X) = \{ x \mid (1 :: x) \in X \}
\end{align}}

ここで関数 Fについて整合している(つまり X \subseteq F(X)である)ような集合 Xのうち 最大 のものを Fについての最大不動点といって\nu Fと書きます.
この場合の最大不動点は直観的には1の無限列からのみなるような集合です.

一般的に最大不動点の近似解をもとめるには最小不動点と同様にKnaster-TarskiとCousot-Cousotの二つの手法が知られています.

Knaster-Tarski

やはりかなり定義通りで, X \subseteq F(X)をみたすような集合すべてを計算してそのunionを取ります.
しかし現実的には X \subseteq F(X)を満たす集合すべてを計算するのは難しいので見つかった範囲でのすべての集合のunionをとることになります.
見つかった集合が多ければ多いほど近似で得られる集合は大きくなって最後には \nu Fそのものになるので,この近似で得られる集合を Sとすると S \subseteq \nu Fが成り立ちます.
つまりこれは \nu Fの過小近似を求める手法です.

Cousot-Cousot

こちらの手法でのアイデアは「いらないものを捨てていけば最後にはいるものだけ残るはず」です.全体集合を初期状態として集合が Fについて整合したものになるまでいらない要素を除去していきます.
これまた全体集合が無限集合だと何回いらない要素を除去しても終わらないことがあるのでどこかで操作を打ち切る必要があります. 無限回繰り返していれば除去されるような要素がこの近似で得られた集合Sには含まれているかもしれないので, \nu F \subseteq Sであることがわかります.
つまりこれは \nu Fの過大近似を求める手法です.

まとめ

以上をまとめると

過小近似 過大近似
最小不動点 Cousot-Cousot Knaster-Tarski
最大不動点 Knaster-Tarski Cousot-Cousot

って感じです.

帰納法(最小不動点)と余帰納法(最大不動点

最小不動点の定義と最大不動点の定義を並べてみましょう.

  • 最小不動点 ...  F(X) \subseteq X であるような Xのうち 最小 なもの
  • 最大不動点 ...  X \subseteq F(X) であるような Xのうち 最大 なもの

きれいに対応づいていることが分かると思います.
この対応はめっちゃ綺麗で, \land \lorの対応ぐらい綺麗でかっこいいです.

モデル検査と帰納法・余帰納法

最大不動点の例で出した1の無限列は何かの最小不動点の要素になりえるでしょうか?
実はそうはなりません.なぜかというと最小不動点はベースケース(例だと空列)を用意してそこから構成できるものを集めたものなので必ず終わり(ベースケース)を含んでおり,無限であるようなものは表せないからです.
そう,最小不動点の要素であるような列はかならず有限なので先頭から順番にパクパク要素を食べていくとかならずベースケースに到達するのです.
この性質から最小不動点は「いつか必ずベースケースを満たす」という意味を持つと読むことができます.
逆に,余帰納法は性質Pを満たすものを何回分解しても性質Pを満たすことを表しているので最大不動点は「いつも必ず性質Pを満たす」という意味を持つと読むことができます.
これは「いつか」とか「いつも」とか言っているので時間に関する制約だとみることができて,まさに,まさに,様相論理の一つである時相論理のFとGに対応します.

こういうわけで最小不動点や最大不動点は時相論理と深い関係にあります.

nyan

最小不動点と最大不動点が入り組んだ制約の解析はある条件を満たせばパリティゲームというゲームの必勝戦略が存在するかという問題に帰着できてゲーム理論とも関係があったりします.

もちろんこの記事で余帰納法について述べ切れているわけではありません(そもそも僕は勉強している途中なので).
帰納法帰納法との綺麗な対応関係やその他もろもろはとても面白いのですが,余帰納法知名度帰納法に比べてとても低いように感じられるのが残念です.

参考になったもの

帰納法・余帰納法の説明はやはり型システム入門(Type and Programming Languages)の21章が一番分かりやすいと思います.

その他には住井先生の日記が初学者にはわかりやすかったです.
帰納法と余帰納法の何がどう双対なのか(初等的に) - sumiiの日記
余帰納的定義 - sumiiの日記

この記事はPOPL16の発表スライドを参考にしました.
http://group-mmm.org/~ichiro/talks/popl2016pub.pdf

C言語で関数のオーバーロード

これはAmusement Creators Advent Calendar (ACAC) の6日目の記事です.

adventar.org

C++C#にあってC言語にはない機能の一つにオーバーロード (overloading) というのがあります. これはC言語でもCPP(CPreProcessor)を使えば限定的ではあるけれどもオーバーロードミミックできる!という内容の記事です.

オーバーロードって何?

オーバーロードってなんなんでしょう?とりあえずC++でどう定義されているのか見てみます.
現行C++ (C++17) のdraftは多分 n4659*1 なのでこれを読んでみると16章で大々的にoverloadingについて言及されているのが見つかります.
冒頭の部分を訳すと"同じスコープにある一つの名前に対して2つ以上の異なる宣言が指定されているとき,その名前はオーバーロードされているという. 付け加えて,同じスコープで同じ名前に対する型の違う宣言が2つあったときそれらはオーバーロード宣言と呼ばれる.関数と関数テンプレートの宣言だけがオーバーロードできて変数や型の宣言はオーバーロードできない" でしょうか.
多分このあたりは他の言語でもだいたい同じなんじゃないかなーと思います.例を出すと

#include <iostream>
void hoge(int) { std::cout << "neko" << std::endl; }
void hoge(char) { std::cout << "inu" << std::endl; } // valid
void hoge(int, int) { std::cout << "syounen" << std::endl; } // valid
// void hoge (int) { std::cout << "piyopiyo" << std::endl; }  ! invalid ! 型が同じ宣言はダメ

int main() {
    hoge(42); // neko
    hoge('a'); // inu
    hoge(42, 'c'); // syounen
}

ってかんじです.
別のことをする関数に同じ名前を付けるのは良くないとかオーバーロードがあるような言語は型推論が決定不能になるといった理由から単純なオーバーロードという機能はあまり好まれていないフシがありますが,まぁこれはオアソビですしC言語には型推論なんて無いのであんまり気にせずいきましょう.

本題

CPPを使ってC言語でもオーバーロードみたいなのを書けるようにしたいんですが,CPPはトークン列しか見れないので型によるオーバーロードはできません.なので引数の違いによるオーバーロードで勘弁して下さい.残念.

実際のコードはこんなかんじです

void hoge1(int n) { printf("neko %d\n", n); }
void hoge2(int n, char c) { printf("inu %d%c\n", n, c); }

#define SELECTER(ONE_, TWO_, SELECT, ...) SELECT
#define HOGE(...) SELECTER(__VA_ARGS__, hoge2, hoge1) (__VA_ARGS__)

int main() {
    HOGE(42);  // neko 42
    HOGE(42, 'a'); // inu 42a
}

マクロHOGEに渡した引数の数が1つならhoge1が,2つならhoge2が呼ばれていることがわかります.
どうしてこのような挙動をするのでしょう?
引数が1つのときを考えるとHOGE(42)SELECTER(42, hoge2, hoge1) (42)に展開されて次にSELECTER(42, hoge2, hoge1)の部分がhoge1に展開されるので最終的にhoge1(42)になります.
引数が2つのときを考えるとHOGE(42, 'a')SELECTER(42, 'a', hoge2, hoge1) (42, 'a')に展開されて次にSELECTER(42, 'a', hoge2, hoge1)の部分がhoge2に展開されるので最終的にhoge2(42, 'a')になります.
つまりSELECTERは前から3番目を取り出すマクロで,そこにHOGE__VA_ARGS__を渡すことでHOGEの引数の数に応じてSELECTERが選ぶトークンがずれるようになってるんですね.
同じテクニックを使えば与えられた引数の数を計算するマクロも作れそうですね.つまりこうです

#include <stdio.h>

#define SELECTER(ONE, TWO, THREE, FOUR, N, ...) N
#define N_ARGS(...) SELECTER(__VA_ARGS__, 4, 3, 2, 1)

int main() {
    printf("%d\n", N_ARGS(neko));  // 1
    printf("%d\n", N_ARGS(neko, inu, syounen));  // 3
}

この例では4つまでしか引数の数を計算できませんがもっと数を増やせば増やした分だけ計算できる引数の数を大きくすることができます.

参考にしたもの

XeLaTeXやLuaLaTeXでascmac.styのitemboxやscreenを使うとき

覚え書き
XeLaTeXやLuaLaTeXでは\tbaselineshift(縦組の和欧文のペースラインの位置調整)が定義されていないのでascmac.styのitemboxやscreenを使おうとすると

! Undefined control sequence.
\screen ->\@savetbaselineshift \tbaselineshift
                                               \tbaselineshift \z@ \@ifnextc...

と怒られる.

なので\usepackage{ascmac}の時に

\usepackage{ascmac}
\newdimen\tbaselineshift

とする.

参考: http://oku.edu.mie-u.ac.jp/tex/mod/forum/discuss.php?d=1454

OCamlのannotファイルの読み方

ocamlcやocamloptでnyan.mlを-annotオプションを付けてコンパイルするとnyan.annotファイルが生成される。 このファイルにはコンパイルするときに得られた識別子のスコープとか式の型とか関数呼び出しが末尾再帰かそうでないかとかの情報が含まれています。例えばテキストエディタが末尾再帰をハイライトする時にこのファイルを使えます。
annotファイルのフォーマットは中身を見れば大体分かるだろうけど、取り敢えず使いそうな事をメモしておきます。
この記事は雰囲気を感じ取って書いています。正式なフォーマットの解説とかあれば教えてください。

*はdon’t careだと思ってください。

annotファイルがどうとか以前に僕はOCaml自体についても初心者なので変なこと書いてるかもです。指摘していただけるとありがたいです。

全体

情報はそれぞれの式や識別子に対して

"ファイル名1" * * 開始位置 "ファイル名2" * * 終了位置
情報名1 (
  情報の詳細
)
情報名2 (
  情報の詳細
)
...

という形式で記述されています。
“ファイル名1"の"開始位置"から"ファイル名2"の"終了位置"までがその式や識別子の書かれている場所です。普通は"ファイル名1"と"ファイル名2"は同じになると思います。
情報名1や情報名2は型とか識別子とかそういうのです。 例えば

"main.ml" * * 8 "main.ml" * * 11
type(
  int -> int
)

って書いてあると先頭から8〜11の位置に書かれてあるものの型がintからintへの関数なんだなーって分かります。

識別子

識別子の宣言に対しては

ident(
  def 識別子 "ファイル名" * * 開始位置 "ファイル名" * * 終了位置
)

という情報がつきます。これは指している文字列は宣言された識別子であり、そのスコープは開始位置から終了位置であるということを示します。

また変数の使用については

ident(
  *_ref 名前 "ファイル名" * * 開始位置 "ファイル名" * * 終了位置
)

という情報がつきます。これは指している識別子が"名前"という名前の変数であり、その変数は開始位置から終了位置で宣言されていることを示します。
この"名前"はモジュール名込みの名前っぽいです。

関数呼び出し

関数呼び出しが末尾再帰であれば

call(
  tail
)

非末尾再帰であれば

call(
  stack
)

という情報がつきます。

WebAssembly手書き (wast) で簡単なSTGを作った

WebAssembly (wasm) のテキスト表現でwastというものがある。
僕の所属しているAmusementCreatorsの48時間ゲームジャムでこのwastをがりがり書いて簡単なSTGを作った。
デモはこちら https://akitsu-sanae.github.io/works/wast-game/index.html
ソースコードはここのgame.wastを見てください https://github.com/akitsu-sanae/wast-game

Web周りの知識に疎いので有名なブラウザで動かないようなコードを書いてたらごめんなさい。指摘してくれると嬉しいです。

wastを書いた感想は記述量の多い昔のC言語って感じだった。キーボードを打つのが疲れるけど思ってたよりマゾマゾしくない。

今回で得られた知見をまとめて一つの記事にする予定。WebAssembly手書きマン増えてくれ。

ゲームを作るにあたって参考になったものを上げておく

C/C++の可変長引数マクロで引数の数でオーバーロードしたい

#define SELECTER(_1, _2, SELECT, ...) SELECT
#define FOO(...) SELECTER(__VA_ARGS__, NYAN, WAN) (__VA_ARGS__)

FOO(neko)       // expanded to `NYAN (neko)`
FOO(inu, dog)   // expanded to `WAN (inu, dog)`

参考

c - Overloading Macro on Number of Arguments - Stack Overflow

c++ - Can macros be overloaded by number of arguments? - Stack Overflow

RustでArrayにcollectしたい

Rustで以下のコードは違法

(0 .. 9).map(|i| i*i).collect::<[i32; 10]>::()

これは配列がFromIteratorを実装していないため.

こういう時はArrayVecを使う.

取り敢えずCargo.tomldependencies

arrayvec = "0.3.20"

を書き加えて

extern crate arrayvec;
use arrayvec::ArrayVec;

let result: ArrayVec<[_, 10]> = (0..9).map(|i| i*i).collect();
result.into_inner().unwrap()

とすればいい