依存型のソースを表示

{{出典の明記|date=2015年4月18日 (土) 11:54 (UTC)}}
{{型システム}}
'''依存型''' (いぞんがた、{{lang-en-short|dependent type}}) とは、[[計算機科学]]と[[論理学]]において、値に依存する型のことである。数学の[[型理論]]の表現形式と計算機科学における[[型システム]]の特徴を併せ持つ。[[直観主義型理論]]においては、全称量化子や存在量化子のような論理学における[[量化子]]をエンコードするために依存型が用いられている。{{仮リンク|ATS (プログラミング言語)|label=ATS|en|ATS (programming language)}}、[[Agda]]、{{仮リンク|Idris|en|Idris (programming language)}}、{{仮リンク|Epigram|en|Epigram (programming language)}}などのいくつかの[[関数型プログラミング言語]]では、依存型を使った非常に表現力の強い型によって、バグを防止している。

依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の''値''に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。 (これは、型そのものを引数として取ることができるという[[ポリモーフィズム]]とは別の概念である。) 依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。

依存型を入れた[[型システム]]は、より複雑になる。プログラム中に出現する2つの依存型が等しいかどうかを判定するとき、プログラムの一部を実行する必要があるかもしれない。特に、依存型に任意の式を含めることが許される場合、型の同値性判定は任意に与えられた2個のプログラムが同じ結果をもたらすかどうかを判定する問題を含んでしまう。したがって、この場合は[[型検査]]は[[決定不能問題|決定不能]]となってしまう。

==歴史==
依存型は、プログラミングと論理学のつながりを深めるために作られた。

1934年に[[ハスケル・カリー]]は、当時考えられていた数学的なプログラミング言語で使われていた型が、[[命題論理]]の公理系と同じパターンに従っていることを発見した。さらに、命題論理の証明それぞれに対して、プログラミング言語における関数(項)が対応していることもわかった。カリーの挙げた例の一つは、[[単純型付きラムダ計算]]と[[直観主義論理]]の対応である。<ref name=curry_howard>{{cite journal|last=Sørensen|first=Morten Heine B.|author2=Pawel Urzyczyn|title=Lectures on the Curry-Howard Isomorphism|year=1998|url=http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385}}</ref>

[[述語論理]]は命題論理に量化子を加えたものである。ハワードとド・ブラウンは型付きラムダ計算に依存関数のための型("任意の"に対応する)と依存ペアのための型("存在する"に対応する)を加えることで、述語論理に対応するプログラミング言語を作り出した。<ref name=dep_types_at_work>{{cite journal|last=Bove|first=Ana|author2=Peter Dybjer|title=Dependent Types at Work|year=2008|url=http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf}}</ref>

(これを含むいくつかの業績により、命題を型と見なす考え方は[[カリー＝ハワード同型対応]]という名前で知られている。)

==形式的な定義==
非常に大雑把に説明すると、依存型は添字づけられた[[族 (数学)|集合の族]]によって与えられると考えることができる。より形式的には、<math>A:\mathcal{U}</math>を<math>\mathcal{U}</math>(型のなす[[宇宙 (数学)|宇宙]])に属する型としたときに、'''型のなす族'''<math>B:A\to\mathcal{U}</math>を考えることができる。すなわち、<math>A</math>に属する値<math>a:A</math>それぞれについて、型<math>B(a):\mathcal{U}</math>が割り当てられているのである。[[終域]]が引数に応じて変化する関数は'''依存関数'''と呼ばれ、このような関数のための型は'''依存型'''、'''依存積型'''、あるいは'''Π型'''と呼ばれる。この例では、依存積型は
:<math>\Pi_{(x:A)}B(x)</math>
あるいは
:<math>\Pi (x:A),B(x)</math>
と表記される。

もし''B''が定数関数<math>B(x)=C</math>であるなら、依存積型は通常の関数型(矢印型)<math>A\to C</math>となる。つまり、<math>\Pi_{(x:A)}B</math>は型判定において関数型<math>A\to C</math>と等しい。

Π型という名前は、依存積型が型の[[直積集合|直積]]と見なせるという考え方に由来している。依存積型は[[全称量化]]の[[モデル理論|モデル]]として理解することもできる。

例えば、[[実数]]の<math>n</math>個の対を<math>\mbox{Vec}({\mathbb R},n)</math>と表記するとき、<math>\Pi_{(n:{\mathbb N})} \mbox{Vec}({\mathbb R},n)</math>は、[[自然数]]''n''を受け取り''n''個の実数の対を返す関数の型である。通常の関数空間は、依存積型で戻り値の型が実際には引数に依存しない特別な場合としてあらわれる。''例えば''、<math>\Pi_{(n:{\mathbb N})}\; {\mathbb R}</math>は自然数から実数への関数の型であり、単純型付きラムダ計算では<math>{\mathbb N}\to{\mathbb R}</math>と表記される。

[[ポリモーフィズム|型多相な関数]]は依存関数(すなわち、依存積型をもつ関数)の重要な例である。多相関数は、型を与えられると、その型を含む型を持つ値として振る舞う。例えば、恒等関数、すなわち任意の型''A''に対し<math>a:A</math>を受け取り''a''をそのまま返す関数、の型は、
:<math>\Pi_{(A:\mathcal{U})} A\to A</math>
と書くことができる。

==依存ペア型==
依存積型の[[双対]]は、'''依存ペア型'''、'''依存和型'''、あるいは'''Σ型'''と呼ばれる型である。これは[[余積]]や[[直和]]、[[非交和]]などのアナロジーである。依存和型は[[存在量化]]のモデルとして理解することもできる。依存和型は
:<math>\Sigma_{(x:A)} B(x)</math>
と表記される。

