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

提供: miniwiki
2018/8/19/ (日) 17:38時点におけるAdmin (トーク | 投稿記録)による版 (1版 をインポートしました)
(差分) ← 古い版 | 最新版 (差分) | 新しい版 → (差分)
移動先:案内、検索
ファイル:Per MartinLoef.jpg
ペール・マルティン＝レーフ

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

経歴

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

直観主義的型理論（intuitionistic type theory）

彼の直観主義的型理論は依存型 (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).

参考文献

関連項目



「http:///http:///mymemo.xyz/mymemo.xyz/wiki/index.php?title=ペール・マルティン＝レーフ&oldid=114388」から取得