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