圏論勉強会
第9回

@ワークスアプリケーションズ

中村晃一
2013年7月11日

謝辞

この勉強会の企画,会場設備の提供をして頂きました
㈱ ワークスアプリケーションズ様
にこの場をお借りして御礼申し上げます。

この会について

  • 圏論(category theory)を題材にいろんなことを学びます。
  • 分かり易さを重視して初歩的な例を多用します。
  • 関数型言語の経験がある方がより楽しめると思います。資料中では主にHaskellを使います。
  • 中高生も数人見ているらしいのでプログラミングと関係が浅い内容も取り上げます。
  • この資料はhttp://nineties.github.com/category-seminarに置いてあります。

第9回

領域理論・不動点意味論

第9回の内容

今回は「領域理論」及び「不動点意味論」というプログラム意味論の重要な分野について紹介します。

本日の内容はとても2時間で扱いきれる様な物ではありませんので,初歩的な(しかし重要な)事柄のみを扱います。web上で得られる詳しい資料としては

などがあります。

プログラム意味論とは

プログラム意味論とは

プログラミング言語の意味を数学的に探求する理論計算機科学の分野を意味論(semantics)と言います。

  • 表示的意味論
  • 操作的意味論
  • 公理的意味論

などの手法が存在します。

表示的意味論とは

表示的意味論(denotational semantics)では,データ・プログラムを集合や関数などの数学的対象(表示(denotation))に対応させる事によって意味を表現する手法を用います。

問:以下で定義された$\mathrm{fact}$の意味は?(引数は自然数とする)

$$\mathrm{fact}(n) = \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*\mathrm{fact}(n-1)$$

表示的意味論では(例えば)関数 $$ \mathrm{fact}(n) = n! \qquad (n\in\mathbb{N})$$ によって$\mathrm{fact}$の意味を表現します。

操作的意味論とは

操作的意味論(operational semantics)では,状態遷移系(数学的に形式化されたインタプリタ)を定義し, プログラムの1ステップの実行を状態遷移系への作用として記述する手法を用います。

問:以下で定義された$\mathrm{fact}$の意味は?(引数は自然数とする)

$$\mathrm{fact}(n) = \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*\mathrm{fact}(n-1)$$

例えば,項書換え系という状態遷移系を用いると$\mathrm{fact}(5)$の評価は $$ \begin{aligned} \mathrm{fact}(5) &\rightarrow \mathrm{if}\ 5 = 0\ \mathrm{then}\ 1\ \mathrm{else}\ 5*\mathrm{fact}(5-1) \\ &\rightarrow 5*\mathrm{fact}(4) \\ &\rightarrow 5*(\mathrm{if}\ 4 = 0\ \mathrm{then}\ 1\ \mathrm{else}\ 4*\mathrm{fact}(4-1))\\ &\rightarrow \cdots \end{aligned} $$ の様に進みます。このような意味の与え方が操作的意味論の手法です。

公理的意味論とは

公理的意味論(axiomatic semantics)では,公理と推論規則を定義する事によってプログラムの意味を記述する手法を用います。

問:以下で定義された$\mathrm{fact}$の意味は?(引数は自然数とする)

$$\mathrm{fact}(n) = \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*\mathrm{fact}(n-1)$$

このプログラムに関して例えば以下の様な推論が行えます。

  • $n = 0$の時にプログラム$x = f(n)$を実行すると$x = 1$となる。

こういった推論を厳密に行う為の規則を与える事によって,プログラムの意味を記述するのが公理的意味論の手法です。

手続き型言語の公理・推論規則の体系であるホーア論理(Hoare Logic)が有名です。

このようにプログラムへの意味の与え方には様々な方法があります。 今回紹介する「領域理論」「不動点意味論」は表示的意味論分野の理論となります。

領域理論

表示的意味論の土台が領域理論(domain theory)です。

表示的意味論は何らかの数学的対象の上に構築されますが,集合と(全域的)関数ではプログラムの意味を上手く表示出来ない事が判り デイナ・スコット(Dana Scott)などによって領域の研究が始められました。

領域理論の要点

