Haskell/Denotational semantics

導入

この章ではHaskellプログラムの意味がどのように形式化されるかという表示的意味論(denotational semantics)を説明します。「square x = x*x というプログラムの意味は、数をその平方数に写す数学の平方関数だ」ということを形式的に規定することはつまらないことにみえるかもしれませんが、それでは f x = f (x+1) のような無限ループするプログラムの意味はどうでしょうか？ 以下ではまずこの疑問に対するScottとStracheyのアプローチを例示し、概して関数プログラムの、特に再帰的な定義の正しさについて論じる基盤を得ることにしましょう。もちろん、これらのトピックではHaskellプログラムを理解するために必要なものに集中します。

この章の他の狙いは、ある関数がその引数を評価する必要があるかどうかというアイディアを捉えた正格と遅延の概念を説明することです。 興味深いことに、これらの概念は実行モデルを参照する必要なく、表示的意味論のみで簡明に定式化することができます。これらは、グラフ簡約でも利用されています。しかし、この章では表示的な定義と⊥ ("Bottom")のような関連する概念に慣れていきましょう。正格性に興味がある読者は、#ボトムと部分関数と#正格と非正格の意味のセクションを見てください。

表示的意味論って？何のためにあるの？

Haskellプログラムは何を意味するでしょうか？ この質問はHaskellの表示的意味論によって答えることが出来ます。一般的にプログラミング言語の表示的意味論はプログラムをそれぞれプログラムの「意味」を表す対応する数学的対象 (denotation : 表示) へ写します。例を挙げると、Haskellプログラム10、 9+1、 2*5 そしてsum [1..4]に対応する数学的対象は、整数10と表現できます。このとき、これらのプログラムは整数10を表示(denote)すると言います。プログラムに対応する数学的対象の集まりは意味領域(semantic domain)と呼ばれます。

プログラムコードから意味領域への写像は、通例、プログラムコードの周りに二重の四角いブラケット(Oxford brackets)で書かれます。例えば、

$[\![{\texttt {2*5}}]\!]=10.$

表示は合成的、すなわち、1+9のようなプログラムの意味は、その成分の意味にのみ依存します。

$[\![{\texttt {a+b}}]\!]=[\![{\texttt {a}}]\!]+[\![{\texttt {b}}]\!].$

同じ表記が、型にも使われます。すなわち、

$[\![{\texttt {Integer}}]\!]=\mathbb {Z} .$

しかし説明を簡単にするため、後の章ではこれらの式を意味対象と暗黙に同一視し、区別を明確にする必要がある場合に限り、この表記法を使うことにします。

Haskellのような純粋関数型言語の、一つのキーとなる性質は、「1+9 は 10 を表示する」のような数学の直接的な解釈がそのまま関数にも引き継がれることです。本質的には、 Integer -> Integer 型のプログラムは、整数間の数学的な関数$\mathbb {Z} \to \mathbb {Z}$を表示します。この式も非停止性を含めるために一般に修正が要るのですが、命令型言語の場合の状況はより悪いです。その型を持つ手続きは、機械の状態をひょっとしたら意図しない方法で変更するような何かを表示します。命令型言語はその言語を機械で実行する方法の記述である操作的意味論に密接に関連しています。 命令型プログラムの表示的意味論を定義し、そのようなプログラムに使用して論じることは可能ですが、そうして定義した意味はしばしば操作的な性質を持っていて、時には関数型言語のための表示的意味論よりも拡張する必要があります。

対照的に、純粋関数型言語の意味はデフォルトで実行の方法から完全に独立しています。 Haskell98の言語仕様でさえ、Haskellの非正格な表示的意味論だけで規定されており、実装方法については規定されていません。

意味領域として何を選ぶか？

それぞれのHaskellプログラムの適切な数学的対象を探ってみることにしましょう。 例として 10, 2*5 と sum [1..4] の場合、これら全ての式は明確に整数10を表示するでしょう。 一般化すると、任意のInteger型の値 x は集合 $\mathbb {Z}$ の元であるようです。 同じ事は、Bool 型でも行うことができます。 f :: Integer -> Integer のような関数は、(引数、値)の組の集合として「関数」を数学的に定義することができ、これは一種のグラフ (graph)です。

しかし、関数をただグラフだ、と解釈するのは早計です。なぜなら、それは再帰的な定義では上手くいかないからです。以下の定義について考えてみます。

shaves :: Integer -> Integer -> Bool
1 `shaves` 1 = True
2 `shaves` 2 = False
0 `shaves` x = not (x `shaves` x)
_ `shaves` _ = False

このコードを 「0、1、2 は長い髭の男性とします。誰が誰の髭を剃っているでしょうか？」 という問題だと考えてみましょう。1の人物は彼自身で、しかし2 の髭は床屋である 0が剃っています。なぜなら 3番目の等式により 0 `shaves` 2 == True だからです。一般に、3行目が言っているのは、「床屋 0 は自分自身ではひげを剃らない、全ての人のひげを剃る」ということです。

では床屋 0 彼自身についてはどうでしょう？ 0 `shaves` 0 は True と False どちらでしょうか？ もし、この式がTrueだとすると、3行目の等式はFalseであり、Falseであるなら3行目の等式はTrueだと言っています。わけがわかりませんが、私たちは単に「0 `shaves` 0 はTrue、またはFalseである」と言うことはできないということだけはわかります。

グラフを用いて関数 shaves を解釈するには、空の点が絶対に必要です。私たちは、いくつかの引数で値が定義されていない 部分関数 (partial functions) を意味対象に組み込めなければなりません。