依存和型は、2番目の型が1番目の値に応じて変化するペアの型を表している。したがって、もし
:<math>(a,b):\Sigma_{(x:A)} B(x)</math>
ならば、<math>a:A</math>であり、<math>b:B(a)</math>である。''B''が定数関数<math>B(x)=C</math>のときは、依存和型は[[直積型]]、すなわち通常の直積<math>A\times C</math>と一致する(型判定において一致する)。

===存在量化としての例===
<math>\Sigma A B_a: \mathcal{U}</math>を、型<math>A: \mathcal{U}</math>上で述語<math>B: A \rarr \mathcal{U}</math>を量化した依存和型とする。このとき、<math>B_a</math>が成立する<math>a:A</math>が存在することと、<math>\Sigma A B_a</math>が非空であることが同値である。例えば、''a''が''b''以下であることと、自然数''n''と''a''+''n''=''b''の証明の組が存在することが同値である。
:<math>a\le b \iff \Sigma \mathbb{N} (\lambda n \rarr a+n=b)</math>

==ラムダ・キューブ==
[[ヘンク・バレンドレクト]] ([[:en:Henk Barendregt]]) はいくつかの型システムを3つの軸にそって分類する[[ラムダ・キューブ]]を発明した。立方体の形をした図の8個の頂点それぞれが型システムに対応している。[[単純型付きラムダ計算]]が最も表現力が低い頂点に配置され、[[Calculus of constructions]] ([[:en:Calculus of constructions]])が最も表現力が高い頂点に配置されている。立方体の3個の軸はそれぞれ単純型付きラムダ計算に対する3種類の異なる拡張を意味している。それぞれ、依存型の追加、型多相性の追加、高階のカインド ([[:en:Kind (type theory)]]) を持つ型コンストラクタ (例えば型から型への関数) の追加、である。ラムダ・キューブは[[純粋型システム]] ([[:en:Pure type system]])によってさらに一般化される。

ラムダ・キューブにおける(狭義の)依存型と多相型は、どちらも(広義の)依存積型の特別な場合と見なせるが、値に関する量化をする場合は(狭義の)依存型、型や型コンストラクタに関する量化をする場合は多相型と呼び、区別される。ラムダ・キューブにおけるカインド(通常の型を集めた特別な型)を<math>*</math>, 超カインド(カインドを集めた特別な型)を<math>\square</math>と表記する。このとき、(狭義の)依存型とは、<math>A:*</math>および<math>B:A\to *</math>を用いて構成される、<math>\Pi_{(x:A)} B(x)</math>という型のことである。一方、多相型は、<math>A:\square</math>および<math>B:A\to *</math>を用いて構成される、<math>\Pi_{(x:A)} B(x)</math>という型のことである。例えば、<math>*:\square</math>であることを用いて<math>\Pi_{(x:*)} B(x)</math>と書いたものは、型に関する量化をしている多相型となる。<ref name=dependent_types_in_lambda_cube>{{cite journal|last=Peterka|first=Ondrej|title=Dependent Types In Lambda Cube|year=2007|url=http://www.fit.vutbr.cz/study/courses/TJD/public/0708TJD-Peterka.pdf}}</ref>

===一階の依存型理論===
一階の依存型を持つ<math>\lambda \Pi</math>型システムは、[[単純型付きラムダ計算]]の関数型(矢印型)を依存積型に一般化することで得られる。これは論理学におけるLogical Framework LF ([[:en:Logical framework#LF]])に対応する。

===二階の依存型理論===
二階の依存型を持つ<math>\lambda \Pi 2</math>型システムは、<math>\lambda \Pi</math>に型コンストラクタ上での量化を許容することで得られる。この型システムでは、依存積演算子は単純型付きラムダ計算の<math>\to</math>演算子と[[System F]]の<math>\forall</math>束縛子の両方の役割を果たす。

===高階の依存型付き多相ラムダ計算===
高階の<math>\lambda \Pi \omega</math>型システムは<math>\lambda \Pi 2</math>を、[[ラムダ・キューブ]]の4つ全てのラムダ抽象の形式に拡張することで得られる。すなわち、項から項への関数、型から項への関数、項から型への関数、そして型から型への関数である。この型システムは[[Calculus of constructions]]に対応する。Calculus of constructionsをさらに拡張すると[[Calculus of inductive constructions]] ([[:en:Calculus of inductive constructions]]) が得られる。これは、[[Coq]]が用いている型システムである。

== プログラミング言語と論理学の両立 ==
[[カリー＝ハワード同型対応]]により、どんなに複雑な数学的な性質も型によって表現できる。もしユーザーが、型が''非空''である (つまり、その型を持つ値が存在する) ことの[[構成的な証明]]を与えることができれば、コンパイラは証明の正当性を検査し、証明の構成を追うことにより、実際にその値を計算できる実行可能なプログラムコードを出力することができる。このように証明を検査できるという性質により、依存型を持つプログラミング言語は[[定理証明支援系]]と近い関係にある。コードを生成できるという視点からは、機械的に検証された数学の証明からプログラムコードを直接導出することができるため、形式手法による[[プログラム検証]]や{{仮リンク|証明つきコード|en|Proof-carrying code}}へのアプローチが考えられる。

==脚注==
{{Reflist}}

==関連項目==
*[[型理論]]
*[[直観主義型理論]]
*[[型付きラムダ計算]]
*[[型システム]]

{{データ型}}
{{Computer-stub}}

{{DEFAULTSORT:いそんかた}}
[[Category:データ型]]
[[Category:型システム]]
[[Category:型理論]]