今日は第1回「プログラミング言語の基礎概念」読書会の日です

Posted on July 5, 2015

第1回「プログラミング言語の基礎概念」読書会に来ています。音読方式なので、議論を中心にメモします。

はじめに

オンライン学習システムに登録して負荷を上げましょう

第一章 1.1

判断と形式は違うもの？
- 違う
推論規則をどう選べばいいの？
- アルゴリズムが存在するものもある
- センス？
- この例だと逆に辿ればいいけど、複雑になるとどうなのか
- completeじゃない公理系だと、導けないことを言えないこともある
- 式は可算個なので全探索はできる
自動化した例
練習問題をオンライン学習システムの砂場で（各自）
練習問題1.3 => \(1 + n_1 (n_2 + 2)\)
- \(N(n_1 \text{times} n_2 \text{is} n_4) = 1 + N(n_1 - 1 \text{times} n_2 \text{is} n_3) + N(n_2 \text{plus} n_3 \text{is} n_4) + 1\), \(N(Z \text{times} n \text{is} Z) = 1\), \(N(n_1 \text{plus} n_2 \text{is} n) = n_1 + 1\) より

1.2

何で具体化できるか、とは？ → SやZ
Fooがかっこ付いたりしてるのは？
- 規則の定義は (Foo) 、適用は Foo と書く
練習問題1.4はプログラムにて

1.3

less than の定義がこれでいいのか
- 逆で、 less than がこれで定義されている、ともいえる
- 現実的には、足りなければ規則を追加する
- 構文とルールを合わせるのは基本
- 公理が被っても公理系としては同じなので
練習問題1.5 → 各自砂場で
練習問題1.6 → CompareNat1 (\(N_2\) を任意に選べる)

1.4

バッカスさん 1978年
- FORTRANの開発から関数型言語の時代へ
- LISPは関数型ってよりメタプログラミングだよね
- ナウアーさんはAlgol 60で受賞
練習問題1.7 → (7)は外せない
練習問題1.8 → めんどい((4)くらいになると木が画面に収まらない)
R-Plusは “デルタ簡約” になってる
n1 plus n2 is n3 と n1 + n2 ---> n3 は何が違うの？
- 前者はペアノ自然数、後者は算術式
- 前後が逆なのが違和感 → 前提なので逆に見える
EvalNatExp は式から値、ReduceNatExpは式から式
PC持ってない人もいるので、練習問題は各自として次へ

第2章 2.1

なんで判断って呼ぶの？ → テクニカルタームなので、命題、でもO.K.
2.2節以降は飛ばせるらしいけど、今回は全部読む
s/metatheroy/metatheory/
\(\equiv\) の意味は？ → ペアノ自然数もBNFで書かれているのでO.K.
練習問題2.1の「意味」とは？ → 普通に大小関係でいい
定理2.12 → 逆はもともと推論規則に入っているので、これで同値になる
- 全て結論に S が入っているので、外せる、というのはなかなか奇妙
定理2.14 の証明は練習問題になってる
今回は 2.1.2 まで