Hatena::Groupxn--272ax3f

論理と計算のしくみ 5.2

論理と計算のしくみ 5.2

プレゼンテーション

5.2 (a) β簡約 (p.197)

  • (\lambda x.M) N というλ項を M[x:=N] に等しいと考える
  • この書き換えを β簡約 という
    • M \rightarrow_\beta M'
  • βレデックス (β-redex, β基): β簡約で書き換えられる場所
    • λ項の出現をいうので ((\lambda x.x) y)((\lambda x.x) y) にβ基は 2 つ

β正規形

  • 例: (\lambda x.xx)(\lambda y.y) \rightarrow_\beta (\lambda y.y)(\lambda y.y) \rightarrow_\beta \lambda y.y
  • \lambda y.y のようにこれ以上簡約のできない形のλ項を β正規形
  • 簡約を続けても正規形に達しない例: (\lambda x.xx)(\lambda x.xx) (\Omega)

正規化の順序

  • 例: (\lambda x.\lambda y.x)(\lambda x.x)\Omega
    • 右のβ基から: (\lambda x.\lambda y.x)(\lambda x.x)\Omega \rightarrow_\beta (\lambda x.\lambda y.x)(\lambda x.x)\Omega\rightarrow_\beta \dots
    • 左のβ基から: (\lambda x.\lambda y.x)(\lambda x.x)\Omega \rightarrow_\beta (\lambda y.(\lambda x.x))\Omega \rightarrow_\beta \lambda x.x

β簡約の定義

文脈 (context) による定義 (p.200)
  • 文脈 (context):
    • λ項の部分項の出現のうちの一箇所が穴に置き換わったもの (穴あき項)
    • C[]\ ::=\ []\ |\ (M C[])\ |\ (C[] M)\ |\ \lambda x.C[]
      • []: 穴 (hole)
    • C[M]: C[] 中の穴を M に置き換えたλ項

文脈 C[] と項 M に対し、次のように定義されるλ項の間の二項関係をβ簡約と呼ぶ

C[(\lambda x.M)N] \rightarrow_\beta C[M[x:=N]]

規則を用いた帰納的定義によるβ簡約の定義 (p.200)
  • Beta
    • (\lambda x.M)N \rightarrow_\beta M[x:=N]
  • AppL
    • M \rightarrow_\beta M' なら MN \rightarrow_\beta M'N
  • AppR, Lam
    • 省略

これらの規則のみを用いて M \rightarrow_\beta N が導かれるときに限り M \rightarrow_\beta N

β簡約に基く二項関係

  • \rightarrow_\beta の反射推移閉包: \rightarrow^*_\beta
    • ex. M \rightarrow_\beta M', M' \rightarrow_\beta M''M \rightarrow^*_\beta M''
  • \rightarrow_\beta の反射推移対称閉包: =_\beta
  • 今後この =\beta でλ項を比較・分類していきます
  • =\beta の能力については後ほどチャーチ・ロッサー性

β簡約の例

チャーチ数

  • n に対応する チャーチ数 \bar{n} := \lambda f.\lambda x. f(f(\dots(f x)\dots))
  • succ = \lambda n.\lambda f.\lambda x.f(n f x) とおくと
    • succ \bar{n} =_\beta \bar{n+1}
  • add = \lambda m.\lambda n.\lambda f.\lambda x.n f (m f x)
  • mul = \lambda m.\lambda n.\lambda f.\lambda x.n (m f) x

論理演算・対

  • true = \lambda x.\lambda y.x
  • false = \lambda x.\lambda y.y
  • if \ L \ then \ M \ else \ N = L M N
  • if \ true \ then \ M \ else \ N \rightarrow_\beta M
  • if \ false \ then \ M \ else \ N \rightarrow_\beta N
  • (M, N) = \lambda z. if \ z \ then \ M \ else \ N
    • first = \lambda p.p \ true
    • second = \lambda p.p \ false

不動点演算子

http://upload.wikimedia.org/wikipedia/commons/1/16/Y-combinator-logo.gif

Y = \lambda f.(\lambda x.f(x x)) (\lambda x.f(x x))

Y による再帰関数の表現
  1. given 再帰的定義: f = \lambda x. \dots f \dots x \dots
  2. λ項 M = \lambda f.\lambda x. \dots f \dots x \dots
  3. 不動点を求める: F = Y M = Y (\lambda f.\lambda x. \dots f \dots x \dots)
  4. F =_\beta M F =_\beta \lambda x. \dots F \dots x \dots

(c) チャーチ-ロッサーの定理 (p.205)

  • 定理 5.1 λ項 M,M_1,M_2 に対して M \rightarrow^*_\beta M_1 かつ M \rightarrow^*_\beta M_2 なら M_1 \rightarrow^*_\beta M' かつ M_2 \rightarrow^*_\beta M' を満たす M' が存在する。
    • 図を見るとわかりやすい
  • 定理 5.2 M_1 =_\beta M_2 ならば M_1 \rightarrow^*_\beta M' かつ M_2 \rightarrow^*_\beta M' を満たす M' が存在する。
    • 図を見るとわかりやすい
  • 系 5.3 M のβ正規形 N が存在するなら一意的に定まり、M \rightarrow^*_\beta N となる (?)
  • 系 5.4 M と N とをβ正規形とする。M と N とが異なれば、M =_\beta N が成り立たない。

(d) チャーチ-ロッサーの定理の証明 (p.206)

  • ダイヤモンド が成り立てば容易だった…
    • ×「M \rightarrow M_1 かつ M \rightarrow M_2 ならば M_1 \rightarrow M' かつ M_2 \rightarrow M' を満たす M' が存在する」
    • 反例: (\lambda z.f z z z)((\lambda x.x)(\lambda x.x))
      1. \rightarrow f((\lambda x.x)(\lambda x.x))((\lambda x.x)(\lambda x.x))((\lambda x.x)(\lambda x.x))
      2. \rightarrow (\lambda z.f z z z)(\lambda x.x)
  • ダイヤモンド性が成り立つような二項関係 並列簡約 を考える (p.207)
    • 元のλ項にはじめから出現するβ基だけをβ簡約するような操作
      • ×(\lambda x.xx)(\lambda y.y) \Rightarrow_\beta \lambda y.y
  • M \rightarrow_\beta M' ならば M \Rightarrow_\beta M' である
  • M \Rightarrow_\beta M' ならば M \rightarrow^*_\beta M' である

証明

  • M \rightarrow^*_\beta M_1, M \rightarrow^*_\beta M_2 と仮定すると M \Rightarrow^*_\beta M_1, M \Rightarrow^*_\beta M_2 (\Rightarrow_\beta の性質)
  • 先ほどのダイヤモンド性より M_1 \rightarrow^*_\beta M', M_2 \Rightarrow^*_\beta M' を満たす M' が存在する
  • M_1 \rightarrow^*_\beta M', M_2 \rightarrow^*_\beta M' を満たす M' が存在する (\Rightarrow_\beta の性質])

以上

  • β簡約について
  • 二項関係 \rightarrow_\beta, =_\beta
  • β簡約の例
  • チャーチ-ロッサーの定理