依存型とは? わかりやすく解説

Weblio 辞書 > 辞書・百科事典 > 百科事典 > 依存型の意味・解説 

依存型

(dependent type から転送)

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/09/29 03:08 UTC 版)

ナビゲーションに移動 検索に移動

依存型 (いぞんがた、: dependent type) とは、計算機科学論理学において、値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。直観主義型理論においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。ATS英語版AgdaIdris英語版Epigram英語版などのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。

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

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

歴史

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

1934年にハスケル・カリーは、当時考えられていた数学的なプログラミング言語で使われていた型が、命題論理の公理系と同じパターンに従っていることを発見した。さらに、命題論理の証明それぞれに対して、プログラミング言語における関数(項)が対応していることもわかった。カリーの挙げた例の一つは、単純型付きラムダ計算直観主義論理の対応である。[1]

述語論理は命題論理に量化子を加えたものである。ハワードとド・ブラウンは型付きラムダ計算に依存関数のための型("任意の"に対応する)と依存ペアのための型("存在する"に対応する)を加えることで、述語論理に対応するプログラミング言語を作り出した。[2]

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

形式的な定義

非常に大雑把に説明すると、依存型は添字づけられた集合の族によって与えられると考えることができる。より形式的には、カテゴリ




英和和英テキスト翻訳>> Weblio翻訳
英語⇒日本語日本語⇒英語
  

辞書ショートカット

すべての辞書の索引

「依存型」の関連用語

依存型のお隣キーワード
検索ランキング

   

英語⇒日本語
日本語⇒英語
   



依存型のページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
All text is available under the terms of the GNU Free Documentation License.
この記事は、ウィキペディアの依存型 (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。 Weblio辞書に掲載されているウィキペディアの記事も、全てGNU Free Documentation Licenseの元に提供されております。

©2025 GRAS Group, Inc.RSS