|
===================================== 〔語彙分解〕的な部分一致の検索結果は以下の通りです。 ・ ー ： [ちょうおん] (n) long vowel mark (usually only used in katakana)
ペール・マルティン＝レーフ (Per Martin-Löf, 1942年 - ) はスウェーデンの論理学者、哲学者、数学者。直観主義型理論の創案者として知られ、現在はストックホルム大学数学部および哲学部の教授を務めている。 1964年から1965年にかけてモスクワのアンドレイ・コルモゴロフのもとで学び、ランダム系列に関する研究〔Per Martin-Löf, "The definition of random sequences," ''Information and Control'', Vol.9, pp. 602-619, 1966.〕を行う。1968年から1969年にかけてはシカゴ大学助教授を務め、ここでウィリアム・ハワードとカリー＝ハワード対応に関して議論している。1971年には型理論に関する最初の草稿を書き上げているが、この最初の非可述体系はジャン＝イヴ・ジラールによって矛盾していることが示された（ジラールのパラドックス）。これをきっかけに型理論の概念的基礎の探求へと導かれていったマルティン＝レーフは、1984年の著作〔Per Martin-Löf, ''Intuitionistic Type Theory'', Bibliopolis, 1984 (ISBN 8870881059).〕で提示した可述型理論を正当化するための証明論的意味論を展開し、またこれに関連していくつかの哲学的著作〔Per Martin-Löf, "On the meanings of the logical constants and the justifications of the logical laws ", ''Atti degli Incontri di Logica Matematica'', Vol.2, 1985, pp. 203-281; Reprinted in ''Nordic Journal of Philosophical Logic'', Vol.1, 1996, pp. 11-60. 〕〔Per Martin-Löf, "Analytic and synthetic judgements in type theory" in Paolo Parrini (ed.), ''Kant and Contemporary Epistemology'', Kluwer, 1994, pp. 87-99 (ISBN 0792326814).〕も発表している。 彼の直観主義型理論は依存型 (dependent type) の概念を発展させたことで知られており、これは後の calculus of construction 等に影響を与えた。また、Nuprl をはじめとして、マルティン＝レーフの型理論に基づいた自動証明システムも開発されている。マルティン＝レーフの業績は今なお論理学および理論計算機科学の研究にインスピレーションを与え続けており、彼のアイデアが持つ可能性はいまだに汲み尽くされていないといえる。 ==出典・参考文献== 〔 * Bengt Nordström, Kent Petersson, and Jan M. Smith. ''Programming in Martin-Löf's Type Theory''. Oxford University Press, 1990. （ウェブサイト で閲覧可能） 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「ペール・マルティン＝レーフ」の詳細全文を読む スポンサード リンク
|