• 高橋正子 計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)

面白かったところや、自分の理解のまとめ。他にも色々載ってる良い本。

帰納的関数

  • 原始帰納的関数
    • ざっくり言うと、c言語でfor (int i = 0; i < n; ++i) { ... }の形のfor文だけ、while文や再帰呼び出し禁止で書けるようなものに対応する関数
    • 全域的、プログラムで言うと必ず停止する
    • 必ず停止するからといって、これに含まれるとは限らない
  • 帰納的関数
    • 原始帰納的関数に$\mu$演算子を加えたもの
      • $\mu$ 演算子とはwhile文に相当するもの
    • turing機械で計算できるのと一緒
    • 部分関数を含む、つまり停止するとは限らない
    • $\mu$演算子は高々1つあれば十分、つまりプログラムに無限loopになりうるloopは1つでよい

型無し$\lambda$計算

  • Church-Rosser性
    • $\lambda$式は好きな順に簡約しても最終結果は不変
  • 正規化定理
    • もし$\beta$簡約を終わらせられるなら、左から簡約していけば終わる
    • 値渡しだと動かないけど名前渡しなら動くプログラムがあるよ、ということぽい

領域理論

  • プログラムで用いるデータ構造って数学的な対象でいうとどんなの？ -> 完備半順序集合(cpo)が妥当
    • エラーだとか無限ループ表したい
      • 情報量の大小を順序にして、エラーとかは最小元と解釈しよう
    • 計算の極限を表したい
      • プログラムは円周率の真の値を算出することはできないけど、3, 3.1, 3.14, 3.141, 3.1315, … というように近付く列はいくらでも計算できて、その極限は真の値
      • fact n = n * fact (n - 1)みたいな再帰してる関数を展開しきるのは無理だけど、0回, 1回, 2回, 3回, … とどんどん展開していくことはできて、その極限は無限に展開した結果
      • そういった列に極限が存在してほしい
  • じゃあプログラムは数学的な関数でいうとどんなの？ -> 連続関数
    • 上の要求がいい感じになればよい
    • 単調
      • 情報量がひっくり返ったりしては困る
    • 極限を保存する
      • 極限がちゃんと扱えなきゃ困る
  • 領域方程式
    • $\lambda$式って関数かつ値なので困る
      • $X \simeq [X -> X]$な$X$を探す
      • $F(X) = [X -> X]$とすると$X$は不動点

$\lambda$計算のmodel

  • 幾つかの公理を満たす数学的構造
  • $D_\infty$
    • 任意のcpoを始点に構成される無限列が台集合
      • 表したいのはその極限
        • Cauchy列による実数の定義と似てる気がする
      • むりやり領域方程式を解いた
    • 圏論勉強会の動画なんかでちょっと触れられてたやつ
      • 別に圏論がなくても語れる
    • $\lambda$式の簡約の極限が反映された構造
      • これでの解釈で作られる$\lambda$式の同値関係は、$\beta$同値でなくても計算結果が極限的に一致する場合等しい
  • $P_\omega$
    • 自然数の集合の全体が台集合
      • $\mathbb{N}\times\mathbb{N}$と$\mathbb{N}$は濃度が同じなので埋め込める
    • $D_\infty$と比べると手軽
      • 極限だとかが不要な場合こちらを使う