随机性和柯氏复杂性

在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）的院士。

参见

直觉类型论

依赖类型

数学结构主义

安德雷·柯尔莫哥洛夫

免责声明：以上内容版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。感谢每一位辛勤著写的作者，感谢每一位的分享。