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

第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 n3n1 + 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 まで