佩爾·馬丁-洛夫

佩爾·埃里克·羅格·馬丁-洛夫（Template:Langx，1942年5月8日—），瑞典邏輯學家、數理統計學家和哲學家。他以其在概率論基礎方面的工作而聞名。自20世紀70年代以後，他的工作主要集中在邏輯學方面。在哲學邏輯方面，他的研究專注於蘊涵及判斷學說，並在一定程度上受到了弗朗茲·布倫塔諾、弗雷格和胡塞爾先前工作的影響；在數理邏輯方面，他致力於創設直覺類型論作為數學的構造性基礎。馬丁-洛夫在類型論方面的工作深深地影響了計算機科學、尤其是後世程式語言理論的發展。

佩爾·馬丁-洛夫是斯德哥爾摩大學的校友。直到2009年退休前，他一直擔任斯德哥爾摩大學的數學和哲學學院的聯合主席這一職務。

他的長兄安德斯·馬丁-洛夫（Template:Langx）是斯德哥爾摩大學的數理統計學榮譽教授；兩人曾在概率論和數理統計的研究上展開合作，其研究成果包括指數族非線性模型、最大期望算法和模型選擇等，廣泛地影響了統計學理論的發展。

佩爾·馬丁-洛夫還是一個業餘的鳥類觀測家，他發表的第一篇科學論文即是關於鳥類遷徙活動中存活率的統計學研究。

隨機性和柯氏複雜性

在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等。

榮譽

佩爾·馬丁-洛夫是瑞典皇家科學院以及歐洲科學院（Academia Europaea）的院士。

參見

• 直覺類型論
• 依賴類型
• 數學結構主義
• 安德雷·柯爾莫哥洛夫

外部連結

• 佩爾·馬丁-洛夫在數學家族譜網站上的條目 （頁面存檔備份，存於網際網路檔案館）