Web Analytics
Privacy Policy Cookie Policy Terms and Conditions 領域理論 - Wikipedia

領域理論

出典: フリー百科事典『ウィキペディア(Wikipedia)』

領域理論 (りょういきりろん、英 domain theory) は、通例、領域 (domain) と呼ばれる特別な種類の半順序集合を研究する数学の分野であり、よって順序理論の一分野である。 主要な応用分野は計算機科学であり、特に関数型プログラミング言語表示的意味論 (denotational semantics) を構築するために用いられる。 領域理論は、近似と収束という直観的概念を極めて一般的な枠組で形式化し、位相空間と密接な関係をもつ。 表示的意味論に対する他の重要なアプローチとしては距離空間を用いるものがある。

目次

[編集] 領域理論の意図と直観的意味

1960年代末にデイナ・スコットが領域についての研究を開始したそもそもの動機は、ラムダ計算表示的意味論について研究するためであった。 ラムダ計算においては、この言語が定めている記法で記される「関数」について考察する。 このラムダ計算では純粋に文法的に、単なる関数から入力引数として別の関数をとるような関数を作ることが可能である。 このラムダ計算には、不動点コンビネータ (fixed point combinator, Y コンビネータとも) といわれるものが存在することが知られている。 これは定義により、ラムダ計算で定められた文法的な変換を施すことで、任意の関数 f に対して f(Y(f)) = Y(f) となる性質をもつものである。

はじめに、このラムダ計算の表示的意味論を作り上げるために、各ラムダ式が通常の(全)関数を表すものとして、両者を対応づけるようなラムダ計算に対する「モデル」を作ることができたのだとしよう。 このようなモデルは純粋に文法的なシステムとしてのラムダ計算と、具体的な数学的関数を扱うための表記上のシステムとしてのラムダ計算との間を結びつけてくれるだろう。 しかし残念なことに、こうしたモデルは存在しない。 もし存在したとするなら、コンビネータ Y に対応する真の全関数、すなわち任意の入力関数 f不動点を計算するような関数を含まなければならなくなるからである。 いくつかの関数(例えば「次者関数」)にはこのような不動点は存在しないので、Y に対応するような関数は存在しえない。 よってよくても、Y に対応する通常の関数は、いくつかの入力に対して必ずしも値が定義されていないような部分関数でなければならない。

スコットは、この困難を回避するため、結果を返さない計算を表現するための「部分」もしくは「不完全」な情報という概念を形式化した。 これは、計算の各領域(例えば自然数)に対して「未定義」出力、つまり決して終わらない計算の「結果」を表す新しい要素を付け加えることによりモデル化される。 さらに、この計算の領域には「未定義の結果」が最小元となるような「順序関係」が与えられている。

ラムダ計算のモデルを見つける上で大切なことは、(半順序集合上で)これらの関数のみを考慮することである。 こうした関数は、最小不動点をもつことが知られている。 これらの関数の集合に適切な順序が与えられたものもこの理論の意味で「領域」ではあるが、あらゆる可能な関数ではなく、その部分集合へ制限することにも別の大きな利点がある。 そうした場合、それ自体の関数空間を含むような領域、すなわち関数自身を適用することのできる関数が得られる。

こうした望ましい特性に加えて、領域理論は直観的な解釈に訴えることも可能にしている。 上述のように、計算の領域は常に半順序が与えられている。 この順序は情報あるいは知識の階層を表現している。 この順序でより大きな要素は、より詳しく定められており、より多い情報を含んでいる。 より小さな要素は、不完全な知識、あるいは途中結果を表現している。

このとき計算は、結果を改善するために領域の要素に繰り返し単調関数を適用することとしてモデル化される。 不動点に達することとは計算が完了することである。 領域が、こうした概念に対する優れた枠組みを与えているのは、それに単調関数の不動点が存在することが保証されており、制限を追加すれば、下側から近似できるからである。

[編集] 形式的定義のための手引き

この節では、領域理論の核心となる概念と定義を与える。 理論の数学的な定式化を意味づけるため、上に述べた、領域についての「情報の順序」という直観的解釈に重点を置くことにしよう。 正確な形式的定義は各概念を扱った文献で知ることができる。 また、一般的な順序理論の定義の一覧は order theory glossary にある。 しかし、領域理論の最も重要な概念は以下で導入される。

[編集] 指定の収束としての有向集合

