TAPLを読む 01

2019-10-01 / [tapl]

3.2 構文

定義 3.2.1は形だけみるとGATDsの構文そのものだ。さらにGADTsで定義した関数はどれも推論規則を表す文法でもあった。

P → QはHaskellの関数p -> qと同じとみなしていることになる。

このTが"木"の集合を表している、というのは、帰納的に定義されている場合限りそう言えるのではないだろうか。要素を外延的に並べただけでは木ではなく列なので。

命題 3.2.6 T = S

難しい。何をしようとしているのかはなんとなく分かる。 T = Sを示すために、数学的帰納法を使っているようだ。

補題 3.3.3

証明の行間がすごい。「なんでそこからそれが言えるの？」という跳躍が埋められない。と思ったけれど、sizeの定義を読めば自動的に大小関係は明らかになるのだった。

定理 3.3.4 [項に関する帰納法の原理]

\( \forall s \in T (\forall r \in T depth(r) < depth(s) \land P(r)) \to P(s) \)

\( \forall s \in T (\forall r \in T size(r) < size(s) \land P(r)) \to P(s) \)

きました意味論。いつもconstallationさんとかが「セマンティクス」とよく言うやつ。なんなのだセマンティクスって。意味論って謎だ。自然言語での意味はとても不安定だからだ。というか意味は検証できないのではないかと思ってしまう。人の思考の中にしか現出しないものだと思っているから。

でも計算機の理論では違うのかもしれない。

そう、意味論という時の意味は「いったい誰のための意味なのか」が分からないとダメだ。それをポイントにして読もう。

「項がどう評価されるか」それが意味論とのこと。評価する主語はなんだ？処理系か？

「単純な言語では、機械の状態は単なる項であり、機械の振る舞いは遷移関数で定義される。」

項はデータ、遷移関数によりデータはどんどん変換されていき、いずれ停止状態となる。ということか。

「項tの意味は、tを初期状態として動き始めた機械が到達する最終状態と考えられる。」

つまり項の評価を繰り返した結果が意味だとする。 1 + 1 * 2という項を評価した結果3が項の意味である、ということができる。インタプリタ−は意味を出力するらしい。

「項の意味は単なる機械状態の列ではなく、数値や関数などの数学的な対象として捉えられる。」

項が数式になるということだろうか。数式になるとどうなる？

「言語に表示的意味を与えることは、意味領域の集まりを見つけ、項を意味領域の元に写す解釈関数を定義することである。」

意味領域が解らないから何を言っているのかわからない。

意味領域: semantic field

命題論理における意味領域とは真理値のことらしい。参考

自然数の演算の意味領域は自然数ってことかな。

二進数のx86命令セットの集合Sへの解釈関数が定義されていれば、その言語にx86意味領域に対する表示的意味を与えることができる、ということか？

操作的意味論が実践的なのに対して表示的意味論が理論的に感じた。