しかも、この有名な例では集合論の根幹に関わる重大な問題を引き起こしました。これは定義の中でそれ自身を定義に使っていて、論理が循環している非叙述的(impredicative)な定義の例です。残念なことに、再帰的な定義では循環は「問題」ではなく「特徴」です。

ボトムと部分関数

⊥ ボトム(Bottom)

部分関数を定義するために、ボトム (bottom) と名付けられた特殊な値「⊥」を導入します（これはASCIIコードで_|_とも書かれます）。私たちは⊥を完全に未定義の値もしくは未定義の関数と言います。 Integer や () のような基本的なそれぞれのデータ型は、通常の要素に加えて⊥を含んでいます。つまり、 Integer 型が取り得る値は、

$\bot ,0,\pm 1,\pm 2,\pm 3,\dots$

のようになります。値の集合に⊥を追加することを 持ち上げ (lifting)と呼びます。これは、しばしば $\mathbb {Z} _{\bot }$ のように添え字で示されます。これは数学的な集合「持ち上げられた整数」の正しい表記ですが、私たちは「Integer 型の値」のように話すことを好みます。これは、$\mathbb {Z} _{\bot }$ という表示は他に「真の」整数 $\mathbb {Z}$ が存在することを示唆しますが、Haskellでは整数といえば型 Integer のことを指すからです。

他の例として、 () 型はただ一つの要素しかないように思えますが、実際には二つの要素が属しています。

$\bot ,()$

今のところ、私たちは Integer 型だけでのプログラミングに留まります。正格、非正格な言語で⊥を含んだ任意の代数的データ型がどのように発散するかは、セクション代数的データ型で扱われています。

Haskellでは、式 undefined は⊥を表示します。この助けを借りて、実際のHaskellプログラムのいくつかの意味的性質を確認することが出来ます。undefined はもちろんundefined :: Integer, undefined :: (), undefined :: Integer -> Integer などのようにどのような型にでも特化することができる多相型 forall a . a を持ちます。 これは Haskell の Preludeでは、

undefined = error "Prelude.undefined"

と定義されています。余談ですが、Curry-Howard同型に従って、多相型forall a . a の任意の値の表示は⊥でなければなりません。

部分関数と意味近似順序

$\bot$ (ボトム型) を使って部分関数を表すことができます。

$f(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\-2&{\mbox{ if }}n{\mbox{ is }}1\\\bot &{\mbox{ else }}\end{cases}}$

ここで、 $f(n)$ は $n=0$ と $n=1$ で定義された値を返しますが、他の全ての $n$には $\bot$ を返します。 $\bot$ 型が値を持たないように、$\bot$は普遍的であることに注意してください。関数$\bot$:: Integer -> Integer は

$\bot (n)=\bot$ for all $n$

と定義されます。ここで、 右辺にある$\bot$はInteger型の値を表します。

形式的には、Integer -> Integer という型を持つ 部分関数 とは、少なくとも持ち上げられた整数集合 $\mathbb {Z} _{\bot }=\{\bot ,0,\pm 1,\pm 2,\pm 3,\dots \}$ から持ち上げられた整数集合への数学的な写像のことをいいます。しかし、$\bot$の特別な役割を認識していないので、それだけでは不十分です。例えば、つぎの定義

$g(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}\bot \\\bot &{\mbox{ else }}\end{cases}}$

は直感に反するように見えますし、事実これは間違っています。 $g(1)$ は未定義な一方、なぜ $g(\bot )$ は値が定義されているのでしょうか？ 直感では全ての部分関数 $g$ は、定義された引数が多いほど定義された結果が得られるべきです。 形式的には、全ての具体的な数は $\bot$ より更に定義されている(more defined)と言えます。

$\bot \sqsubset 1\ ,\ \bot \sqsubset 2\ ,\dots$

ここで、$a\sqsubset b$ は $b$ が $a$ より更に定義されていることを表します。 同様に、$a\sqsubseteq b$ は $b$ は $a$ より更に定義されているか、等しい（そのため同じだけの定義度）です。 $\sqsubset$ は意味近似順序(semantic approximation order)と呼ばれます。なぜなら、定義された値をより定義されていない値によって近似できるので、「更に定義されている」とは「よりよい近似である」だと解釈できるからです。もちろん、$\bot$はデータ型の最小元となるよう設計されており、 x が $\bot$ を表していた場合を除けば、全ての$x$は$\bot \sqsubset x$を常に満たすといつでも言えます:

$\forall x\neq \bot \ \ \ \bot \sqsubset x$

他の数より "更に定義されている" ような数は存在しないので、任意の数の組における数学的な関係 $\sqsubset$ は偽になります。

$1\sqsubset 1$ は成立しない。 $1\sqsubset 2$ も $2\sqsubset 1$ も成立しない。

これは、普通の順序述語 $\leq$ では任意の二つの数を比較できるのとは対照的です。手っ取り早く覚える方法は次の文として考えるといいでしょう。「$1$ と $2$は『情報の内容』としては異なるが、『情報の量』としては同じである。」。 それが、私たちが $\leq$と異なる記号$\sqsubseteq$を使うもうひとつの理由です。

$1\sqsubseteq 2$ も $2\sqsubseteq 1$ も成立しない。 が、 $1\sqsubseteq 1$ が成立する。

$\sqsubseteq$は半順序(partial order)を規定し、Integer型の値は半順序集合 (partially ordered set、poset)をなすと言います。半順序は次の三つの法則で特徴付けられます。

• 反射率 : 全ての自分自身との半順序は自分自身である。$x\sqsubseteq x$ for all $x$
• 推移律 ：$x\sqsubseteq y$ かつ $y\sqsubseteq z$なら、$x\sqsubseteq z$
• 反対称律 : $x\sqsubseteq y$ かつ $y\sqsubseteq x$ が成立するなら、$x$ と $y$は等しい。 $x=y$。

