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

Posted on August 23, 2015

第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\) になる

今日は２章まで。