佩尔·马丁-洛夫
佩尔·埃里克·罗格·马丁-洛夫（瑞典语：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）.