演習
順序$\leq$について整数は半順序集合をなしているでしょうか？

次のグラフによって、 Integer型の値における順序$\sqsubseteq$を表現することができます。

ここで、全ての二つのノード間のリンクは、上にある方が下にある方に比べて、更に定義されされているとします。($\bot$を除いて)階層は1レベルだけであるため、 Integer は平坦領域(flat domain)であるといいます。図で見ると $\bot$が何故ボトムと呼ばれるのかがわかるでしょう。常に一番下に居座っているからです。

単調性(Monotonicity)

私達が部分関数に対して抱いた直感は、これで以下のように定式化することが出来ます。

半順序集合どうしを対応付ける全ての部分関数 $f$ は 単調 写像である。

引数が更に定義されると、更に定義された値を返す。

$x\sqsubseteq y\Longrightarrow f(x)\sqsubseteq f(y)$

特に、$h(\bot )=1$ である関数 $h$ は定数関数： $h(n)=1$ for all $n$ です。ここでは、 $1\sqsubseteq 2$ 等が成立しないことが重要なことに注意してください。

Haskellに翻訳すると、単調性の意味は $\bot$ は条件式で使えない、すなわち、$\bot$や、それと等価なundefinedをパターンマッチ出来ないということです。そうでないと、上記の例 $g$ がHaskellのプログラムとして表現できてしまいます。後で見るように、$\bot$はまた非停止プログラム(non-terminating program)をも表すので、Haskell内部から $\bot$ を観測することが出来ないことは、停止性問題と関連しているのです。

もちろん、より更に定義されているという概念は、任意の可能な引数について関数がもう一方より更に定義されていることを言うことで、部分関数に拡張可能です：

$f\sqsubseteq g{\mbox{ if }}\forall x.f(x)\sqsubseteq g(x)$

したがって、部分関数もまた半順序集合をなし、未定義の関数$\bot (x)=\bot$を最小元として持ちます。

不動点反復としての再帰的定義

階乗関数の近似

これで私たちは部分関数を記述する手段を手に入れたので、再帰的定義の解釈を与えることができます。再帰関数の例としてよく知られている階乗関数 $f(n)=n!$ を見てみましょう。

