| Per Martin-Löf | |
|---|---|
Per Martin-Löf in 2004
|
|
| Born | May 8, 1942 |
| Citizenship | Sweden |
| Nationality | Swedish |
| Fields | Computer Science Logic Mathematical statistics Philosophy |
| Institutions | Stockholm University University of Chicago Aarhus University |
| Alma mater | Stockholm University |
| Doctoral advisor | Andrei N. Kolmogorov |
| Known for | Random sequences Exact tests Repetitive structure Sufficient statistics Expectation maximization method Type theory |
| Notable awards | Royal Swedish Academy of Sciences |
Per Erik Rutger Martin-Löf (born 1942) is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer science. Since the late 1970s, Martin-Löf's publications have been mainly in logic. In philosophical logic, Martin-Löf has wrestled with the philosophy of logical consequence and judgment, partly inspired by the work of Brentano, Frege, and Husserl. In mathematical logic, Martin-Löf has been active in developing intuitionistic type theory as a constructive foundation of mathematics; Martin-Löf's work on type theory has influenced computer science.
Per Martin-Löf holds a joint chair for Mathematics and Philosophy at Stockholm University.
His brother Anders Martin-Löf is now emeritus professor of mathematical statistics at Stockholm University; the two brothers have collaborated in research in probability and statistics. The research of Anders and Per Martin-Löf has influenced statistical theory, especially regarding exponential families, the expectation-maximization method for missing data, and model selection.
Per Martin-Löf is an enthusiastic bird-watcher, whose first scientific publication was on the mortality rates of ringed birds.
Contents |
In 1964–65 Martin-Löf was studying in Moscow under the supervision of Andrei N. Kolmogorov. During this time, Martin-Löf wrote his 1966 article On the definition of random sequences, which gave the first suitable definition of a random sequence.
Earlier researchers such as Richard von Mises had attempted to formalize the notion of a test for randomness in order to define a random sequence as one that passed all tests for randomness; however, the precise notion of a randomness test was left vague. Martin-Löf's key insight was to use the theory of computation to formally define the notion of a test for randomness. This contrasts with the idea of randomness in probability; in that theory, no particular element of a sample space can be said to be random.
Martin-Löf randomness has since been shown to admit many equivalent characterizations—in terms of compression, randomness tests, and gambling – that bear little outward resemblance to the original definition, but each of which satisfy our intuitive notion of properties that random sequences ought to have: random sequences should be incompressible, they should pass statistical tests for randomness, and it should be difficult to make money betting on them. The existence of these multiple definitions of Martin-Löf randomness, and the stability of these definitions under different models of computation, give evidence that Martin-Löf randomness is a fundamental property of mathematics and not an accident of Martin-Löf's particular model. The thesis that the definition of Martin-Löf randomness "correctly" captures the intuitive notion of randomness has been called the "Martin-Löf-Chaitin Thesis"; it is somewhat similar to the Church–Turing thesis.[1]
Following Martin-Löf's work, algorithmic information theory defines a random string as one that cannot be produced from any computer program that is shorter than the string (Chaitin–Kolmogorov randomness); i.e. a string whose Kolmogorov complexity is at least the length of the string. This is a different meaning from the usage of the term in statistics. Whereas statistical randomness refers to the process that produces the string (e.g. flipping a coin to produce each bit will randomly produce a string), algorithmic randomness refers to the string itself. Algorithmic information theory separates random from nonrandom strings in a way that is relatively invariant to the model of computation being used.
An algorithmically random sequence is an infinite sequence of characters, all of whose prefixes (except possibly a finite number of exceptions) are strings that are "close to" algorithmically random (their length is within a constant of their Kolmogorov complexity).
Per Martin-Löf has done important research in mathematical statistics, which (in the Swedish tradition) includes probability theory and statistics.
Per Martin-Löf began bird watching in his youth and remains an enthusiastic bird-watcher.[2] As a teenager, he published an article on estimating the mortality rates of birds, using data from bird ringing, in a Swedish zoological journal: This paper was soon cited in leading international journals, and this paper continues to be cited.[3][4]
In the biology and statistics of birds, there are several problems of missing data. Martin-Löf's first paper discussed the problem of estimating the mortality rates of the Dunlin species, using capture-recapture methods. A second problem of missing data arises with studying the sex of birds. The problem of determining the biological sex of a bird, which is extremely difficult for humans, is one of the first examples in Martin-Löf's lectures on statistical models.
Martin-Löf wrote a licenciate thesis on probability on algebraic structures, particularly semigroups, a research program led by Ulf Grenander at Stockholm University.[5][6][7]
Martin-Löf developed innovative approaches to statistical theory. In his paper "On Tables of Random Numbers", Kolmogorov observed that the frequency probability notion of the limiting properties of infinite sequences failed to provide a foundation for statistics, which only considers finite samples.[8] Much of Martin-Löf's work in statistics was to provide a finite-sample foundation for statistics.
In the 1970s, Per Martin-Löf made important contributions to statistical theory and inspired further research, especially by Scandinavian statisticians like Rolf Sundberg, Thomas Höglund, and Steffan Lauritzen. In this work, Martin-Löf's previous research on probability measures on semigroups led to a notion of "repetitive structure" and a novel treatment of sufficient statistics, in which one-parameter exponential families were characterized. He provided a category-theoretic approach to nested statistical models, using finite-sample principles. Before (and after) Martin-Löf, such nested models have often been tested using chi-square hypothesis tests, whose justifications are only asymptotic (and so irrelevant to real problems, which always have finite samples [9]).
Martin-Löf's student, Rolf Sundberg, developed a detailed analysis of the expectation-maximization (EM) method for estimation using data from exponential families, especially with missing data. Sundberg credits a formula, later known as the Sundberg formula, to previous manuscripts of the Martin-Löf brothers, Per and Anders.[10][11][12][13] Many of these results reached the international scientific community through the 1976 paper on the expectation maximization (EM) method by Arthur P. Dempster, Nan Laird, and Donald Rubin, which was published in a leading international journal, sponsored by Royal Statistical Society.[14]
In philosophical logic, Per Martin-Löf has published papers on the theory of logical consequence, on judgments, etc. He has been interested in Central-European philosophical traditions, especially of the German-language writings of Franz Brentano, Gottlob Frege, and of Edmund Husserl.
Martin-Löf has worked in mathematical logic for many decades.
From 1968 to '69 he worked as an Assistant Professor at the University of Chicago where he met William Alvin Howard with whom he discussed issues related to the Curry–Howard correspondence. Martin-Löf's first draft article on type theory dates back to 1971. This impredicative theory generalized Girard's System F. However, this system turned out to be inconsistent due to Girard's paradox which was discovered by Girard when studying System U, an inconsistent extension of System F. This experience led Per Martin-Löf to develop the philosophical foundations of type theory, his meaning explanation, a form of proof-theoretic semantics, which justifies predicative type theory as presented in his 1984 Bibliopolis book, and extended in a number of increasingly philosophical texts, such as his influential On the Meanings of the Logical Constants and the Justifications of the Logical Laws.
The 1984 type theory was extensional while the type theory presented in the book by Nordström et al. in 1990, which was heavily influenced by his later ideas, was intensional and more amenable to being implemented on a computer.
Martin-Löf's intuitionistic type theory developed the notion of dependent types and directly influenced the development of the calculus of constructions and the logical framework LF. A number of popular computer-based proof systems are based on type theory, for example NuPRL, LEGO, Coq, ALF, Agda, Twelf and Epigram.
Martin-Löf is a member of the Royal Swedish Academy of Sciences.[15]