領域理論では以下の事が主張されます。

  • 計算の領域は最小値を持つ完備半順序集合である。
  • 計算を表示する関数は連続関数である。

どのような意味か気になると思いますが,まずはいくつか定義と定理の確認を行います。

cpo

計算が行われる「領域」の定義です。

始対象を持ち$\omega$余完備な半順序集合を単に完備半順序集合(complete partial order)と呼び,cpoと表記する。

先ほどの圏論的な定義を翻訳すると以下のようになります。

完備半順序集合cpoとは半順序集合$(D,\leqq)$であり,

  • 最小値$0$を持つ。(自然数の$0$ではなく,始対象の$0$です。)
  • 任意の$\omega$-chain $$ x_0\leqq x_1\leqq x_2 \leqq x_3 \leqq \cdots $$ に対して上限$\displaystyle\lim_{\rightarrow}x_i$が存在する。すなわち, $$ \begin{aligned} & \text{任意の$i \in\omega$について} x_i \leqq \lim_{\rightarrow}x_i \\ & \text{任意の$i \in\omega$について} x_i \leqq x\ \text{ならば}\ \lim_{\rightarrow}x_i \leqq x \end{aligned} $$ を満たす。

連続関数

cpo $A$からcpo $B$への$\omega$余連続な函手$F$を単に連続関数(continuous function)と呼び,$F:A\rightarrow B$と表す。

これも翻訳すると以下のようになります。

cpo間の連続関数$F: A\rightarrow B$とは以下の条件を満たすものである。

  • $\displaystyle a\leqq b\ \Rightarrow\ F(a)\leqq F(b)$
  • $\displaystyle F(\lim_{\rightarrow}x_i) = \lim_{\rightarrow}F(x_i) $

これから判るように、ここで単に「連続関数」と呼んでいるものは「単調な連続関数」の事です。

最小不動点定理

完備半順序集合と連続関数を用いる事の恩恵として以下の定理が得られます。

$D$をcpo,$F: D\rightarrow D$を連続関数とすると, $$ \color{red}{x = F(x)} $$ を満たす$x\in D$が必ず存在し,その最小の値$\theta$は $$ \color{red}{\theta = \lim_{\rightarrow} F^i(0)} = \lim_{\rightarrow} F(F(\cdots F(0)\cdots)) $$ で与えられる。

一般に関数$f$に対して$x = f(x)$を満たす$x$を$f$の不動点(fixed point)と言います。

【証明:不動点であること】
$D$をcpo,$F:D\rightarrow D$を連続関数とする。
$0$は始対象であるから $$ 0 \leqq F(0) $$ が成り立つ。さらに$F$は単調であるからこの不等式より $$ F(0) \leqq F^2(0) $$ が得られる。これを繰り返して$\omega$-chain $$ 0 \leqq F(0) \leqq F^2(0) \leqq F^3(0) \leqq \cdots \quad\cdots (1) $$ を得る。すると$D$はcpoなので $$ \lim_{\rightarrow} F^i(0) $$ が存在する。従って$F$は連続であるから $$ F(\lim_{\rightarrow}F^i(0)) = \lim_{\rightarrow}F(F^i(0)) = \lim_{\rightarrow}F^{i+1}(0) = \lim_{\rightarrow}F^i(0) $$ となる。(最後の変形は,$\omega$-chain $\{F^{i+1}(0)\}$の先頭に$0\leqq F(0)$を繋げたものは$(1)$と一致する為。)
従って$\displaystyle\lim_{\rightarrow}F^i(0)$は$F$の不動点である。

【証明続き:最小の不動点であること】
$F$の不動点$x = F(x)$が他に存在したと仮定すると,$0$は始対象であるから $$ 0 \leqq x $$ が成り立ち,さらに$F$は単調であるから $$ F(0) \leqq F(x) = x$$ が成り立つ。これを繰り返して任意の$i\in\omega$に対して $$ F^i(0) \leqq x$$ が得られる。すると余極限$\displaystyle\lim_{\rightarrow}F^i(0)$の性質より $$ \lim_{\rightarrow}F^i(0) \leqq x $$ となる。従って$\displaystyle\lim_{\rightarrow}F^i(0)$は$F$の最小の不動点である。