すでに述べたように、領域理論は計算の領域をモデル化するのに半順序集合を取り扱う。 目標は、このような順序集合の要素を「情報の断片」あるいは「計算の(部分的)結果」として解釈することである。 そこでは、この順序でより大きな要素は、それ以下の要素の情報を矛盾しない方法で拡張したものとなる。 ここでこの単純な直観的解釈からすでに、領域は多くの場合、最大元を持っていないことがわかる。 最大元を持つことは、他の「すべて」の要素の情報を含むというあまり面白くない状況にあたる要素が存在することを意味するからである。

この理論で重要な役割をはたす概念のひとつは、領域の有向部分集合 (directed subset)、すなわち、任意の 2 要素が上界をもつような非空の部分集合である。 領域についての直観的解釈の観点では、有向部分集合の中のすべての 2 つの情報の断片が、部分集合の別のある要素によって「矛盾なく」拡張されていることを意味する。 よって、「矛盾しない指定」、つまり、どの 2 つの要素も矛盾することのない部分的結果の集合として有向集合をみることができる。 この解釈は、各要素がそれより前の要素よりも明確なものとなっているような解析学数列の概念と比較できる。 実際、距離空間の理論では、数列は、領域理論における有向集合の役割と多くの点で類似した役割を演じる。

いま、数列のときと同じように、有向集合の「極限」に興味がある。 上で述べたことに従えば、これは、有向集合のすべての要素の情報を拡張した情報の最も一般的な断片にあたる要素、すなわち、有向集合に含まれる情報を「正確」に含み、それ以上のものはもたない唯一の要素ということになるだろう。 順序集合の形式では、これは有向集合の上限 (最小上界) にすぎない。 数列の極限の場合のように、有向集合の上限は常に存在するとは限らない。

もちろん、指定が矛盾しないならば必ず「収束」するような計算の領域、すなわち、すべての有向集合が上限をもつような順序に興味をもつのが自然だろう。 この特性は有向完備半順序集合 (directed complete partial order set)、あるいは略して dcpo を定める。 実のところ、領域理論のほとんどの考察は、少なくとも有向完備であるような順序のみを考えている。

不完全な知識を表現するものとして、部分的に指定された結果を考えるというアイデアから、最小元の存在という別の望ましい特性が導かれる。 この要素は情報を持たないという状態のモデルとなり、ふつう計算が開始される地点である。 これはまた、まったく何も結果を返さないような計算の出力とみなすこともできる。 理論にとっての重要さから最小元をもつ dcpo完備半順序集合 (complete partial order set) または単に cpo と呼ばれる。

[編集] 計算と領域

計算の領域が何であるべきかについて、すでにいくつかの基礎的で形式的な記述がそろったので、計算そのものへと目を転じることができる。 明らかに、それは関数でなければならなず、ある計算の領域から入力をもらい、ある(おそらくは異なった)領域へと出力を返す。 さらに、入力の情報の内容が増えたなら、関数の出力がより多くの情報を含むとも期待できるだろう。 これは、形式的には単調な関数を要求していることになる。

Dcpo を扱うときには、有向集合の極限の構成と矛盾しない計算も要求するかもしれない。 これは形式的に、ある関数 f に対して、有向集合 D の像 f(D) (すなわち、D の各要素の像の集合)がやはり有向集合であって、上限として D の上限の像をもつことを意味する。 これを f有向集合の上限を保存するとも言える。 また、2 要素の有向集合を考えればわかるように、このような関数は単調でなければならないこともわかる。 この特性は、スコット連続 (Scott-continuous) な関数の概念を与える。 多くの場合あいまいにはならないので、これは単に 連続関数 とも言われる。

[編集] 近似と有限性

領域理論は、情報の状態の構造をモデル化する純粋に定性的なアプローチである。 より多くの情報を含むものについて語ることはできても、付け加えられた情報の量は示されない。 しかし、与えられた情報の状態よりも、ある意味ではるかに単純な(はるかに不完全な)要素について語りたい場合もある。

例えば、あるベキ集合上に部分集合の包含の自然な順序を与えたとき、無限集合であるような任意のベキ集合の要素は、その任意の有限の部分集合よりも「有用」である。 こうした関係をモデル化しようとするなら、まず領域の順序 から導かれる狭義の順序 < (厳密に小さい)について考えるかもしれない。 しかし、これは全順序の場合には有用な記号であっても、半順序集合の場合には多くのことを教えてはくれない。 いま一度、集合の包含順序を考えれると、ある(無限集合かもしれない)集合は、それに 1 要素のみを加えただけの別の集合よりもそれだけで厳密に小さくなる。 これが「はるかに単純な」ものであるという概念を捉えているとは同意しにくいだろう。

