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)で書かれます。例えば、
導入

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

と定義されます。ここで、 右辺にある ⊥ {\displaystyle \bot } はInteger型の値を表します。
ボトムと部分関数

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

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

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

他の数より "更に定義されている" ような数は存在しないので、任意の数の組における数学的な関係 ⊏ {\displaystyle \sqsubset } は偽になります。
ボトムと部分関数

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

⊑ {\displaystyle \sqsubseteq } は半順序(partial order)を規定し、Integer型の値は半順序集合 (partially ordered set、poset)をなすと言います。半順序は次の三つの法則で特徴付けられます。
ボトムと部分関数

次のグラフによって、 Integer型の値における順序 ⊑ {\displaystyle \sqsubseteq } を表現することができます。
ボトムと部分関数

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

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

特に、 h ( ⊥ ) = 1 {\displaystyle h(\bot )=1} である関数 h {\displaystyle h} は定数関数: h ( n ) = 1 {\displaystyle h(n)=1} for all n {\displaystyle n} です。ここでは、 1 ⊑ 2 {\displaystyle 1\sqsubseteq 2} 等が成立しないことが重要なことに注意してください。
ボトムと部分関数

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

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

したがって、部分関数もまた半順序集合をなし、未定義の関数 ⊥ ( x ) = ⊥ {\displaystyle \bot (x)=\bot } を最小元として持ちます。
不動点反復としての再帰的定義

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

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

未定義の関数 f 0 ( n ) = ⊥ {\displaystyle f_{0}(n)=\bot } から始めると、部分関数の列は次のような結果になります。
不動点反復としての再帰的定義

などなど。明らかに、
不動点反復としての再帰的定義

となり、関数の列は階乗関数に収束するでしょう。
不動点反復としての再帰的定義

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

ここでの場合、 x 0 {\displaystyle x_{0}} は関数、 g {\displaystyle g} は関数から関数への写像である汎関数です。
不動点反復としての再帰的定義

g ( x ) = n ↦ if n == 0 then 1 else n ∗ x ( n − 1 ) {\displaystyle g(x)=n\mapsto {\mbox{ if }}n==0{\mbox{ then }}1{\mbox{ else }}n*x(n-1)\,}
不動点反復としての再帰的定義

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

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

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

これで、関数 f0,f1,...にサンプルの引数を与えて評価し、 undefined を返すかどうか見ることができます。
不動点反復としての再帰的定義

もちろん、f4が本当に全ての引数について未定義なのかを確認するのにこの方法は使えません。
不動点反復としての再帰的定義

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

を持つとき、かつそのときに限って、その半順序集合は有向完備半順序であると言います。
不動点反復としての再帰的定義

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

明らかに Integer は(d)cpoです。なぜなら複数の要素からなる単調な列は以下の形式でなければならないからです。
不動点反復としての再帰的定義

ここで、 n {\displaystyle n} は普通の数です。それゆえ n {\displaystyle n} はすでに上限です。
不動点反復としての再帰的定義

関数Integer -> Integer については、単調なシーケンスは無限の長さかもしれないので、同じ論証が成立しません。しかしIntegerが(d)cpoであるため、全ての点 n {\displaystyle n} について、上限
不動点反復としての再帰的定義

が存在します。意味近似順序は各点ごとに定義されるので、この関数 f {\displaystyle f} が私たちが求めていた上限です。
不動点反復としての再帰的定義

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

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

この関数の近似列を書き下せば
不動点反復としての再帰的定義

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

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

しかしながら、不動点にも色々あるかもしれません。具体的には、仕様を満たす次のようないくつかの f {\displaystyle f} が存在します。
不動点反復としての再帰的定義

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

と言うとき、 g {\displaystyle g} の最小不動点 f {\displaystyle f} と定義します。明確に、最小は意味近似順序 ⊑ {\displaystyle \sqsubseteq } を基準にしています。
不動点反復としての再帰的定義

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

であることです。次に、
不動点反復としての再帰的定義

を議論することができますので、
不動点反復としての再帰的定義

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

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

Haskellにおいて、高階関数の不動点解釈は、不動点コンビネータ
不動点反復としての再帰的定義

の助けを得て、
不動点反復としての再帰的定義

のようにコーディングすることができます。
不動点反復としての再帰的定義

不動点コンビネータは、
不動点反復としての再帰的定義

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

一引数の関数fが、
正格と非正格の意味

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

次の関数は例は全て正格関数です。
正格と非正格の意味

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

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

は矛盾します。したがって唯一可能な選択肢は
正格と非正格の意味

で、succは正格です。
正格と非正格の意味

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

なぜ正格言語の関数型の引数は正格ではないのでしょうか?もし正格だった場合は、不動点反復は塵のように崩れ去るでしょう! g {\displaystyle g} ::(Integer -> Integer) -> (Integer -> Integer)の不動点反復を覚えていますか?
正格と非正格の意味

もし g {\displaystyle g} が正格なら、シーケンスは以下のようになります。
正格と非正格の意味

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

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

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

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

次の例を見てみましょう。
代数的データ型

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

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

Maybe Boolの住人にはどのようなものがあるでしょうか?
代数的データ型

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

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

結果として、正格言語の領域は全て平坦です。
代数的データ型

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

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

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

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

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

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

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

等式スタイルのマルチパターンマッチの例の論理or:
代数的データ型

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

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

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

次のようになります。
代数的データ型

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

デフォルトでは、letとwhereも非正格に束縛します。
代数的データ型

は、次と等価です。
代数的データ型

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

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

しかしここで、連鎖の長さもまた無限になっています。
代数的データ型

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

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

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

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

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

onesの近似シーケンスの要素をtakeに適用できます:
代数的データ型

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

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

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

のようにコンパクトに書くことができ、単純に次のことを意味します。
代数的データ型

what simply means that
代数的データ型

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

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

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

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

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

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

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

この説明のために、次の二つの関数を考えます。
代数的データ型

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

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

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

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

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

テンプレート:Haskell navigation