Loading AI tools
来自维基百科，自由的百科全书
佩爾·埃里克·羅格·馬丁-洛夫（瑞典語：Per Erik Rutger Martin-Löf，1942年5月8日—），瑞典邏輯學家、數理統計學家和哲學家。他以其在概率論基礎方面的工作而聞名。自20世紀70年代以後，他的工作主要集中在邏輯學方面。在哲學邏輯方面，他的研究專注於蘊涵及判斷學說，並在一定程度上受到了弗朗茲·布倫塔諾、弗雷格和胡塞爾先前工作的影響；在數理邏輯方面，他致力於創設直覺類型論作為數學的構造性基礎。馬丁-洛夫在類型論方面的工作深深地影響了計算機科學、尤其是後世程式語言理論的發展。[1]
佩爾·馬丁-洛夫是斯德哥爾摩大學的校友。直到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等。
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