より手の込んだアプローチは、いわゆる近似の順序、あるいはより示唆的に way-below relation と呼ばれるものを定めることである(way below は「ずっと下の」の意)。 要素 x が要素 y よりも way below であるとは、上限 sup D をもつ有向集合 D 各々に対して、y ≤ sup D ならば、各 D 中に要素 d が存在し、xd となることである。 このとき、xy近似するとも言い、xy と書く。 一点集合 {y} も有向であることから、これは xy であることも導く。 例えば、集合の包含の順序においては、無限集合はその任意の有限部分集合よりも way above であることがわかる。 一方、有限集合 {0}, {0, 1}, {0, 1, 2}, ... からなる有向集合(実際には鎖)を考えれば、この鎖の上限は、すべての自然数の集合 N なので、これは、N より way below であるような無限集合がないことを示している。

しかし、ある要素よりも way below であるということは相対的な概念であり、要素のみについて大したことを明らかにはしない。 例えば、有限集合というものを順序理論的方法で特徴づけたいとしても、ある集合より way below であるような無限集合もある。 この意味で有限の要素 x がもつ特殊な特性は、それらがそれ自体よりも way below、すなわち xx であることである。 この特性をもつ要素はコンパクトであるとも言われる。 このような要素が、他の数学における意味で「有限」でも「コンパクト」でもある必要はないが、これは、集合論位相における対応する概念にある程度沿って名付けられたものである。 領域のコンパクトな要素は、それが含まれていないような有向集合の極限として得られないという重要で特殊な特性をもっている。

Way-below relation についてのその他の重要な帰結は、この定義が領域の多くの重要な側面を捉えるのに非常に適したものだという主張を裏付けている。 詳細は way-below relation についての文献を参照。

[編集] 領域の基底

前節の考察は別の疑問を提起する。 領域のすべての要素がはるかに単純な要素の極限として得られることを保証することは可能だろうか? これは現実の問題に大いに関係がある。 我々は無限の対象を計算できないが、それでもこれによってそれをいくらでも近似する望みがあることになる。

より一般的には、上限として他のすべての要素を得るのに十分であるような部分集合に制限したい。 よって、半順序集合 P基底 (base) B を、任意の P 中の x に対して、x よりも way below であるような B 中の要素の集合の上限が x となるような P の部分集合として定義する。 半順序集合 P は、基底をもつとき連続半順序集合である。 特にこのとき P 自体は基底である。 多くの応用分野では、主要な研究の対象を連続 (d)cpo に制限している。

最後に、半順序集合に対するいくらか強い制限は「コンパクト」な要素の基底の存在を要求することにより与えられる。 このような半順序集合は代数的であるといわれる。 代数的半順序集合は、それが有限のものに制限されていても、すべての要素の近似を可能にするため、表示的意味論の観点からはとりわけ行儀よくふるまう。 前に注意したように、すべての有限の要素は古典的な意味で「有限」であるとは限らず、有限の要素が非可算な集合を構成することもありうる。

しかしある場合には、半順序集合に対する基底は可算である。 この場合、ω 連続半順序集合と言う。 従って、もし可算の基底がすべて有限の要素からなるなら、ω 代数的な順序が得られる。

[編集] 特殊な種類の領域

特に簡単で特殊な領域として、 elementary あるいは平坦領域 (flat domain) として知られているものがある。 これは、他のすべての要素より小さいものとみなされる単一の「底」と、整数のような比較不能な要素の集合からなる。

他にも、「領域」として適切なものとなりうる興味深い特殊な種類の順序構造を数多く得ることができる。 すでに、連続半順序集合と代数的半順序集合について議論した。 それらの特性を合わせ持つより特殊な半順序集合は連続かつ代数的な cpo である。 さらに、完備性を加えることにより、連続束と代数束を得る。 これは単に各々の特性を持つ完備束である。 代数的な場合については調べる価値のある半順序集合のより広い種類が見出される。 スコット領域は最初に領域理論が研究された構造であった。 それよりいくらか広い種類の領域としては、SFP domain, L domain, bifinite domain がある。

