Pixel Pedals of Tomakomai

北海道苫小牧市出身の初老の日常

トップ > 技術 > 今日は 圏論勉強会 第9回 の日です

今日は 圏論勉強会 第9回 の日です

技術 数学

前々回ぶりに圏論勉強会ではない方の圏論勉強会 第9回に来ています。資料とustreamは公開されています。

第9回: 領域理論・不動点意味論 / 講師 @9_ties さん

  • 意味論は圏論が活躍する分野
    • たくさんあるが、今日は初歩的な重要な事柄をピックアップ
    • 今日一回で領域理論を終わる(!)
  • 意味論とは？ → プログラミング言語の意味を数学的に探求。理論計算機科学の分野
    • プログラムは実行することで意味がわかる。が実行せずに意味を知りたい
  • 表示的意味論(denotational semantics)→集合や関数に対応させる
    • fact n = if n = 0 then 1 else n * fact (n - 1) → fact n = n!
    • 計算とは何か(今でも答えは出ていない)
    • モナドも一種のdenotation。入出力やエラーを付け足すもの
    • 「マシン」「計算」の概念は消えている
  • 操作的意味論(operational semantics)→数学的に形式化された状態遷移系の遷移によって意味を記述
    • 項書換え系。先程のfactは簡約列で表現される
    • レジスタマシン、スタックマシンを考える場合も
    • 「マシン」「計算」の概念が残っている
  • 公理的意味論→公理と推論規則によって意味を与える
    • 先ほどのfactは、n=0の時にx=f nを実行するとxは1になる、のような定義
    • 手続き型言語の体系 → ホーア論理
  • この勉強会では表示的意味論をやる
  • 集合と全域的関数ではプログラムの意味を表示できない
    • 領域 → Dana Scott
  • 領域理論の要点
    • 計算の領域は、最小値を持つ完備半順序集合(cpo)
    • 計算を表示する関数は連続関数
  • cpo (complete partial order)
    • 始対象を持ち、ω余完備な半順序集合
    • 半順序集合(D, ≦)
    • 最小値0
    • 任意のω-chainに上限が存在
  • cpo Aからcpo Bへのω余連続な関手Fを単に連続関数と呼ぶ
    • F:A→Bと書く
    • a≦b → Fa ≦ Fb、F(lim x_i)=lim F(x_i)
    • 単調な連続関数だが、cpoを考えてる時点で単調は当たり前なので略
  • 最小不動点定理
    • Dはcpo、F:D→Dは連続 → あるxについて、x = F xとなる
    • 不動点の最小値は、lim F^i(0)
    • 証明。0≦F 0≦F^2 0 ≦ ...(ω-chain)。F(lim F^i(0))=lim F(F^i(0))=lim F^(i+1)(0)
      • ω-chainの先頭に0をつけただけなので、lim F^(i+1)(0) = lim F^i(0)なので不動点
      • 他の不動点x。0≦x。F(0)≦F(x)=xより、F^i(0)≦x。よってlim F^i(0)≦x。よって最小。
  • 不動点の例
    • f x = x * xの不動点はx=0、1
    • 任意の関数は ($) の不動点。($) ($) ($) (+ 1) は (+ 1)。ただしデータはこの不動点じゃない
  • 不動点は再帰と関連する。最小不動点定理は具体的な不動点の構成方法を与えることが重要。
    • 最小不動点の性質に基づき、性質を検証できる
  • どうしてcpoなのか
    • f n = if n < 10 then 0 else f(n+1)は10以上では未定義
    • 部分関数(partial function)という→⊥が必要
    • fはN→NではなくN∪{⊥}→N∪{⊥}
    • 直積を考えると(1, ⊥)や(⊥, 2)が含まれる → 部分オブジェクト(最近は呼ばないらしい)。
    • 遅延評価だと、fst (1, undefined)はundefinedにならない
  • 部分オブジェクトにcpoの構造を入れられる
    • a≦b を a=⊥またはa=bで定義する。flat cpoと呼ぶ
    • 対には(a, b)≦(c, d)をa≦cかつb≦dで順序を入れる
      • Haskellだと⊥∈A×Bであり、⊥≦(⊥,⊥)となるので注意
  • 関数にも半順序を入れられる
    • g≦f を すべてのxについてg x≦f xで定義する
    • 例えば、g n = 0とすると先ほどの部分関数fについてf ≦ g
  • cpoについて、対、連続関数の集合もcpo
    • 始対象とlimを自明な感じで定義すればいい
  • a≦bを、bの方が詳しい情報を持っていると解釈すれば良い
    • ⊥は情報がない。0、1、・・・は情報がある
    • ω-chainは未定義部が減っていくようなデータの列
    • ω余完備はすべての情報を含む最小のデータが存在すること
    • 単調関数は、「入力の情報量を増やしたら出力の情報量も増える」ということ
      • fst (undefined, 1)よりfst (0, 1)のほうが情報量が多い
  • 再帰関数と不動点の関係
    • fact = (λf n. if n = 0 then 1 else n * fact (n - 1)) fact
    • factがF = λf n. if n = 0 then 1 else n * fact (n - 1)の不動点になっている
    • haskellだとfact = fix (\f n -> if n = 0 then 1 else n * fact (n - 1))
  • "最小"不動点とは、ノイズが入っていない不動点
    • 任意のcについて、λn . if n = 0 then 1 else c も λf n.if n = 0 then 1 else f (n+1) の不動点になってしまう
    • cはノイズと言える。良い表示と言えない
    • 再帰を最小の不動点として意味を与える → 不動点意味論
  • 最小不動点はlim F^i(0) だった。
  • 不動点帰納法
    • 許容的な命題(admissible)→ω-chainの全てについて真ならP(lim x_i)も真
    • 数学的帰納法によってP(⊥)が真、P(f)が真であればP(F f)も真であることを言えばよい
  • 例: マッカーシーの91関数
    • F f = λn. if n > 100 then n - 1 else f (f (n+11))の最小不動点をfとする
    • f 100までは91が返ってきて、その後は1ずつ増える
    • g n = if n > 100 then n - 10 else 91とするとf≦gであることを示せる
    • P(f)をf≦gとする。これが許容的かはほんとは別途議論が必要
    • ⊥≦gは自明。
    • h≦gとすると、F h = λn. if n > 100 then n - 1 else h (h (n+11))
    • ≦F h = λn. if n > 100 then n - 1 else g (g (n+11)) (単調性から)
    • =F h = λn. if n > 100 then n - 1 else g (if n + 11 > 100 then n - 10 else 91)
    • =F h = λn. if n > 100 then n - 1 else (if n + 11 > 100 then g(n - 10) else g(91))
    • =F h = λn. if n > 100 then n - 1 else (if n > 89 then (if n - 10 > 100 then n - 10 else 91) else 91)
    • =F h = λn. if n > 100 then n - 1 else (if n > 89 then (if n > 110 then n - 10 else 91) else 91)
    • =F h = λn. if n > 100 then n - 1 else 91 = g