なのログ

だから見てて下さい・・・俺の・・・変身

型システム入門を読んでいます(第1回)

第1回です。
はじめ第2回と書いてしまい消しました。やっぱ0オリジンってクソだわ。

それでですね、わりかし元気に読んでおります。
今3章です。と言うと進みが良いように感じられるかもしれないんですが、

1章「はじめに」:型システムとは何か、型研究の歴史とかをちょっと紹介
2章「数学的準備」:これから使っていく、集合関連の定義や帰納法の準備

といった内容です。つまりは場合によっては読まなくていいエリア。なんだこの牛歩。
ちなみに続きは、

3章「型無し算術式」:実際に(極簡単な)構文を定義して、それについて考える
4章「算術式のML実装」:まだよんでないからわかんないよ!

となっております。
そのまま32章まで。魔界かな?


で。

僕がこの本を開いて、初めにネットの海に訪ねたことを書きましょう。

記号 説明
a∈A aはAの要素 Aはaを(1要素として)含む
A⊂B 部分集合 AはBの部分集合
A∪B 和集合
A∩B 積集合
Φ ゼロ集合
/A 補集合

是非「マジかよ」と思って頂きたい。
(要するに、2章「数学的準備」の内容です)
(そして冊子中では説明されないレベルの常識)(ぶっちゃけ高校数学)

いやその、これに関しては微妙に事情がありまして、
僕、学生の頃にこの内容を勉強してないんですよね。

とはいえ、論理学っていう題目ではやることをやっていたり、
論理の証明の背理法とか帰納法っていう言葉に覚えはあったりとするので、
だいたいは大丈夫なはずです。しかし記号を扱ったことがマジで一切無かった。

というわけでググりました。
和集合と積集合がほんとにもう入ってこなくて、
ぶっちゃけこれまで生きてきた中でもこの記号達を見ては
「どっちがキャップでどっちがカップこの野郎もっとわかりやすくしろ
とブチギレていた訳ですが、今回やっと覚えられたと思います。
なんか上からきたやつ全部受け止めそうな形してるから和集合。こんなん。

ほんと、正直な願望を言うと記号に+とか✕とかORとかANDとか
書いておいて欲しすぎましたね。なんやねんこの視覚的になんでもねえ記号。(キレすぎ)

まあこんな部分で文字を連ねても仕方がないので、
つらつらと読んでいる事でも書いていこうと思います。

ぶっちゃけわからん所はわからんままに読んだりしているんですが、
とりあえず一旦一周(あるいは11章らへんまで)読んでみて、
後から見返すなどしてみたいところです。※「11章らへんまで」の理由↓
数学初心者のための「型システム入門」入門 - 廻る技術の覗き穴


3章「型無し算術式」

この章に入ったところ、すぐに言語体系が定義されました。

値として3つ

true  (定数:真)
false (定数:偽)
0     (定数:ゼロ)

関数、式(演算子)として4つ

succ t    (tの後の値)
pred t    (tの前の値)
iszero t  (tのゼロ判定)
if t then t else t (条件式)
※tは任意の項

なのやつ氏はなんだかこの時点で何もわからないまま
「お、それっぽい~」などと言いながら手を叩いて喜んでいます。猿か。

なんだか、
「とりあえず確かに?機械語寄りに考えて?どんな値でも作れそうだな?」
とか感じ取っています。

そして次のページで一文あり「っはぁ~~型無し算術式完全に理解した」とか言い始めます。

この項の構文は succ true や if 0 then 0 else 0 のような怪しげな項の形成を許すことに注意されたい。このような項については後でもっと述べることとしよう。実際、ある意味まさにこうした例のおかげで、この小さな言語が本書の目的から見て興味深いものとなっている。 (ページ18)

「それなんだよな~~俺言われる前から思ってたわ~~完全に理解した」

要は「"trueの次の値"って何だよ?」とか「"もし:0"って何がだよ?」となるよねという話で、
(Cあたりの経験のせいで"if 0"は定義できそうな気がしてしまうものの、)
「それを許す許さないってまさしく型の話~~ハァ勝った~~~」とか言っています。

余裕やな!型無し算術式!


そうは問屋が卸すめえ。

次の見開きの一角です。

[具体的な項の定義] 各自然数について、集合Siを以下のように定義する。

S0      = Φ
S(i+1)  =   {true, false, 0}
        = ∪ {succ t1, pred t1, iszero t1 | t1 ∈ Si}
        = ∪ {if t1 then t2 else t3 | t1, t2, t3 ∈ Si}

「は~~ うん ちょろい ちょr・・・ ? はい? 何て?

ここを噛み砕くのに結構かかりました。
要は冒頭の集合の記号の確認に戻ったりしました。

今はなんとかわかります。これをした意図は微妙に謎ではあるんですが。
要は「が処理ステップみたいなもので、その処理ステップ内で表現できる値を全部出しました」
みたいなことだと思っています。

ステップ数0だとなんにもなくて、
ステップ数1だとはじめから定義されている値3つ(true,false,zero)、
ステップ数2だとそいつらにそれぞれ前とか後とかゼロ判定とかifとかかけたやつ...
と、どんどん増えていく感じです。
if ~ then ~ else ~ の種類が3乗のオーダで増えていくので、わりと爆発的なやつです。

と、まあ「書いてあることはわかったけど何故それを書いたのかはわかんねえな」
という感じでここは納得をしました。
上述の処理ステップ的な事で正解してろ・・・!という気持ちしかない。

あとなんかSiに含まれる項tに対して、
内部に現れる定数の集合を Const() とする定義、
性質として
Size()(直線に連なった処理の数)と
Depth()(分岐の中で一番処理が多い数)というものが導入されました。

「せやな」と思って流し読みました。
使われる様子が出てこないと・・・わからないんだ・・・俺・・・。


3.5 「評価」

章は少し進みまして、3.4 「意味論のスタイル」とかを軽く読み飛ばしつつ
現在この部分を読んでいます。

さっきまで処理ステップが進むたびにいたずらに長くなっていた式に対して、 ifとかの処理を進めて評価して、結果的にこの値だよね、ということをするのが書いてあるっぽいです。
それとなくプログラミング屋に馴染みのありそうな内容な気がして、するっと読めそうな気はします。

ぶっちゃけあと2ページとかで3.6「注記」を含めて3章が終わるところまで読んでいるんですが、
わりと文字を連ねた気がするのでここで区切っておきます。

次回はこの型無し算術式を解析して評価する感じだと思います。そいでは。