最小不動点定理の重要性

不動点再帰と密接に関わります。最小不動点定理が重要であるのは,最小不動点の存在だけでなく,その具体的な構成方法を与えるからです。

「$X$は$F$の最小不動点である」という形で$X$について述べる事が出来れば

  • $X$を具体的に構成してしまう
  • 最小不動点の性質に基づいて,$X$の性質を検証する

といった事が可能になります。

何故cpoを考えるのか?

まず,$n$は自然数であるとして以下のコードの表示を考えてみて下さい。

$$ f(n) = \mathrm{if}\ n < 10\ \mathrm{then}\ 0\ \mathrm{else}\ f(n+1) $$

$n \geqq 10$の時,$f(n)$を評価しても値は得られないので $$ f(n) = \left\{\begin{array}{cc} 0 & \text{($n<10$のとき)} \\ \text{値なし} & \text{($n\geqq 10$のとき)} \end{array}\right. $$ の様になります。このように定義域の一部でしか定義されない関数を部分関数(partial function)と言います。プログラムの意味論では部分関数を適切に表現する必要があります。

ボトム

部分関数を表現する為に,ボトム(bottom)と呼ばれる「値なし」の状況を表現する為の値をデータ領域に追加します。 これは記号$\color{red}{\bot}$で表されます。

集合$A = \{a,b,c,\cdots\}$に$\bot$を追加した集合を

$$ A_{\bot} = \{\bot,a,b,c,\cdots\} $$

と表す事にします。

例えば,先ほどの関数$f$は$f: \mathbb{N}_{\bot} \rightarrow \mathbb{N}_{\bot}$というドメイン・コドメインを持つ関数として表す事が出来ます。

部分オブジェクト

次に,cpo $A$と$B$の直積 $$ A\times B = \{(a,b) | a\in A, b\in B\} $$ を考えると,一部だけが定義された状態のデータが生じます。

例えば領域$\mathbb{N}_{\bot} \times\mathbb{N}_{\bot}$には $$ (\bot, \bot),\ (1, \bot),\ (\bot, 0),\ (1, 2),\cdots $$ などのデータが含まれる事になります。

この意味で領域の値を部分オブジェクト(partial object)などとも呼びます。

部分オブジェクトという概念が登場しましたが,これにcpoの構造を自然に入れる事が出来ます。

部分オブジェクトの順序

まず$ A_{\bot} = \{\bot,a,b,c,\cdots \}$の各要素には

$$ a \leqq b \ \mathrm{iff}\ a = \bot\ \text{または}\ a = b$$

によって順序を入れます。この形の領域を平坦なcpo(flat cpo)とも呼ばれます。

例えば$\mathbb{N}_{\bot}$の様子は下図の様になります。

部分オブジェクトの順序

対$(a,b)$には

$$ (a_1,b_1) \leqq (a_2, b_2) \ \mathrm{iff}\ a_1\leqq a_2\text{かつ}b_1\leqq b_2$$

によって順序を入れます。

例えば$\mathbb{N}_{\bot}\times\mathbb{N}_{\bot}$の様子は下図の様になります。

部分オブジェクトの順序

さらに関数自体もデータの一種ですが,これにも半順序構造が入ります。 関数$f, g: A\rightarrow B$間の順序は

$$ g\leqq f\ \mathrm{iff}\ \text{全ての$x\in A$について}g(x)\leqq f(x) $$

によって順序を入れます。

例えば$f,g:\mathbb{N}_{\bot}\rightarrow\mathbb{N}_{\bot}$を $$ \begin{align} f(n) & = 0 \\ g(n) & = \mathrm{if}\ n < 10\ \mathrm{then}\ 0\ \mathrm{else}\ g(n+1) \end{align} $$ と定義した場合$g\leqq f$となります。

cpoに関する定理

cpoの構成に関しては以下のような定理が成り立ちます。

  • $A,B$がcpoならば$A\times B$もcpo
  • cpo $A,B$に対し$[A\rightarrow B]$を$A$から$B$への連続関数の集合とすると$[A\rightarrow B]$もcpoである。

時間の関係上証明は省略しますが $$\begin{aligned} & \bot_{A\times B} = (\bot_{A},\bot_{B}),\ \lim_{\rightarrow}(a_i,b_i) = (\lim_{\rightarrow}a_i,\lim_{\rightarrow}b_i) \\ & \bot_{[A\rightarrow B]} = \text{(常に$\bot_{B}$を返す関数)},\ (\lim_{\rightarrow}f_i)(x) = \lim_{\rightarrow}f_i(x) \end{aligned}$$ とすれば良いです。但しcpo $D$の最小値を$\bot_{D}$と表しています。

順序関係の直感的な解釈

部分オブジェクト$a$,$b$が $$ a \leqq b$$ の関係であるという状況は

  • $b$は$a$より良く定義されている。
  • $b$は$a$より詳しい情報を持っている。

などと解釈する事が出来ます。

cpoの直感的な解釈

今の考え方に基づくと,計算の領域としてcpoを用いる事が自然だと思えるのではないでしょうか。

  • 最小値$\bot$は「何も情報がない状態」を表している。
  • $\omega$-chain $$ x_0\leqq x_1\leqq x_2\leqq \cdots $$ は情報量が向上していく($\bot$の部分が減っていく)ようなデータの列に対応する。
  • $\omega$余完備であるということは,この列の全ての情報を含む,最小のデータが存在する事を表す。

単調関数の直感的な解釈

続いて関数$f: A\rightarrow B$が単調であるとは

$$ a \leqq b\ \Rightarrow\ f(a)\leqq f(b) $$

が成り立つ事でした。

この条件は「入力の情報量を増やしたら,出力の情報量も増える」という事だと解釈出来ます。

再帰関数の不動点意味論

例として再帰関数

$$\mathrm{fact}(n) = \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*\mathrm{fact}(n-1)$$

を用います。

$\lambda$記法を用いるとこれは

$$\mathrm{fact} = \lambda n. \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*\mathrm{fact}(n-1)$$

とも表せます。

右辺の$\mathrm{fact}$をさらに引数に持ち上げると

$$\mathrm{fact} = (\lambda f. \lambda n. \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*f(n-1))(\mathrm{fact})$$

となります。

つまり,

$$ F(f) = \lambda n. \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*f(n-1)$$

と置くと $$ \mathrm{fact} = F(\mathrm{fact}) $$ と表されるので,

「$\mathrm{fact}$は$F$の不動点である。」

と述べる事が出来ます。

再帰関数と不動点

このようにある再帰関数の表示$f$は適当な関数$F$を用いて

「$f$は$F$の不動点である」

という形で表現する事が出来ます。

最小不動点=ノイズが最小の不動点

$F$の不動点は複数存在し得ますが,最小不動点$f$は $$ g = F(g) $$ を満たすような$g$の中で情報量が最小の関数であると直感的に説明する事が出来ます。

$$ f(n) = \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ f(n+1) $$

という関数を考えます。先ほどと同様にするとこれは

$$ F(f) = \lambda n. \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ f(n+1)$$

の不動点という事になります。

ここで$c\in\mathbb{N}_{\bot}$を任意の定数として $$ f(n) = \mathrm{if}\ n=0\ \mathrm{then}\ 1\ \mathrm{else}\ c$$ という関数を考えると $$ f = F(f) $$ が成り立つ(練習問題)ので不動点となりますが,例えば$c = 100$にした

$$ f(n) = \mathrm{if}\ n=0\ \mathrm{then}\ 1\ \mathrm{else}\ 100 $$

には元のプログラムに無い情報が含まれてしまっています。これでは適切な表示だと言えないでしょう。

不動点意味論

そこで再帰プログラムの表示$f$を

「$f$は$F$の最小不動点である」

という形式で与える事にします。このような意味論を不動点意味論(fixed point semantics)と言います。

さらに,領域としてcpoを取り,$F$が連続であるならば最小不動点定理によって

$$ f = \lim_{\rightarrow}F^i(\bot)$$

である事が得られます。

$$ F(f) = \lambda n. \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*f(n-1)$$ の最小不動点$\displaystyle f = \lim_{\rightarrow}F^i(\bot)$を調べます。

まず $$F(\bot) = \lambda n.\mathrm{if}\ n=0\ \mathrm{then}\ 1\ \mathrm{else}\ \bot$$ となります。(乗算は$n*\bot = \bot$のように評価されます。)

すると $$\begin{aligned} F^2(\bot) &= \lambda n. \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*F(\bot)(n-1)\\ &= \lambda n. \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*(\mathrm{if}\ n-1=0\ \mathrm{then}\ 1\ \mathrm{else}\ \bot) \\ &= \lambda n. \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ n*(\mathrm{if}\ n=1\ \mathrm{then}\ 1\ \mathrm{else}\ \bot) \\ &= \lambda n. \mathrm{if}\ n = 0\ \mathrm{then}\ 1\ \mathrm{else}\ (\mathrm{if}\ n=1\ \mathrm{then}\ 1*1\ \mathrm{else}\ \bot) \\ &= \lambda n. \mathrm{if}\ n < 2\ \mathrm{then}\ n!\ \mathrm{else}\ \bot\\ \end{aligned} $$ となります。

例(続き)

以下同様にすると $$ F^i(\bot) = \lambda n. \mathrm{if}\ n < i\ \mathrm{then}\ n!\ \mathrm{else}\ \bot$$ が得られます。つまり$ F^i(\bot) $は$i$未満の自然数$n$については$n!$を返す関数です。

すると任意の$i$について $$ F^i(\bot) \leqq f $$ を満たすような$f$は $$ f = \lambda n. n! $$ しか無いのでこれが最小不動点となります。

例2

今の例では,最小不動点を用いるありがたみが解りにくいと思いますので,有名な例をもう一つ紹介します。

マッカーシーの91関数 $$ f(n) = \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ f(f(n+11))$$

この$f$が一体どのような部分関数によって表示されるのか,パッと見ではよく分かりません。 しかし,以下の$F$の最小不動点を計算するだけで自動的に求めてしまうことが出来ます。 $$ F(f) = \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ f(f(n+11))$$

例2(続き)

順番に計算してみると $$\begin{aligned} F(\bot) &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ \bot \\ F^2(\bot) &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ F(\bot)(F(\bot)(n+11)) \\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ F(\bot)(\mathrm{if}\ n+11 > 100\ \mathrm{then}\ n+11-10\ \mathrm{else}\ \bot) \\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ F(\bot)(\mathrm{if}\ n > 89\ \mathrm{then}\ n+1\ \mathrm{else}\ \bot) \\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ (\mathrm{if}\ n > 89\ \mathrm{then}\ F(\bot)(n+1)\ \mathrm{else}\ \bot) \\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ (\mathrm{if}\ n > 89\ \mathrm{then}\ (\mathrm{if}\ n>99\ \mathrm{then}\ n-9\ \mathrm{else}\ \bot)\ \mathrm{else}\ \bot) \\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ (\mathrm{if}\ n > 89\ \mathrm{then}\ (\mathrm{if}\ n>99\ \mathrm{then}\ n-9\ \mathrm{else}\ \bot)\ \mathrm{else}\ \bot) \\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ (\mathrm{if}\ n =100 \ \mathrm{then}\ 91 \ \mathrm{else}\ \bot) \end{aligned} $$ となります。$n-9$に辿り着くのは$n=100$の時のみである事に注意して下さい。

例2(続き)

同様に計算を進めると $$ F^i(\bot) = \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ (\mathrm{if}\ 100\leqq n < 99+i\ \mathrm{then}\ 91\ \mathrm{else}\ \bot)$$ が得られます。

従ってこの極限が最小不動点ですので,マッカーシーの91関数は

$$ f(n) = \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ 91 $$

という関数である事が判りました。

Haskellを使った説明


import Data.Function

-- 実際に動くコードで最小不動点のアイデアを理解しましょう。
-- fact(n) = n!の例を使います。

-- 以下のfactFの最小不動点がfactです。
factF :: (Integer -> Integer) -> (Integer -> Integer)
factF f = \n -> if n == 0 then 1 else n*f(n-1)

-- すると以下のような関数の列が出来ます。
-- factNはN未満の自然数nについては正しくn!を返し,N以上の自然数についてはundefinedを返します。
fact0 = undefined
fact1 = factF undefined
fact2 = factF (factF undefined)
fact3 = factF (factF (factF undefined))
fact4 = factF (factF (factF (factF undefined)))
fact5 = factF (factF (factF (factF (factF undefined))))

-- 求める関数factはこの列の極限です。
-- Haskellの標準ライブラリには最小不動点を求める為の関数fixが用意されており
-- 以下の様にfactを得る事が出来ます。
fact = fix factF

不動点帰納法

数列 $$ \bot,F(\bot),F^2(\bot),F^3(\bot),\cdots,F^i(\bot),\cdots $$ の極限として最小不動点 $$ \lim_{\rightarrow}F^i(\bot) $$ が与えられるわけですが,この構造に基づいて帰納的に最小不動点の性質について証明を行う事が出来ます。

不動点帰納法で利用できる命題

cpo $D$の値を引数にとる命題$P(x)$が以下の条件を満たすとします。

任意の$\omega$-chain $$x_0 \leqq x_1 \leqq x_2 \leqq \cdots $$ について $$ P(x_0),P(x_1),\cdots\text{の全てが真ならば} P(\lim_{\rightarrow}x_i)\text{も真} $$

このような$P(x)$を許容的(admissible)などと呼びます。

不動点帰納法

$F: D\rightarrow D$をcpo $D$上の連続関数とし,$P(x)$を$D$上の許容的な述語とした時

  • $P(\bot)$が真
  • 任意の$f\in D$について,$P(f)$が真ならば$P(F(f))$も真

が成り立つならば,$\displaystyle P(\lim_{\rightarrow}F^i(\bot))$も真である。

このような不動点の構成に基づく帰納法を不動点帰納法と言います。

先ほどのマッカーシーの91関数に関する簡単な命題を証明してみます。

$ F:[\mathbb{N}_{\bot}\rightarrow\mathbb{N}_{\bot}]\rightarrow [\mathbb{N}_{\bot}\rightarrow\mathbb{N}_{\bot}]$を $$ F(f) = \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ f(f(n+11))$$ と定義し,$F$の最小不動点を$f$とする。
ここで$g:\mathbb{N}_{\bot}\rightarrow\mathbb{N}_{\bot}$を $$ g(n) = \mathrm{if}\ n>100\ \mathrm{then}\ n-10\ \mathrm{else}\ 91 $$ (但し$g(\bot) = \bot$)と定義すると $$ f \leqq g $$ である事を示せ。

$f\leqq g$が真であるということは($\mathbb{N}_{\bot}$が平坦なcpoなので) $$ f(n) \neq \bot \ \text{ならば} f(n) = g(n) $$ という事を意味します。

【証明】
$\bot \leqq g$である事は明らか。
$h:\mathbb{N}_{\bot}\rightarrow\mathbb{N}_{\bot}$が$h\leqq g$を満たすと仮定すると $$ \begin{aligned} F(h) &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ h(h(n+11))\\ &\leqq \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ g(g(n+11))\\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ g(\mathrm{if}\ n>89\ \mathrm{then}\ n+1\ \mathrm{else}\ 91) \\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ (\mathrm{if}\ n>89\ \mathrm{then}\ g(n+1)\ \mathrm{else}\ 91) \\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\\ &\qquad (\mathrm{if}\ n>89\ \mathrm{then}\ (\mathrm{if}\ n>99\ \mathrm{then}\ n-9\ \mathrm{else}\ 91)\ \mathrm{else}\ 91) \\ &= \lambda n. \mathrm{if}\ n > 100\ \mathrm{then}\ n-10\ \mathrm{else}\ 91 \\ &= g \end{aligned} $$ より$F(h)\leqq g$である。従って不動点帰納法により $$ \lim_{\rightarrow}F^i(\bot) \leqq g$$ である。

第9回はここで終わります

お疲れ様でした。
領域理論、不動点意味論に思いの外時間がかかってしまったので,始代数・終余代数と不動点の関係,プログラム運算の続きは来週に回します。