$f(n)={\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n\cdot f(n-1)$

ここまでで見てきたように、この再帰関数を集合を記述したものとして直接解釈すると問題を引き起こしかねないのですが、与えられた全ての$n$について $f(n)$を計算するためには右辺を繰り返していかなければならないことは直感的にわかります。この繰り返しは次のように形式化できます。一つ前の関数に次の定義を適用したもので右辺が構成されているような関数の列 $f_{k}$ を計算するのです。

$f_{k+1}(n)={\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n\cdot f_{k}(n-1)$

未定義の関数 $f_{0}(n)=\bot$ から始めると、部分関数の列は次のような結果になります。

$f_{1}(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\\bot &{\mbox{ else }}\end{cases}}\ ,\ f_{2}(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\1&{\mbox{ if }}n{\mbox{ is }}1\\\bot &{\mbox{ else }}\end{cases}}\ ,\ f_{3}(n)={\begin{cases}1&{\mbox{ if }}n{\mbox{ is }}0\\1&{\mbox{ if }}n{\mbox{ is }}1\\2&{\mbox{ if }}n{\mbox{ is }}2\\\bot &{\mbox{ else }}\end{cases}}$

などなど。明らかに、

$\bot =f_{0}\sqsubseteq f_{1}\sqsubseteq f_{2}\sqsubseteq \dots$

となり、関数の列は階乗関数に収束するでしょう。

この反復は、不動点反復(fixed point iteration)としてよく知られる図式に沿っています。

$x_{0},g(x_{0}),g(g(x_{0})),g(g(g(x_{0}))),\dots$

ここでの場合、 $x_{0}$ は関数、$g$ は関数から関数への写像である汎関数です。

$x_{0}=\bot$ and

$g(x)=n\mapsto {\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n*x(n-1)\,$

もし$x_{0}=\bot$から始めると、反復によって増加的に定義されてゆく、階乗関数の近似関数列が得られます。

$\bot \sqsubseteq g(\bot )\sqsubseteq g(g(\bot ))\sqsubseteq g(g(g(\bot )))\sqsubseteq \dots$

(この関数列が増加的であることの証明：まず、最初の不等式$\bot \sqsubseteq g(\bot )$は、$\bot$ がいかなるものより更に定義されてるということがないことから言えます。2番目の不等式は、最初の不等式の両辺にgを適用し $g$ が単調であることから言えます。3番目以降も同様です。）

この反復の図式は、Haskellで記述してみると分かりやすいでしょう。汎関数は普通の高階関数ですので、次のように書けます。

g :: (Integer -> Integer) -> (Integer -> Integer)
g x = \n -> if n == 0 then 1 else n * x (n-1)

x0 :: Integer -> Integer
x0 = undefined

(f0:f1:f2:f3:f4:fs) = iterate g x0

これで、関数 f0,f1,...にサンプルの引数を与えて評価し、 undefined を返すかどうか見ることができます。

 > f3 0
 1
 > f3 1
 1
 > f3 2
 2
 > f3 5
 *** Exception: Prelude.undefined
 > map f3 [0..]
 [1,1,2,*** Exception: Prelude.undefined
 > map f4 [0..]
 [1,1,2,6,*** Exception: Prelude.undefined
 > map f1 [0..]
 [1,*** Exception: Prelude.undefined

もちろん、f4が本当に全ての引数について未定義なのかを確認するのにこの方法は使えません。

収束

数学者にとっては、この近似関数の列は収束するのかという問題が残っています。これに答えるために、有向完備半順序(directed complete partial order、dcpo)という概念を導入します。ある半順序集合について、全ての単調なシーケンス$x_{0}\sqsubseteq x_{1}\sqsubseteq \dots$ (連鎖 (chain)とも呼ばれます) が上限(least upper bound、supremum)

$\sup _{\sqsubseteq }\{x_{0}\sqsubseteq x_{1}\sqsubseteq \dots \}=x$

を持つとき、かつそのときに限って、その半順序集合は有向完備半順序であると言います。

明らかに、意味近似順序については高階関数を近似する階乗関数の単調な列が極限を持つことを確かめることが出来ます。私たちの表示的意味論については、最小元 $\bot$を持つdcpoだけを取り扱います。そのようなdcpoは完備半順序(complete partial order、cpo)と呼ばれています。

明らかに Integer は(d)cpoです。なぜなら複数の要素からなる単調な列は以下の形式でなければならないからです。

$\bot \sqsubseteq \dots \sqsubseteq \ \bot \sqsubseteq n\sqsubseteq n\sqsubseteq \dots \sqsubseteq n$

ここで、 $n$ は普通の数です。それゆえ$n$はすでに上限です。

関数Integer -> Integer については、単調なシーケンスは無限の長さかもしれないので、同じ論証が成立しません。しかしIntegerが(d)cpoであるため、全ての点$n$について、上限

$\sup _{\sqsubseteq }\{\bot =f_{0}(n)\sqsubseteq f_{1}(n)\sqsubseteq f_{2}(n)\sqsubseteq \dots \}=:f(n)$

が存在します。意味近似順序は各点ごとに定義されるので、この関数$f$が私たちが求めていた上限です。

これらは、階乗関数の非叙述的な定義をwell definedに構成されたものに変換するという私たちの目標のために最後にふれました。もちろん、全ての$n$について実際に$f(n)$に値が定義されていることがまだ示されていません。しかし、これは難しくありませんし、不明確な定義(ill-formed definition)よりはるかに合理的です。

ボトムは非停止性を含む

新しく得られた再帰的な定義についての洞察を停止しない例に試してみるのは有益です。

$f(n)=f(n+1)$

この関数の近似列を書き下せば

$f_{0}=\bot ,f_{1}=\bot ,\dots$

となり、 $\bot$だけで構成されています。明らかに、結果の極限もまた $\bot$ になります。操作的な観点からは、このプログラムを実行した機械は永久にループします。よって、非停止(non-terminating)な関数や値もまた $\bot$ で表せることが解ります。ゆえに、停止性問題の決定不能性を考えれば、Haskellの中で$\bot$にパターンマッチさせることは不可能なのです。

最小不動点としての解釈

以前、近似意味をよく知られた"不動点反復"の例と言いました。そしてもちろん、階乗関数 $f$ の定義は汎関数$g$の不動点の仕様としても考えることが出来ます。

$f=g(f)=n\mapsto {\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n\cdot f(n-1)$

しかしながら、不動点にも色々あるかもしれません。具体的には、仕様を満たす次のようないくつかの$f$が存在します。

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

もちろん、このようなプログラムを実行するとき、$f(1)$か$f(2)$なら機械は永久にループし$f(1)$の値について有用な情報を生成しません。これは意味対象$f$となるものとして最小に定義された不動点に対応し、これは確かに自然な選択(a canonical choice)です。したがって、

$f=g(f)$

と言うとき、$g$の最小不動点$f$と定義します。明確に、最小は意味近似順序 $\sqsubseteq$を基準にしています。

$g$の条件に連続性(continuous、"chain continuous"とも呼ばれます)を加えたとき、私たちの反復構成は最小不動点の存在が保証されます。$g$が連続であるとは、単に$g$が単調なシーケンスの上限を保つ、つまり

$\sup _{\sqsubseteq }\{g(x_{0})\sqsubseteq g(x_{1})\sqsubseteq \dots \}=g\left(\sup _{\sqsubseteq }\{x_{0}\sqsubseteq x_{1}\sqsubseteq \dots \}\right)$

であることです。次に、

$f=\sup _{\sqsubseteq }\{x_{0}\sqsubseteq g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}$

を議論することができますので、

${\begin{array}{lcl}g(f)&=&g\left(\sup _{\sqsubseteq }\{x_{0}\sqsubseteq g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}\right)\\&=&\sup _{\sqsubseteq }\{g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}\\&=&\sup _{\sqsubseteq }\{x_{0}\sqsubseteq g(x_{0})\sqsubseteq g(g(x_{0}))\sqsubseteq \dots \}\\&=&f\end{array}}$

かつ繰り返しの極限は$g$の不動点であることが確かめられます。また、不動点反復によって実際に最小の不動点が得られることも確かめたいと思うかもしれません。

演習
$x_{0}=\bot$ で始まる不動点の繰り返しによって得られる不動点が最小不動点でもある、つまり他のどの不動点よりも小さいことを証明せよ。(ヒント：$\bot$はcpoの最小元で、gは単調である)

ところで、私たちの書いたそれぞれのHaskell関数が確かに連続であることはどのように確認すれば良いのでしょうか？単調性と同様に、プログラミング言語によって強制されているはずです。確かに、これらの性質は少しだけ強制したり、破ったりすることができるので、質問には少し無意味さを感じます。 しかし直感的には、単調性は$\bot$をパターンマッチさせることが不可能であることから保証されます。連続性については、任意の型aに対して、全ての単純な関数 a -> Integer は Integerの単調なシーケンスは有限の長さであることから自動的に連続であることが言えます。 全ての型aの値の無限の連鎖は、Integerの有限の連鎖に移され、上限を保つことは単調性から言えます。$g$::(Integer -> Integer) -> (Integer -> Integer)のような高階関数の場合、連続性はカリー化のために具現化します。つまりカリー化によって問題の型は ::((Integer -> Integer), Integer) -> Integer と同型な型なので、a=((Integer -> Integer), Integer)とすることができます。

Haskellにおいて、高階関数の不動点解釈は、不動点コンビネータ

fix :: (a -> a) -> a.

の助けを得て、

factorial = fix g

のようにコーディングすることができます。

不動点コンビネータは、

fix f = let x = f x in x

によって定義することができ、これは階乗関数を展開するときに少し戸惑いを残しますが、結果は最初の方法でHaskellの階乗関数を定義したときと異なると言うことはありません。しかしもちろん、このセクション全体で行った構成は、現実のHaskellプログラムを走らせたときには常に起こるわけではありません。この構成はHaskellプログラムの数学的解釈を確かなものにするための手段にすぎません。しかしそれでも、undefinedの助けによって、Haskellだけを使ってこれらの意味論を探究することができるのはとても素晴らしいことです。

正格と非正格の意味

正格関数

一引数の関数fが、

f ⊥ = ⊥.

を満たすとき、かつそのときに限って、その関数は正格(strict)であると呼ばれます。

次の関数は例は全て正格関数です。

id     x = x
succ   x = x + 1
power2 0 = 1
power2 n = 2 * power2 (n-1)

これらについて、特に予期しないことは何もありません。しかし何故これらの関数は正格なのでしょうか？それは、これらの関数を実際に正格であることを証明してみるのが有益でしょう。idの場合、これは定義からそのまま成り立ちます。succの場合、⊥ + 1は⊥になるか、またはそうでないかを熟慮する必要があります。もし、⊥にならないのならば、⊥ + 1 = 2もしくはより一般的に具体的なある数 kで⊥ + 1 = kと表せるでしょう。しかし全ての関数は単調であることを思い出すと、⊥ ⊑ 4 であることから

2 = ⊥ + 1 ⊑ 4 + 1 = 5

のようにならなければなりません。しかし、2 ⊑ 5、2 = 5、2 ⊒ 5のいずれも成り立たないので、kは2ではありません。一般に、

k = ⊥ + 1 ⊑ k + 1 = k + 1

は矛盾します。したがって唯一可能な選択肢は

succ ⊥ = ⊥ + 1 = ⊥

で、succは正格です。

演習
power2 が正格であることを証明せよ。一つはpower2 nは$2^{n}$であるという"明白な"事実を基にすることができ、後者は不動点繰り返しを使って証明するといいだろう。

非正格言語と正格言語

非正格(non-strict)な関数を探してみましょう。Integer -> Integer型の非正格関数のプロトタイプが起こすことは一つだけです。

one x = 1

全ての具体的な数をk とすると constk x = k はその亜種です。何故これらが唯一可能なものなのでしょうか？ one n は one ⊥より少なく定義されてはいけないことを思い出してください。Integerは平坦領域であるため、両者は等しくなければなりません。

なぜ one は非正格なのでしょうか？そのことを確認するために、Haskellのインタプリタを使って試してみると、

> one (undefined :: Integer)
1

⊥ではありません。oneはその引数を完全に無視するので、これは合理的です。

⊥を"非停止"などの意味で解釈するとき、ある人はoneの非正格性とは、その引数を強制的に評価する際に無限ループは避けられないということを意味する、と言うかもしれません。しかし、またある人は、全ての関数は結果を計算する前にその引数を評価しなければならず、one ⊥ は⊥を意味しなければならない、と言うかもしれません。つまり、もし引数を計算するプログラムが停止しない場合、oneも同様に停止すべきではない、と。

これらの主張の違いは、関数型プログラミング言語の場合、使う人が自由に選ぶことができるか、または他の設計がなされているかに現れます。ある人は、言語の正格、非正格は、関数の評価が正格、非正格のどちらがデフォルトなのかに依存すると言います。Haskellの選択は非正格です。対照的に、MLとLispは正格な意味論を選択しています。

多引数の関数

正格性の概念を多変数関数に拡張しましょう。例えば、二引数の関数 f が全ての x について

f x ⊥ = ⊥

を満たすとき、かつそのときに限って関数fは第二引数について正格であると言います。しかし多引数の場合、他の引数で与えた値に依存する混合形式の正格性がはるかに一般的です。例えば、条件式

cond b x y = if b then x else y

におけるyの正格性は、bがTrueかFalseかどうかに依存することがわかります：

cond True  x ⊥ = x
cond False x ⊥ = ⊥

xも同様です。どうやら、condはxとyが両方とも⊥なら確実に⊥になるようですが、どちらか一方の引数が少なくとも定義されているとは限りません。この振る舞いは正格性連結(joint strictness)と呼ばれています。

明らかにcondは、then節とelse節の両方を評価しない事が重要なif-then-else文のように振る舞います。

if null xs then 'a' else head xs
if n == 0  then  1  else 5 / n

ここでは、条件が満たされたときelseの部分は⊥です。したがって、非正格言語では、if-then-elseのようなプリミティブな制御文をcondのような関数でラップすることができます。このように、自分の制御オペレータを自分で定義することができます。

正格言語では、これは非正格性は正格な場合に比べ、コードの再利用のためのより多くの柔軟性を提供する一般的な観察を垣間見ることがあります。この主題に関する詳細は、遅延性の章を見るといいでしょう。

正格言語の全ての関数は正格ではない

このセクションは間違いであることが指摘されています(原文の議論を参照)

正格性や非正格性は、正格な言語でさえも注意することが重要で、全ての関数が正格ではありません。正格性と非正格性のどちらをデフォルトで選択したかは、特定の引数のデータ型に適用されます。Integer、(Bool,Integer)やEither String [Integer]のようなデータが含まれている引数の型は正格性を課しますが、Integer -> Boolのような関数型は必ずしも正格である必要はありません。Haskellライクな構文の正格言語を仮定して、インタープリタとセッションしてみます。

!> let const1 _ = 1

!> const1 (undefined :: Integer)
!!! Exception: Prelude.undefined

!> const1 (undefined :: Integer -> Bool)
1

なぜ正格言語の関数型の引数は正格ではないのでしょうか？もし正格だった場合は、不動点反復は塵のように崩れ去るでしょう！ $g$::(Integer -> Integer) -> (Integer -> Integer)の不動点反復を覚えていますか？

$\bot \sqsubseteq g(\bot )\sqsubseteq g(g(\bot ))\dots$

もし $g$ が正格なら、シーケンスは以下のようになります。

$\bot \sqsubseteq \bot \sqsubseteq \bot \sqsubseteq \dots$

明らかに無駄な$\bot$に収束しています。$g$ が引数の関数より更に定義されて作られているのが重要です。これは $g$ が有益な不動点を得るためには、その引数が正格であってはならないことを意味します。

補足ですが、この関数型は非正格でなければならないという事実は、正格な言語でいくつかの非正格な振る舞いを回復するために使用することが出来ます。一つは、()は単一の要素だけをもつよく知られた型を表す()型を引数にとる関数() -> Integerと、Integerのようなデータ型を単純に置き換えます。そのような関数は全て(⊥のほかに)唯一()だけが引数の値であり、単独の整数に対応します。しかし、() -> Integer型の引数の場合のその操作は非正格かもしれません。

演習
正格言語でIntegerを非正格な振る舞いの() -> Integerに持ち上げるのは面倒です。このことを行う関数 lift :: Integer -> (() -> Integer) を描く事は出来るでしょうか？どこに罠が潜んでいるでしょうか？

代数的データ型

動機付けとしてInteger型間の部分関数の場合を処理した後に、現在のHaskellにおける任意の代数的データ型の表示的意味論に範囲を拡張したいと思います。

用語について一言：特定の型の意味対象の集まりは通常、領域(domain)と呼ばれます。この用語は、"特定の定義"より一般的な名前で、私たちの領域がcpo(完全半順序)であると判断し、値の集合と一緒に不動点反復を可能にするためにいくつかの条件に従った更に定義(more defined)に関係します。通常、領域の値がコンピューター上でいくつかの有限の方法で表現でき、非可算無限集合のねじれた方法を熟慮するのを回避するために、cpoに条件を追加して確認します。しかし、私たちは一般の領域理論の定理を証明しようとしているわけではないため、条件を維持するだけの構成が生じます。

データ構築子

次の例を見てみましょう。

data Bool    = True | False
data Maybe a = Just a | Nothing

ここで、True、False、Nothing は引数の無いデータ構築子で、Justは一引数のデータ構築子です。

⊥はTrueとFalseの値からなる集合に加えられた最小元であることを思い出すと、この型は持ち上げられていると言えます。半順序集合の図が1レベルのみから構成されている領域を平坦領域と呼ぶのでした。私たちはすでに$Integer$が平坦領域で、⊥の上のレベルには無限の数があることよく知っています。

Maybe Boolの住人にはどのようなものがあるでしょうか？

⊥, Nothing, Just ⊥, Just True, Just False

したがって、一般的なルールは一つ以上の引数を持つデータ構築子に全ての可能な値を挿入することです。⊥のことも忘れずに。半順序については、任意の他の関数が単調でなければならないように、データ構築子も単調でなければなりません。したがって、半順序は次のようになります。

しかし、考慮すべき事があります：なぜJust ⊥ = ⊥ではないのでしょうか？"Just undefined"は"undefined"と同様に未定義を意味するでしょうに！答えは言語が正格であるか非正格であるかに依存します。正格言語の場合、全てのデータ構築子はデフォルトで正格です。すなわち、Just ⊥ = ⊥で、図は次のように減ります。

結果として、正格言語の領域は全て平坦です。

しかし、Haskellのような非正格言語の場合、データ構築子はデフォルトで非正格で、Just ⊥は⊥とは異なる新しい要素です。なぜなら、私たちはこれらに対して異なる反応を示す関数を書くことができるからです：

f (Just _) = 4
f Nothing  = 7

fはデータ構築子Justの中身を無視するので、f (Just ⊥)は4です。しかし、f ⊥は⊥です（直感的には、fが⊥を渡された場合、Justに分岐するかNothingに分岐するか判断することはできず、⊥を返すでしょう）。

これは、元のグラフが示すように非平坦領域を生じさせます。これらの扱いはどうあるべきでしょうか？グラフ簡約の文脈では、⊥は未評価の式とも考えられるかもしれません。したがって、x = Just ⊥という値は、（例えばルックアップなどの）計算は成功しておりNothingではなく、しかし、真の値はまだ評価されていないことを伝えています。もしxが成功したか失敗したかだけに興味があるなら、これは平坦領域での場合のようにxがJust TrueかJust Falseかを実際に計算する不要な作業から私たちを救います。非平坦領域の完全な影響は遅延性の章で見つけることができますが、一つの著名な例である無限リストを#再帰的データ型と無限リストのセクションで扱います。

パターンマッチング

正格関数のセクションでは、いくつかの関数が異なる入力に異なる結果を返し、単調性を主張することを検査することによって証明しました。しかしながら、代数的データ型の観点からは、現実のHaskellライフにも正格性の一つの源が存在する場合もあります。パターンマッチ、すなわちcase式です。data構文のデータ構築子をパターンマッチする際の一般的なルールは関数が正格になるように強制されます。すなわち、データ構築子に対して⊥を与えると常に⊥になります。説明のために、次のコードを考えてみます。

const1 _ = 1

const1' True  = 1
const1' False = 1

最初の関数const1は非正格ですが、一方const1'は正格です。なぜなら、関数の結果は引数に依存しないものの、TrueかFalseかを判断しているからです。関数引数のパターンマッチはcase式と等価で、

const1' x = case x of
   True  -> 1
   False -> 1

というコードと同様に正格性を課します。もしcaseで囲まれた引数の表示が⊥ならcase式の表示も⊥です。しかしながら、case式の引数は以下のようにもっと関与している可能性があります。

foo k table = case lookup ("Foo." ++ k) table of
  Nothing -> ...
  Just x  -> ...

これが、fooの正格性のために何を意味するのかを追跡するのは難しいことがあります。

等式スタイルのマルチパターンマッチの例の論理or：

or True _ = True
or _ True = True
or _ _    = False

等式は上から下にマッチされていくことに注意します。最初の等式は orの最初の引数に対してTrueかどうかマッチします。よって、orは最初の引数において正格です。この等式はor True xがxにおいて非正格であることも教えてくれます。もし最初の引数がFalseの場合、二番目の引数に対してTrueかマッチするので、or False xがxにおいて正格です。ワイルドカードの場合は一般に非正格のサインであることに注意すると、関数の正格性はデータ構築子に対するパターンマッチに関してこれらの位置に依存します。

演習
論理andの場合に同等の議論を与えよ。 "排他的論理和"(xor)は引数の一方がわかれば、他方の引数について非正格にできるだろうか？

パターンマッチの別の形式として、チルダを~付けた反駁不可パターン(irrefutable patterns)と名付けられたものがあります。これは次のように使います。

f ~(Just x) = 1
f Nothing   = 2

反駁不可パターンはf ⊥ = 1でも、常に成功して結果を返します(これが名前の由来です)。しかし、fの定義を変更した時、

f ~(Just x) = x + 1
f Nothing   = 2      -- この行は離れて残ることがあります。

次のようになります。

f ⊥       = ⊥ + 1 = ⊥
f (Just 1) = 1 + 1 = 2

もし引数がパターンにマッチしたら、対応する値をxに束縛します。そうでなければ、任意の変数xのように⊥を束縛します。

デフォルトでは、letとwhereも非正格に束縛します。

foo key map = let Just x = lookup key map in ...

は、次と等価です。

foo key map = case (lookup key map) of ~(Just x) -> ...

演習
Haskellの言語定義ではパターンマッチの詳細な定義を与えています。あなたは今や、これを理解することができるはずです。見てみましょう！ or関数の二つのBoolean引数が以下の性質を持つことについて考える: or ⊥ ⊥ = ⊥ or True ⊥ = True or ⊥ True = True or False y = y or x False = x この関数は正格性連結の例だが、遙かに鮮明だ。両方の引数が⊥の時だけ⊥になる。 (少なくとも引数はTrueか⊥に制限する)。このような関数はHaskellで実装することができるだろうか？

再帰的データ型と無限リスト

再帰的データ型の場合も基本から大きく異なるということはありません。ユニット型のリストを考えてみます。

data List = [] | () : List

これは単純な型に思えますが、$\bot$を適合させる方法は驚くほど沢山あり、対応するグラフも複雑になっています。このグラフのボトムが下に表示されています。省略記号はグラフがこの方向に沿って続くことを示します。赤い楕円の要素は、これが連鎖の最後であることを示しています。リストの要素は通常の形式になっています。

しかしここで、連鎖の長さもまた無限になっています。

⊥ $\sqsubseteq$ ():⊥ $\sqsubseteq$ ():():⊥ $\sqsubseteq$ ...

収束のセクションで全ての単調なシーケンスは上限を持たなければならないと注意したように、これはいくつかの問題を引き起こします。このことが可能になるのは無限リストが許可されている場合のみです。無限リスト（時にはストリーム(stream)とも呼ばれる）は非常に有用で、これらの多様な使い道を遅延性の章でかなり詳細に扱っています。ここでは、これらの表示的意味論がどのように理由づけられるかを示します。なお、以降の議論はリストのみに制限しますが、木のような任意の再帰的データ構造に容易に一般化できます。

以下では、Haskellにおける無限リストの実用的なプログラミングとの構文上のギャップを埋めるために、標準的なリスト型に戻ります。

data [a] = [] | a : [a]

演習
[Bool]に対応する非平坦領域を図で表せ。 図を[Integer]に変更するにはどのようにすればいいだろうか？

無限リストを使って計算する最良の例を示します。そのためには、まず無限リストが必要です。

ones :: [Integer]
ones = 1 : ones

この再帰的な定義に不動点反復を適用するとき、onesの上限が存在すべき事を確認します。

⊥ $\sqsubseteq$ 1:⊥ $\sqsubseteq$ 1:1:⊥ $\sqsubseteq$ 1:1:1:⊥ $\sqsubseteq$...

これは1の無限リストです。take 2 onesはどうあるべきかを考えてみましょう。takeの定義は次の通りです。

take 0 _      = []
take n (x:xs) = x : take (n-1) xs
take n []     = []

onesの近似シーケンスの要素をtakeに適用できます：

take 2 ⊥       ==>  ⊥
take 2 (1:⊥)   ==>  1 : take 1 ⊥      ==>  1 : ⊥
take 2 (1:1:⊥) ==>  1 : take 1 (1:⊥)  ==>  1 : 1 : take 0 ⊥
               ==>  1 : 1 : []

1:1:[]は完全に定義されているので、take 2 (1:1:1:⊥)などはtake 2 (1:1:⊥) = 1:1:[] と同じでなければならないことがわかります。入力のリストのシーケンスと出力リストのシーケンスの結果の両方を上限に取って、

take 2 ones = 1:1:[]

を結論づけることができます。したがって、まさに予想したとおりonesの先頭から二つの要素を取り出すように振る舞います。

この例を一般化すると、無限リストの推論について、近似シーケンスとその上限を渡すことを考慮しなければならないことがわかります。まさに無限リストです。まだ、私たちはそれにしっかりとした地面を与えていません。解決策は、連鎖自体の全体を無限リストと認識し、正式に私達の領域の新しい要素として追加することです：無限リストとはこれら近似のシーケンスです。もちろん、onesのような任意の無限リストは、

ones = 1 : 1 : 1 : 1 : ...

のようにコンパクトに書くことができ、単純に次のことを意味します。

what simply means that

ones = (⊥ $\sqsubseteq$ 1:⊥ $\sqsubseteq$ 1:1:⊥ $\sqsubseteq$ ...)

演習
もちろん、onesよりも興味深い無限リストは存在する。再帰的定義を用いて次の無限リストをHaskellで書け。 自然数のリスト nats = 1:2:3:4:... 右のような循環リスト cycle123 = 1:2:3: 1:2:3 : ... 前の演習を参考にして、Preludeの関数repeatとiterateがどのよう解決しているかを見よ。 式drop 3 natsが表す値を、テキストで使った例を使って見つけ出せ。 リストが正格な場合、すなわち[Integer]の領域が平坦であることを仮定する。その領域はどのようなものだろうか？無限リストについてはどうだろうか？onesはどのような値を表すだろうか？

ナゾナゾです。コンピュータで無限リストを計算する方法は何でしょうか？無限の時間のあとに全ての結果を表示する？ええっと、これはその通り。引っかけは、無限リストの有限な一部分だけを考慮した場合にコンピュータは有限の時間で終了するかもしれない、ということです。なので、無限リストは「潜在的に無限リスト」のように考えるべきでしょう。一般に、中間結果は無限リストの形式をとるのに対し、最終的な値は有限です。中間では無限のデータ構造のような、真の無限を扱うときにプログラムの正しさを推論できるのが表示的意味論の利点の一つです。

演習
中間結果として無限リストを使えることを実証するために、次によってmap (+1) natsが無限のシーケンスを最初に計算することに対応することを示せ。 take 3 (map (+1) nats) = take 3 (tail nats) もちろん、最終結果が確かに無限の時間を要する例を与える必要がある。 filter (< 5) nats の表示は何だろうか？ 時々だが、前の演習のfilterはtakeWhileと置き換えることができる。なぜ時々なのだろうか？そうでない場合はどうなるだろうか？

最後に注意点として、再帰的な領域の構造は関数の再帰的な定義に類似した不動点反復によって行うことができます。しかし、無限連鎖の問題に明示的に取り組まなければなりません。形式的な構成での解説は外部リンクを参照してください。

Haskell特産品: 正格性注釈とnewtype

Haskellは正格性注釈(strictness annotations)によってデータ構築子のデフォルトの非正格性動作を変更する方法を提供しています。データ型宣言で次のように

data Maybe' a = Just' !a | Nothing'

エクスクラメーションマーク "!"をデータ構築子の引数の前に指定することで、この引数は正格になります。それ故、先の例はJust' ⊥ = ⊥となります。より進んだ情報は正格性の章で見つけることができるでしょう。

あるケースで、次のようにデータ型をリネームしたいことがあります。

data Couldbe a = Couldbe (Maybe a)

しかしながら、Couldbe aは⊥とCouldbe ⊥の要素を両方含んでいます。newtypeの助けを借りて次のように定義します。

newtype Couldbe a = Couldbe (Maybe a)

このアレンジはCouldbe aはMaybe aと意味的に等価ですが、型検査では別の型として扱われます。特に、構築子Couldbeは正格です。しかし、次の定義とはまた微妙に異なるのです。

data Couldbe' a = Couldbe' !(Maybe a)

この説明のために、次の二つの関数を考えます。

f  (Couldbe  m) = 42
f' (Couldbe' m) = 42

ここで、f' ⊥は構築子Couldbe'のパターンマッチが失敗しf' ⊥ = ⊥の原因となります。しかし、newtypeバージョンの方は、Couldbeにマッチして失敗することはありません。f ⊥ = 42になります。ある意味では、この違いは次のように記述できます：

• 正格性注釈を付けた方の場合、Couldbe' ⊥は⊥のシノニム。
• newtypeの場合、⊥はCouldbe ⊥のシノニム。

⊥でのパターンマッチの失敗と、Constructor ⊥でのパターンマッチの失敗は一致しません。

newtypeは再帰型の定義にも使うかもしれません。リスト型[a]の代替となる次のような型を例にあげます。

 newtype List a = In (Maybe (a, List a))

再び、ポイントはIn構築子が&prep;を持ち上げて追加されたIn &prep;を導入しないということです。

Other Selected Topics

External Links

表示的意味論についてのオンライン書籍

• Schmidt, David A. (1986). Denotational Semantics. A Methodology for Language Development. Allyn and Bacon. http://www.cis.ksu.edu/~schmidt/text/densem.html.