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

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

2章メタ定理と帰納法による証明

  • 公理と原理の違いは?
    • 公理という言葉が出てこない?
    • 「公理的意味論」って言葉はありそう
    • 元の言葉がprincipleだったのでは
    • 「数学的帰納法」は証明できない? → できない。公理っぽい
    • agda : データ型に対する構造帰納法がビルトインで入っているから?
    • coqはともかくagdaは自分で書かなきゃいけない?
    • agdaはfixを書くことができない
    • データ構造に沿った再帰と帰納法は同じ

2.1.1 NatとCompareNat1-3に関するメタ定理

  • 定理 2.11
    • \(S(n)\) は任意の自然数? (0は自然数に入るか問題)
    • CompareNat2 では公理
  • 定理 2.12
    • \(S\)を剥がしても大小関係は変わらない
  • Comparenat 1-3 で特別なものはあるの?
    • 違いはない
    • 証明するものによっては向き不向きはある
  • 定理2.14はどのくらい示せばいい?
      1. → (2) → (3) だけ示せば

2.1.2 EvalNatExp に関するメタ定理

2.1.3 ReduceNatExp に関するメタ定理

  • 定理2.22が間違えている
    • \(e_2\)\(e_3\) がペアノ自然数まで簡約されてたら成り立たない?
    • \(e_2\)\(e_3\) がペアノ自然数ではない、という条件がいる
    • \(\to\) は1ステップだが、きちんと1ステップで合流はできる
  • 定理2.24
    • 自明では? → この場合は自明でしょう
    • 自明ではない作り方はできるの?
    • \(\to_d\)\(\to^*\) で定義した場合の違いとか
    • \(\to_d\)\(\to\) を模倣できる
  • 定理2.26はどう示す?
    • サイズのようなものを定義し、必ず減ることを示す
    • 演算子の個数、がよさそう
    • プログラム意味論の本では型について帰納法使ってたけど → この推論規則では型とかはないので
    • 型なしラムダ計算では強正規化可能性はなりたたない(だから型が必要)
      • \((\lambda x.x x) (\lambda x.x x)\)

2.2 数学的帰納法

  • \(\sum_{i=1}^0 i\) は定義できるのか → 定義は怪しいけど、\(i=0\)入れても変わらないのはまあそうだよね
  • 例2.31 : なんでこうなるか不思議(意味は分かるけど直観的ではないという意味で)

2.3 構造帰納法

  • \(Z \operatorname{plus} n_2 \operatorname{is} n_3\)\(Z \operatorname{plus} n_2 \operatorname{is} n_4\) が成り立つときに \(n_3 \equiv n_4\) は言っていいの?
    • Natの4つしかルールは使えない
    • 「はずである」にその気持ちが入っているのでは
  • Haskellでexistsどうするのみたいな話
  • 「P-ZEROの形より」をHaskellで表現するには
    • case で場合分けで矛盾では
    • inductive ではないのでHaskellでは無理でしょう ( undef あるし)

2.3.2 算術式に関する構造帰納法

  • 原理2.33が何を言っているのか
    • オペラントについてある性質が言えれば、+*したものも性質が言える。という状態ならすべての算術式について成り立つ
    • 自然数と違って再帰の仕方が木となる
  • 図2.3は\(Z*S(S(Z))+S(Z)\)を言いたいだけ

2.4 帰納法による定義

  • 関数って?
    • 同じ値について同じ値をただ一つだけもつ
  • 閉包性 == 全域性
  • s/定義2.4/定義2.35/

2.5 導出に関する帰納法

  • 導出のツリーを帰納法している
  • 導出の部分を省略するのは??
    • 導出規則が帰納法に適していない場合は省略できない(というか帰納法にならない)
    • わかっているなら省略してもいい
  • 読み替えたところが肝

2.6 整礎帰納法

  • 整礎性は集合の性質ではなく集合と順序を合わせた性質
  • 0 は? → 極小元。前提が \(\phi\) になる

今日は2章まで。