これらすべての種類の順序は、単調写像、スコット連続写像、あるいはより特殊化された様々な写像を射として用いた dcpoカテゴリーに割り当てられる。 最後に、「領域」という用語自体は正確なものでなく、よって以前に形式的定義を与えてきたとき、あるいは詳細が不適切なものであるときには略語のみが用いられる。

[編集] 重要な帰結

半順序集合 Ddcpo であるのは、D 中の各鎖が上限を持つとき、かつそのときに限る。 しかし、有向集合は鎖よりもずっと強力である。

最小元をもつ半順序集合 Ddcpo であるのは、D 上のすべての単調関数 f が不動点を持つとき、かつそのときに限る。 もし f が連続なら、最小不動点をもつ。 これは、最小元 0 上での f の有限回の繰り返しすべての上限 n ∈ N fn(0) として与えられる。

もちろん、領域理論が適用される応用分野に依存して、この他にも多くの帰結がある。 文献を参照して頂きたい。(そして寄稿して頂きたい。)

[編集] 文献

おそらく今日の領域理論についての書籍で最も勧められるもののひとつであり、基本的理論の多くの部分に非常に明確で詳細な視点を与えている :

  • G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott, Continuous Lattices and Domains, In Encyclopedia of Mathematics and its Applications, Vol. 93, Cambridge University Press, 2003. ISBN 0521803381

領域理論の標準的な文献であり、無償でオンラインで手に入れられる :

  • S. Abramsky, A. Jung: Domain theory. In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, vol. III. Oxford University Press, 1994. (ISBN 019853762X) (download PDF PS.GZ)

スコットの古典的論文のひとつ :

  • D. S. Scott. Data types as lattices. In G. Muller et al., editors, Proceedings of the International Summer Institute and Logic Colloquium, Kiel, volume 499 of Lecture Notes in Mathematics, pages 579-651, Springer-Verlag, 1975.

順序理論の一般的で読みやすい説明であり、領域理論の入門も含まれている :

  • B. A. Davey and H. A. Priestley, Introduction to Lattices and Order, 2nd edition, Cambridge University Press, 2002. ISBN 0521784514
他の言語
THIS WEB:

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - be - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - closed_zh_tw - co - cr - cs - csb - cu - cv - cy - da - de - diq - dv - dz - ee - el - eml - en - eo - es - et - eu - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gd - gl - glk - gn - got - gu - gv - ha - haw - he - hi - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mg - mh - mi - mk - ml - mn - mo - mr - ms - mt - mus - my - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - rm - rmy - rn - ro - roa_rup - roa_tara - ru - ru_sib - rw - sa - sc - scn - sco - sd - se - searchcom - sg - sh - si - simple - sk - sl - sm - sn - so - sq - sr - ss - st - su - sv - sw - ta - te - test - tet - tg - th - ti - tk - tl - tlh - tn - to - tokipona - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu

Static Wikipedia 2008 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2007:

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - be - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - closed_zh_tw - co - cr - cs - csb - cu - cv - cy - da - de - diq - dv - dz - ee - el - eml - en - eo - es - et - eu - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gd - gl - glk - gn - got - gu - gv - ha - haw - he - hi - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mg - mh - mi - mk - ml - mn - mo - mr - ms - mt - mus - my - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - rm - rmy - rn - ro - roa_rup - roa_tara - ru - ru_sib - rw - sa - sc - scn - sco - sd - se - searchcom - sg - sh - si - simple - sk - sl - sm - sn - so - sq - sr - ss - st - su - sv - sw - ta - te - test - tet - tg - th - ti - tk - tl - tlh - tn - to - tokipona - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu

Static Wikipedia 2006:

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - be - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - closed_zh_tw - co - cr - cs - csb - cu - cv - cy - da - de - diq - dv - dz - ee - el - eml - en - eo - es - et - eu - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gd - gl - glk - gn - got - gu - gv - ha - haw - he - hi - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mg - mh - mi - mk - ml - mn - mo - mr - ms - mt - mus - my - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - rm - rmy - rn - ro - roa_rup - roa_tara - ru - ru_sib - rw - sa - sc - scn - sco - sd - se - searchcom - sg - sh - si - simple - sk - sl - sm - sn - so - sq - sr - ss - st - su - sv - sw - ta - te - test - tet - tg - th - ti - tk - tl - tlh - tn - to - tokipona - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu