佩爾·馬丁-洛夫
佩爾·埃里克·羅格·馬丁-洛夫（瑞典語：Per Erik Rutger Martin-Löf，1942年5月8日—），瑞典邏輯學家、數理統計學家和哲學家。他以其在概率論基礎方面的工作而聞名。自20世紀70年代以後，他的工作主要集中在邏輯學方面。在哲學邏輯方面，他的研究專注於蘊涵及判斷學說，並在一定程度上受到了弗朗茲·布倫塔諾、弗雷格和胡塞爾先前工作的影響；在數理邏輯方面，他致力於創設直覺類型論作為數學的構造性基礎。馬丁-洛夫在類型論方面的工作深深地影響了計算機科學、尤其是後世編程語言理論的發展。[1]
| 佩爾·馬丁-洛夫 Per Martin-Löf | |
|---|---|
 馬丁-洛夫（2004年） | |
| 出生 | 1942年5月8日 瑞典斯德哥爾摩 |
| 國籍 | 瑞典 |
| 母校 | 斯德哥爾摩大學 |
| 知名於 | 隨機序列 精確檢驗 重複結構 充分統計量 最大期望算法 類型論 |
| 獎項 | 瑞典皇家科學院 |
| 科學生涯 | |
| 研究領域 | 計算機科學 邏輯 數理統計學 哲學 |
| 機構 | 斯德哥爾摩大學 芝加哥大學 奧胡斯大學 |
| 博士導師 | 安德雷·柯爾莫哥洛夫 |
佩爾·馬丁-洛夫是斯德哥爾摩大學的校友。直到2009年退休前[2]，他一直擔任斯德哥爾摩大學的數學和哲學學院的聯合主席這一職務。[3]
他的長兄安德斯·馬丁-洛夫（瑞典語：Anders Martin-Löf）是斯德哥爾摩大學的數理統計學榮譽教授；兩人曾在概率論和數理統計的研究上展開合作，其研究成果包括指數族非線性模型、最大期望算法和模型選擇等，廣泛地影響了統計學理論的發展。
隨機性和柯氏複雜性
在1964年到1965年間，馬丁-洛夫曾在莫斯科大學學習，師從柯爾莫哥洛夫。在1966年發表的論文On the definition of random sequences中，他首次給出隨機序列的確切定義。
早期的研究者如理查德·馮·米澤斯曾嘗試形式化隨機性測試的概念，用以定義一個可通過所有隨機性測試的序列為隨機序列；然而，隨機性測試的確切概念仍未清晰。而馬丁-洛夫的開創性地運用了計算理論來形式化定義隨機性測試這一概念。該方法與概率論中對隨機性的定義大異其趣；在概率論中，取樣空間中任何一個特定的元素均不可能是隨機的。
在馬丁-洛夫工作的啟發之下，後來的算法信息論將所謂「隨機字符串」定義為一個不能夠被任何短於該字符串的計算機程序生成的字符串（蔡廷-柯爾莫哥洛夫隨機性），即一個柯氏複雜性不小於自身長度的字符串。由於統計學上的隨機性通常只關心產生字符串的過程，而算法隨機性關心的是字符串的內在性質。由此，算法信息論第一次明確地將「隨機」和「非隨機」、藉由計算模型中的概念區分開了。
數理統計學
邏輯學
哲學邏輯學
在哲學邏輯方面，馬丁-洛夫發表過關於蘊涵理論、判斷學說等方面的著作。他的研究興趣根植於中歐的哲學傳統，尤其是德語學者如弗朗茲·布倫塔諾、弗雷格，以及胡塞爾的哲學理論。
類型論
馬丁-洛夫長期從事數理邏輯的研究。
在1968年到1969年間，他在美國芝加哥大學擔任助理教授期間結識了邏輯學家威廉·霍華德（William Alvin Howard），並共同探討了後來被稱之為柯里-霍華德同構（Curry–Howard correspondence）的論題。馬丁-洛夫在1971年完成了他最初的關於類型論研究的初稿，所提出的理論是非直謂性的，將吉拉德（Jean-Yves Girard）的系統F進行了一般化。然而，隨後由于吉拉德在研究系統U之後發現了吉拉德悖論，導致該理論不再廣泛適用。這激發了馬丁-洛夫對於類型論哲學基礎的研究。
馬丁-洛夫開創的直覺類型論提出了依賴類型的概念，直接啟發了構造演算（CoC）與LF邏輯框架的建立。一些流行的計算機證明系統和程序語言在此基礎上得以開發，包括：Coq、Agda、NuPRL、LEGO、Twelf 和 Epigram等。
榮譽
參考文獻
- ^ See e.g. Nordström, Bengt; Petersson, Kent; Smith, Jan M., Programming in Martin-Löf ’s Type Theory: An Introduction (PDF), Oxford University Press, 1990 [2014-07-19], （原始內容存檔 (PDF)於2016-03-04）.
- ^ Philosophy and Foundations of Mathematics: Epistemological and Ontological Aspects. A conference dedicated to Per Martin-Löf on the occasion of his retirement （頁面存檔備份，存於網際網路檔案館）. Swedish Collegium for Advanced Study, Uppsala, May 5-8, 2009. Retrieved 2014-01-26.
- ^ 3.0 3.1 Member profile （頁面存檔備份，存於網際網路檔案館）, Academia Europaea, retrieved 2014-01-26. 引用錯誤：帶有name屬性「ae」的
<ref>標籤用不同內容定義了多次 - ^ Martin-Löf, P. Mortality rate calculations on ringed birds with special reference to the Dunlin Calidris alpina. Arkiv för Zoologi (Zoology files), Kungliga Svenska Vetenskapsakademien (The Royal Swedish Academy of Sciences) Serie 2. 1961,. Band 13 (21).
- ^ Dempster, A.P.; Laird, N.M.; Rubin, D.B. Maximum Likelihood from Incomplete Data via the EM Algorithm. Journal of the Royal Statistical Society, Series B. 1977, 39 (1): 1–38. JSTOR 2984875. MR 0501537.
- ^ The Royal Swedish Academy of Sciences: Per Martin-Löf. [2009-05-01]. （原始內容存檔於2020-09-22）.