ペール・マルティン=レーフ

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索
ペール・マルティン=レーフ

ペール・マルティン=レーフ (Per Martin-Löf, 1942年 - ) はスウェーデン論理学者、哲学者、数学者直観主義型理論の創案者として知られ、現在はストックホルム大学数学部および哲学部の教授を務めている。

1964年から1965年にかけてモスクワアンドレイ・コルモゴロフのもとで学び、ランダム系列に関する研究[1]を行う。1968年から1969年にかけてはシカゴ大学助教授を務め、ここでウィリアム・ハワードカリー=ハワード対応に関して議論している。1971年には型理論に関する最初の草稿を書き上げているが、この最初の非可述体系はジャン=イヴ・ジラールによって矛盾していることが示された(ジラールのパラドックス)。これをきっかけに型理論の概念的基礎の探求へと導かれていったマルティン=レーフは、1984年の著作[2]で提示した可述型理論を正当化するための証明論的意味論を展開し、またこれに関連していくつかの哲学的著作[3][4]も発表している。

彼の直観主義型理論は依存型 (dependent type) の概念を発展させたことで知られており、これは後の calculus of construction 等に影響を与えた。また、Nuprl をはじめとして、マルティン=レーフの型理論に基づいた自動証明システムも開発されている。マルティン=レーフの業績は今なお論理学および理論計算機科学の研究にインスピレーションを与え続けており、彼のアイデアが持つ可能性はいまだに汲み尽くされていないといえる。

出典・参考文献[編集]

  1. ^ Per Martin-Löf, "The definition of random sequences," Information and Control, Vol.9, pp. 602-619, 1966.
  2. ^ Per Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984 (ISBN 8870881059).
  3. ^ 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.
  4. ^ 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).
  • Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990. (ウェブサイトで閲覧可能)