『プログラム意味論』（横内寛文）
第1章 表示的意味論の考え方
第2章 ラムダ計算の基礎
第3章 領域理論の基礎
第4章 関数型言語の意味論
第5章 カテゴリ理論の基礎
第6章 領域方程式
第7章 ラムダ計算の意味論
意味函数を使う
2. ラムダ計算
2.2
def. 2.2.4 ラムダ式間の等式を導く体系 (pp. 17-18)
2.5
β簡約
def. 2.5.10
これは parallel reduction
pについてLを具体的に構成することでチャーチ・ロッサー性を証明する
reductionの記法
1重矢印→: 1ステップの簡約
頭が2重の矢印: 複数ステップの簡約
パスと解釈したwint.icon
2.6
ラムダ抽象では変数名の衝突回避が面倒
ただしξ規則の分だけ足りないので、拡張が必要
e.g. I, K, S
CL式は左結合
$ I=SKK
2.7
関数的, functional
普通のラムダ計算ではラムダ抽象だけが関数的
外延的ラムダ抽象ではすべてのラムダ式が関数
cf. 7章
η-変換
ポイントフリー相当wint.icon
§2.8 型付きラムダ計算
しっかりやりたいwint.icon
型構成子: →
→は右結合
いつものwint.icon
ラムダ抽象の束縛変数の右隣に型宣言を書く$ \lambda x\colon\sigma.M
muratak式は括弧で括る: $ \lambda(x\colon\sigma).M
正式な再帰的定義はここだけ拡張する
typing/type judgement（型付け・型判別式）
変数部分を無視すれば等しい
型判定式を導出する形式体系
規則は自然演繹のシークエントNMとみなす方がいいらしいwint.icon 派生規則
3つの推論規則
def 2.8.5
等式を追加した体系を考える
$ \Gamma（basis, context）
型判定式を導出する形式体系から誘導された3つの規則も使える
強正規化可能
Th. 2.8.10 強正規化定理
型が付くなら正規化可能
def. 2.8.11 帰着可能性で（間接的に）証明する
型の構造的帰納法で定義する
特に型構成子について
補題
帰着可能⇔強正規化可能
これと↓
強正規化可能性のリダクション順序上の推移律 $ M \rightarrow_\beta N wint.icon
リダクションのステップ数は単調減少 (>)wint.icon
β簡約の「λ→代入」を逆転させて「代入∧引数⇒λ」の帰着可能性を示すwint.icon
型が付くなら帰着可能wint.icon
→これで証明できる
η公理
定義可能
⇔ 関数をλ抽象でラップしても同じwint.icon
βη簡約も定義可能
練習問題
5. 型付きラムダ計算においては不動点コンビネータは存在しない
領域 (domain) = データの集合
プログラムも含む
cf. コンパイラ
3.1 データの近似と極限
ところで有限的に近似できるデータを扱うプログラムは計算可能函数とみなせる
e.g. ストリーム型
ref. 木原『数学基礎論と計算可能性』（数理科学, 2021, 8）
再帰的な（函数の）プログラムは本質的には無限長になる
p. 60
有限長で打ち切ると未定義⊥が出てくる
= 部分函数
プログラムを関数の近似で表せる嬉しさがここに現れてる
→ 極限？
cf. 3.3
部分関数$ [S \rightharpoonup T]
（有限的）近似のためのデータ構造を天下りに与えるwint.icon
$ a \sqsubseteq b: 近似（=低精度）↔高精度
最小元⊥$ \bot
最大元⊤$ \top
下限$ \sqcap X
上限$ \sqcup X
= 近似の極限
= 最小下界
つまり(元の)集合Xに入ってるとは限らない
ここですでに超越的な（＝有限的でない）操作があるwint.icon
上限の存在を保証したいwint.icon
最小元ありの定義を採用wint.icon
= pointed dcpo
つまりcppo
例
冪集合束
部分函数の集合
グラフと同型wint.icon
ここでスローガンwint.icon
平坦cpo (flat cpo)
集合$ S + \botにおいて$ a \sqsubseteq b \equiv a=\bot \lor a=b
最小元以外は互いに比較不能
1階層の木
部分函数を全域函数にできる
例
有界閉区間+実数全体R
系として、幅ゼロの区間を実数とみなせる。有理数の区間で極限的に表せる
prop. 3.1.12
上限の条件を任意のω鎖に弱めると、有向集合は上限を持つが濃度は可算に押さえられる
prop. 3.1.13
上限＝最小上界
prop. 3.1.14
$ \exists \sqcup \{ \sqcup{X_i} \mid i \in I\} \implies \sqcup \{ \sqcup{X_i} \mid i \in I\} = \sqcup{X} = \sqcup{(\cup\{X_i \mid i \in I\})}
3.2
データの近似列のω鎖から、プログラムの出力の近似列を作りたい
→単調関数
順序集合論における単調性の定義
プログラムが表す関数は単調である
def. 3.2.2 連続, continuous
f(sup X) = sup(map f X)
sup ▷ f = (map f) ▷ sup
スローガンその2
「プログラムが表す」
ここでの「プログラム」は AST 程度を意味するらしい
cpo上の連続関数は常に単調
連続⇒単調
単調⇏連続
反例: [0,1], λx.floor(x)
strict ω-chain (a⊏b)
⊑ではない
これがない⇔「単調性＝連続性」 (prop. 3.2.3)
有限の高さのcpo
e.g. 平坦cpo
Thm. 3.2.4 「cpo上の連続関数の全体はcpo」
関数に“外延的”な⊑を定義する
問題
3.3
部分関数の最小元0
Φ[fact]の極限で階乗関数を定義する
Thm. 3.3.1 最小不動点定理
cpo上の連続関数は不動点を持つ
誤植 1...
実行モデルがないと停止性を議論できない
環境の記法が分かりづらいwint.icon
3.4
構成例
直積
有限積も
非形式的なλ記法の導入
apply, curry も作れる
直和も作れる
直和空間
inl, inr の定義
ストリクト関数
正格関数？wint.icon
cf. 値呼び評価戦略
3.5
型付きラムダ式はすべて連続関数を表現する
型判別式の値を考えたい？
4.
PCFも関数型プログラミング言語
5.
具体例
Poset
CPO
Posetの部分圏
$ \mathrm{CPO}_{⊥}
Mon
直積があるならば、冪があるとき
CPO（圏）はcccである
Set（圏）もCCC
6
これが必要: $ X \cong \lbrack X \to X \rbrack
逆極限法という解法がある
表6.4 (p. 197) poset と圏の対応
table:poset-cat
poset category (Poset)
半順序集合 Posetの対象
a ⊑ b morph f: A → B
a ⊑ a id_A: A → A
transitivity compose ○
最小元 始対象
,
,
単調函数 函手
fix
fix eq
7. ラムダ計算の意味論
cf. Ω-コンビネータ
歴史的にはこれがオリジナルのモチベーションだったようだ？wint.icon
ref.