不動点意味論メモ
(追記: 書籍のこのレジュメとは別に、不動点意味論の直感的イメージについての補足を、一番下に書き加えました。)
メモというよりは補間てかんじ。
- 作者: 横内寛文
- 出版社/メーカー: 共立出版
- 発売日: 1994/06/01
- メディア: 単行本
- 購入: 2人 クリック: 57回
- この商品を含むブログ (17件) を見る
の3.3より。
再帰関数
階乗の(再帰)関数定義
fact(x) => if x = 0 then 1 else x * fact(x - 1)
factを基にした、Φfact: [N -> N] -> [N -> N]の定義([N→N]はN上の部分関数)
Φfact(f)(x) => if x = 0 then 1 else x * f(x - 1)
Φでは未定義値undefも受け付ける。undefの定義
undef = N => undef undef * N => undef f(undef) => undef if undef then M else N => undef
3.1より: 部分関数factn(x)の半順序での最小限(fact0)はあらゆる引数で未定義
fact0(x) => undef fact1(x) => if x = 0 then 1 else undef fact2(x) => if x = 0 then 1 else x * (if x - 1 = 0 then 1 else undef) ... fact∞(x) =>
０(x) => undef
再帰関数の上限
任意の関数f: X->Xとn∈Nでの、f^n(x)の定義
f^n(x) => f(f(...(f(x))..)) (fがn個)
Φfact^n(０)の部分関数表現
Φfact^0(０)(x) => undef <= ０(x)
Φfact^1(０)(x) => 1 (x = 0) <= Φfact(０)(x) => if x = 0 then 1 else x * ０(x-1)
undef (x >= 1)
Φfact^2(０)(x) => 1 (x = 0) <= Φfact(Φfact(０))(x) => if x = 0 then 1 else x * Φfact(０)(x - 1)
1 (x = 1) => if x = 0 then 1 else x * (if x - 1 = 0 then 1 else (x - 1) * ０((x - 1) - 1))
undef (x >= 2)
Φfact^3(０)(x) => 1 (x = 0) <= Φfact(Φfact(Φfact(０)))(x)
1 (x = 1)
2 (x = 2)
undef (x >= 3)
...
Φfact^n(０)(x) => x! (0 <= x < n)
undef (x >= n)Φfact^n(０)は3.1のfactnを展開したものと一致する
半順序 Φfact^0(０) ≦ Φfact^1(０) ≦ ... の上限
Φfact^* => ∨{Φfact^n(０) | n ∈ N}おさらい
半順序関係(以下の3つが成り立つ二項関係)
- 反射律: a ≦ a
- 反対称律: a ≦ b ＆ b ≦ a → a = b
- 推移律: a ≦ b ＆ b ≦ c → a ≦ c
半順序集合: 要素間に反順序関係が定義されている集合
半順序集合Dの部分集合Xにおいて
- 上限∨X: (半順序関係で)最小の上界
- 上界d: ∀x ∈ X (x ≦ d)
d ∈ D だが、d ∈ Xとは限らないΦfact^*(x) => x!よりΦfact(Φfact^*)を展開
Φfact(Φfact^*) => if x = 0 then 1 else x * (x - 1)!
=> if x = 0 then 0! else x!
=> x!
Φfact(Φfact^*) = Φfact^*Φfact^*は、再帰定義の性質を満たしている
このΦfact(f)は、領域(cpo(完備半順序集合)、プログラムが扱う領域のこと) N->N 上の連続関数である
cpo D
- 最小限を持つ
- 任意の有向集合X ⊆ Dについて、Xの上限∨X ∈ Dが存在する
3.2による連続関数の定義
- D, D': cpo
- f: D -> D'
- 任意の有向集合X ⊆ Dについて、{f(x) | x ∈ X}に上限がある
連続関数: f(∨X) = ∨{f(x) | x ∈ X} である関数
(有向集合X: ∀a∈X ∀b∈X ∃c∈X(a ≦ c かつ b≦c)(一般的に、cpo上の連続関数の上限は不動点)
最小不動点定理
定理3.1.1: 最小不動点定理
- D: cpo
- f: D->D の連続関数
のとき
- (1) f(a) = a
- (2) f(b) = b なら a ≦ b
となる a ∈ D が存在する。このaが最小不動点。
a = ∨{f^n(⊥) | n ∈ N}
⊥はD上の最小限証明
- Dはcpoなので最小限⊥が存在する
- fは単調関数(a≦bならf(a)≦f(b)である関数)
⊥ ≦ f(⊥) <- 最小限
f(⊥) ≦ f(f(⊥)) <- 単調関数
f(f(⊥)) ≦ f(f(f(⊥))) <- 単調関数
...
よって
⊥ ≦ f(⊥) ≦ f^2(⊥) ≦ ...
- A = {f^n(⊥) | n = 0, 1, 2, ...}は有向集合であるので、上限∨Aが存在する
(1)∨Aが不動点(f(∨A) = ∨A)であることを示す
- f(∨A) => f(∨{f^n(⊥) | n = 0, 1, 2, ...})
=> ∨{f(f^n(⊥)) | n = 0, 1, 2, ...} <- 連続関数の定義から
=> ∨{f^n(⊥) | n = 1, 2, 3, ...}
=> ∨{f^n(⊥) | n = 0, 1, 2, ...} <- f^0(⊥) = ⊥、上限dは⊥≦dになるので影響しない？
=> ∨A
(2) 任意の不動点f(b) = bについて
-- ⊥ ≦ b
-- n >= 0 で f^n(⊥) ≦ f^n(b) = b (単調関数だから)
--- ∨A ≦ b
最小不動点の意味
Φfact^*はΦfactの最小不動点。Φfact^*はN上の全関数であり、Φfact(f) = fを満たすfはΦfact^* 1つのみ。
しかし、再帰呼び出し形で書かれた関数の意味が一意にならない場合もある。
例
- fact'(x) => if x = 10 then 10! else x * fact'(x - 1)
- Φfact'(f)(x) => if x = 10 then 10! else f(x - 1)
- 0 - 1 => 0
の場合、0 <= x < 10のとき再帰の無限ループになる。
f(x) => undef (0 <= x < 10)
x! (10 <= x)はΦfact'の最小不動点(Φfact'*(undef))であるが、ほかにも存在する
すべての最小不動点gが以下のようにかける(Φfact'(g) = gになる)
g(x) => x!*α (0 <= x < 10)
x! (10 <= x)
α: undefか任意の自然数fはgになる最小のもの(undef ≦ x!*α だから?)。
(プログラム上の厳密な意味定義については、４章で行う)
ループの意味づけ
(ループはEnv->Envの再帰関数)
階乗x!のループ計算
r := 1 while x != 0 do r := r * x; x := x - 1 od
- 環境全体 Env
- 変数集合 Var = {x, r}
- プログラム P : Env -> Env
- 部分関数で表す: P
- 環境φ、ψ
[[P]](φ) => [[r:=1; while x!=0 do r:=r*x; x:=x-1 od]](φ)
=> [[while x!=0 do r:=r*x; x:=x-1 od]](φ(r:=1))
ただし、φ(r:=1) => φ(r:=1)(r) = 1, φ(r:=1)(x) = φ(x)部分関数をさらに展開
[[while x!=0 do r:=r*x; x:=x-1 od]](ψ) => ψ (ψ(x) = 0)
[[while x!=0 do r:=r*x; x:=x-1 od]](ψ') (ψ(x) != 0)
ただし、ψ' = [[r:=r*x; x:=x-1]](ψ)
= ψ(r:=ψ(r)*ψ(x), x:=ψ(x)-1)このwhile文はEnvに対して再帰的に定義されている
(このwhileのような)[Env->Env]な部分関数全体はcpoである
Φ: [Env->Env] -> [Env->Env]
Φ(f)(ψ) => ψ (ψ(x) = 0)
f([[r:r*x; x:=x-1]](ψ)) (ψ(x) != 0)は連続関数であり、最小不動点Φ^*が存在する
Φ^*(f)(ψ) => ψ (ψ(x) = 0)
Φ^*([[r:r*x; x:=x-1]](ψ)) (ψ(x) != 0)が成り立ち、Φの不動点はΦ^*のみ。よって
[[while x != 0 do r:r*x; x:=x-1 od]] = Φ^*
Pは
[[r:=1; while x != 0 do r:r*x; x:=x-1 od]](Φ) = Φ^*(φ(r:=1))
fact'とループの二例では[N->N]、[Env->Env]を扱ったが、平坦cpo(a≦b => a = ⊥ または a = b)な[N⊥->N⊥]、[Env⊥->Env⊥]でも同じ議論ができ、より統一的になる。(4章はこちらを用いる)
練習3.3
どうとけばいいものだろうか
1.
- cpo D
- 連続関数 f: D->D
- a ∈ D
a ≦ f(a) ならば、 a以上のfの不動点のうち最小ものが存在する、ことを示せ
a ≦ f(a) ≦ f^2(a) ≦ ...
A = {f^n(a)|n ∈N}の上限∨Aがあり、fの不動点のひとつ(f(∨A) = ∨A)
最小不動点dは d≦∨A
??
2.
- cpo D
- 連続関数 f: D->D
- fの不動点全体 F
F∪{⊥}は[D->D]の半順序に関してcpoになる、ことを示せ
cpoであることを示すには有向部分集合に上限が存在すること。 最小不動点が上限??
3.
- cpo D
- 連続関数 f: D->D
- a ∈ D
f(a) ≦ aならば、fの最小不動点はa以下である、ことを示せ
... ≦ f^2(a) ≦ f(a) ≦ a
A={f^n(a)|n∈N}とし、下限を∧Aは不動点f(∧A) = ∧A
よって、最小不動点d ≦ ∧A (最小不動点定理より)。
よってd≦a
4.
- Φ: [N->N]->[N->N]
- Φ(f)(x) => if x > 100 then x - 10 else f(f(x+11))
Φの最小不動点は
- f91 => if x > 100 then x - 10 else 91
と一致することを示せ(MacCarthyの91関数)
(ヒント) 3の結果を使って、∨{Φ^n(⊥) | n = 0, 1, 2, ...} ≦ f91 を示す
Φ^1はx>100 Φ^2はx>100, x=100 Φ^3はx>100, x=100, x=99 までは展開したけど... Φ(f91) ≦ f91を示せってことのようだ Φ(f91) => if x > 100 then x - 10 else f91(if x > 89 then x + 1 else 91) => if x > 100 then x - 10 else f91(if 91 < x <= 100 then x + 1 else 91) => if x > 100 then x - 10 else if (if 91 < x <= 100 then x + 1 else 91) > 100 then (if 91 < x <= 100 then x + 1 else 91) - 10 else 91 => if x > 100 then x - 10 else if x = 100 then (x + 1) - 10 else 91 => if x > 100 then x - 10 else 91 => f91 つまりΦ(f91) = f91、Φ(f91) ≦ f91かつ f91 ≦ Φ(f91) 最小不動点をdとすると、 d ≦ f91 (3の結果より)かつ、f91≦d (最小不動点定理より)よって d = f91
補足: 不動点意味論の直感的イメージ
実のところ、この本では、「数学的な関数」を前提知識としてもっていることを全体にわたり要求している。一方で現在では、プログラムを理解するのに数学の基礎知識を必要とせずにすむことができる。
そのため、数学の知識がなかったり、(プログラムの関数を数学と区別していたりして)それを意識していなかったりする場合だと、直感的にはわかりにくいものになってしまっている。そこで以下、直感的につなげられるような概念を間において補足する。
関数≒map
まず、一般化すると、関数とは入出力のペアの集合である。たとえば、f(x) = 1/xというような公式であらわしたりするけど、この関数はf = [...,(1, 1), (2, 1/2), (3, 1/3), ...]というmapとみなすこともできる。数学の性質のようなものについて学習する場合は、往々にして関数は単に「ペアの集合」として認識してたほうが、理解しやすいのではないかと思う。
全関数とは、たとえば、引数が整数ならペアの左側は全整数があるmapのことである。部分関数は、ペアの左側には全整数が入ってない(いいかえるといくつかの整数が欠けている)mapのことである。
(数学としての「関数」は基本的に全関数のことである。一方プログラム言語での多くの「関数」は部分関数として定義される場合が多い。たとえば、引数はintなのに負の数を渡すとIndexErrorを出してしまう関数など)
不動点
「関数fの不動点」とは、x = f(x)となるxのこと。上のfならx=1のときf(x)=1なでの、x=1は不動点になる。このようにこの概念は関数が公式表現だろうがmap表現だろうが差はない。
xが整数でなく、実数だろうが、集合だろうが、関数(≒map＝ペア集合)だろうが、同値性判定ができる以上、x = f(x)とうなるようなxのことをfの不動点という。
最大不動点、最小不動点
最小とか最大とは、要素間に(半)順序関係での大小がついた集合があって、その中で最も小さいものと最も大きいもののこと。
ある関数fの最小不動点とか最大不動点というものは、fの不動点が複数あった場合、それらfの不動点だけを要素にもつ集合があるとみなして、その中で最小のものや最大のものを指す。
(一般的に半順序関係の場合、各不動点のみでの間で、最大最小がつけられなければ、そういう場合は最大/最小不動点は存在しない、といえるけれど)。
たとえば、上のf(x)=1/xに相当するfであれば、xを最小のx=-∞からどんどん増やしていって、x=-1のときf(x)=-1となって初めて不動点が見つかる。このx=-1は最小不動点といえる。一方、xを最大のx=∞から、どんどん減らしていって、x=1のときf(x)=1となり、初めて不動点が見つかる。このx=1は最大不動点といえる。
このように最小の値があって、そこからどんどん増やしていけて、はじめてみつかった不動点のことを、最小不動点ということもできる。逆に最大の値があって、そこからどんどん減らしていけて、はじめてみつかった不動点のことを、最大不動点ということもできる。
こういう風にして見つけるようなものを、絶対的な性質となるように語りなおしているのが本文の内容だったりする。
(不動点関数についてでは、不動点を求める関数の引数は関数であり、その最大値つまり世の中に存在する関数全体を集合にしたものから、どんどんその要素である関数を減らす、というようなことは難しいので最大不動点はほとんど扱わない。しかし、一般的な集合、特に有限集合を引数戻り値にとる関数では、その不動点については、最大最小を両方扱うことも多い).
不動点関数
「Yの不動点関数」とは、関数を引数にとる関数Yの不動点のこと。
この不動点関数とは、関数を引数にとるあるYについて、f=Y(f)となるfのこと。
そして、このfを不動点関数という。
fは部分関数、つまりは入出力のペアの集合である、とも言える。そしてその半順序関係は、この集合の半順序関係に基づいている。つまり、その関数が、ある関数があらわすペア集合を含んでいるペア集合であれば、「より大きい」関数である、といえる。
つまり、階乗を表す関数は
- nil = []
- fact0 = [(0, 1)]
- fact1 = [(0, 1), (1, 1)]
- fact2 = [(0, 1), (1, 1), (2, 2)]
- fact3 = [(0, 1), (1, 1), (2, 2), (3, 6)]
- ...
と無数にあってfact1 ＜ fact2 ＜ fact3 ＜ ... である。
この順番に沿って、階乗を生成する関数を生成する関数FACTがあるとする。
この関数FACTは以下のようになる:
- fact0 = FACT(nil)
- fact1 = FACT(fact0)
- fact2 = FACT(fact1)
- fact3 = FACT(fact2)
- ...
つまり
- FACT = [(nil, fact0), (fact0, fact1), (fact1, fact2), (fact2, fact3), ...]
である。
このFACTの不動点は、fact = FACT(fact)となる関数factのことである。
つまり[(0, 1), (1, 1), (2, 2), (3, 6), ...]のペア集合を、FACTでどんどん増やしていったとき、「これ以上増えていかない」もの(fact)がある、ということである。
- FACT = [(nil, fact0), (fact0, fact1), (fact1, fact2), (fact2, fact3), ..., (fact, fact)]
そしてそのfactこそが不動点関数であり、nilからどんどん増やしていってはじめて見つかった不動点になっているため、最小の不動点関数というものになる。
