HOME
The Info List - Per Martin-Löf


--- Advertisement ---



Per Erik Rutger Martin-Löf (/ˈmɑːrtɪn lɒf/;[1] Swedish: [ˈmaʈiːn ˈløːv];[2] born May 8, 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.[3] Until his retirement in 2009,[4] Per Martin-Löf
Per Martin-Löf
held a joint chair for Mathematics and Philosophy
Philosophy
at Stockholm University.[5] His brother Anders Martin-Löf
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
Per Martin-Löf
has influenced statistical theory, especially concerning exponential families, the expectation-maximization method for missing data, and model selection.[6] Per Martin-Löf
Per Martin-Löf
is an enthusiastic bird-watcher; his first scientific publication was on the mortality rates of ringed birds.[7]

Contents

1 Randomness and Kolmogorov complexity 2 Mathematical statistics

2.1 Bird-watching and sex determination 2.2 Probability
Probability
on algebraic structures 2.3 Statistical models

2.3.1 Model selection
Model selection
and hypothesis testing 2.3.2 Expectation maximization method
Expectation maximization method
for exponential families

3 Logic

3.1 Philosophical logic 3.2 Type theory

4 Awards 5 See also 6 Notes 7 References

7.1 Bird watching
Bird watching
and missing data 7.2 Probability
Probability
foundations 7.3 Probability
Probability
on algebraic structures, following Ulf Grenander 7.4 Statistics
Statistics
foundations 7.5 Foundations of mathematics, logic, and computer science

8 External links

Randomness and Kolmogorov complexity[edit] Main article: Algorithmically random sequence See also: Kolmogorov complexity
Kolmogorov complexity
and Algorithmic information theory In 1964 and 1965, Martin-Löf studied in Moscow under the supervision of Andrei N. Kolmogorov. He wrote a 1966 article On the definition of random sequences that gave the first suitable definition of a random sequence. Earlier researchers such as Richard von Mises
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 define formally 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 satisfies 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 impossible 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.[8] 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
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). Mathematical statistics[edit] Per Martin-Löf
Per Martin-Löf
has done important research in mathematical statistics, which (in the Swedish tradition) includes probability theory and statistics. Bird-watching and sex determination[edit]

The Dunlin
Dunlin
(Calidris alpina)

See also: Bird watching, Bird ringing, Mark and recapture, and Ornithology Per Martin-Löf
Per Martin-Löf
began bird watching in his youth and remains an enthusiastic bird-watcher.[9] 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.[7][10] 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
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. Probability
Probability
on algebraic structures[edit] See also: probability distribution, harmonic analysis, Haar measure, Laplace transform, and semigroup Martin-Löf wrote a licenciate thesis on probability on algebraic structures, particularly semigroups, a research program led by Ulf Grenander at Stockholm University.[11][12][13] Statistical models[edit] See also: Exponential family and Statistical model 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 considers only finite samples.[14] Much of Martin-Löf's work in statistics was to provide a finite-sample foundation for statistics. Model selection
Model selection
and hypothesis testing[edit]

The steps of the EM algorithm
EM algorithm
on a two component Gaussian mixture model on the Old Faithful
Old Faithful
dataset

See also: Model selection, Sufficient statistic, hypothesis test, and Exact test In the 1970s, Per Martin-Löf
Per Martin-Löf
made important contributions to statistical theory and inspired further research, especially by Scandinavian statisticians including 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).[14] Expectation maximization method
Expectation maximization method
for exponential families[edit] See also: Missing data
Missing data
and Expectation maximization
Expectation maximization
method 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.[15][16][17][18] 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 the Royal Statistical Society.[19] Logic[edit]

Franz Brentano

Philosophical logic[edit] See also: Logical consequence, Entailment, Analytic philosophy, Continental philosophy, Intuitionism, and Phenomenology (philosophy) In philosophical logic, Per Martin-Löf
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. Type theory[edit] Main article: Type theory See also: Intuitionistic type theory, Proof-theoretic semantics, and Dependent type 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
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, 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, Epigram and Idris. Awards[edit] Martin-Löf is a member of the Royal Swedish Academy of Sciences[20] and of the Academia Europaea.[5] See also[edit]

Franz Brentano Rudolf Carnap Michael Dummett Gottlob Frege Ulf Grenander Jaakko Hintikka Edmund Husserl Andrei N. Kolmogorov Anders Martin-Löf John von Neumann Peter Pagin Dag Prawitz Charles Sanders Peirce Frank P. Ramsey Bertrand Russell Dana Scott Alfred Tarski Alan Turing

Notes[edit]

^ Does HoTT Provide a Foundation for Mathematics? by James Ladyman (University of Bristol, UK) ^ Peter Dybjer on types and testing – The Type Theory Podcast ^ See e.g. Nordström, Bengt; Petersson, Kent; Smith, Jan M. (1990), Programming in Martin-Löf ’s Type Theory: An Introduction (PDF), Oxford University Press . ^ Philosophy
Philosophy
and Foundations of Mathematics: Epistemological and Ontological Aspects. A conference dedicated to Per Martin-Löf
Per Martin-Löf
on the occasion of his retirement Archived 2014-02-02 at the Wayback Machine.. Swedish Collegium for Advanced Study, Uppsala, May 5–8, 2009. Retrieved 2014-01-26. ^ a b Member profile, Academia Europaea, retrieved 2014-01-26. ^ For details, see the #Statistical models section of this article. ^ a b Martin-Löf (1961). ^ Jean-Paul Delahaye, Randomness, Unpredictability and Absence of Order, in Philosophy
Philosophy
of Probability, p. 145–167, Springer 1993. ^ George A. Barnard, "Gone Birdwatching", New Scientist, 4 December 1999, magazine issue 2215. ^ S. M. Taylor (1966). "Recent Quantitative Work on British Bird Populations. A Review". Journal of the Royal Statistical Society, Series D. 16 (=No. 2): 119–170. JSTOR 2986734.  ^ Martin-Löf, P. The continuity theorem on a locally compact group. Teor. Verojatnost. i Primenen. 10 1965 367–371. ^ Martin-Löf, Per Probability
Probability
theory on discrete semigroups. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 4 1965 78–102 ^ Nitis Mukhopadhyay. A Conversation with Ulf Grenander. Statist. Sci. Volume 21, Number 3 (2006), 404–426. ^ a b Kolmogorov, Andrei N. (1963). "On Tables of Random Numbers". Sankhyā Ser. A. 25: 369–375.  ^ Rolf Sundberg. 1971. Maximum likelihood theory and applications for distributions generated when observing a function of an exponential family variable. Dissertation, Institute for Mathematical Statistics, Stockholm University. ^ Anders Martin-Löf. 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Evaluation of lifetimes in time-lengths below one nanosecond"). ("Sundberg formula") ^ Per Martin-Löf. 1966. Statistics
Statistics
from the point of view of statistical mechanics. Lecture notes, Mathematical Institute, Aarhus University. ("Sundberg formula" credited to Anders Martin-Löf). ^ Per Martin-Löf. 1970. Statistika Modeller (Statistical Models): Anteckningar fran seminarier läsåret 1969–1970 (Notes from seminars in the academic year 1969–1970), with the assistance of Rolf Sundberg. Stockholm University. ("Sundberg formula") ^ Dempster, A.P.; Laird, N.M.; Rubin, D.B. (1977). "Maximum Likelihood from Incomplete Data via the EM Algorithm". Journal of the Royal Statistical Society, Series B. 39 (1): 1–38. JSTOR 2984875. MR 0501537.  ^ "The Royal Swedish Academy of Sciences: Per Martin-Löf". Retrieved 2009-05-01. [dead link]

References[edit] Bird watching
Bird watching
and missing data[edit]

Martin-Löf, P. (1961). "ringed birds". Arkiv för Zoologi (Zoology files), Kungliga Svenska Vetenskapsakademien (The Royal Swedish Academy of Sciences) Serie 2. Band 13 (21). 

George A. Barnard, "Gone Birdwatching", New Scientist, 4 December 1999, magazine issue 2215. Seber, G.A.F. The Estimation of Animal Abundance and Related Parameters. Caldwel, New Jersey: Blackburn Press. ISBN 1-930665-55-5.  Royle, J. A.; R. M. Dorazio (2008). Hierarchical Modeling and Inference in Ecology. Elsevier. ISBN 1-930665-55-5. 

Probability
Probability
foundations[edit]

Per Martin-Löf. "The Definition of Random Sequences." Information and Control, 9(6): 602–619, 1966. Li, Ming and Vitányi, Paul, An Introduction to Kolmogorov Complexity and Its Applications, Springer, 1997. Introduction chapter full-text.

Probability
Probability
on algebraic structures, following Ulf Grenander[edit]

Grenander, Ulf. Probability
Probability
on Algebraic Structures. (Dover reprint) Martin-Löf, P. The continuity theorem on a locally compact group. Teor. Verojatnost. i Primenen. 10 1965 367—371. Martin-Löf, Per. Probability
Probability
theory on discrete semigroups. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 4 1965 78—102 Nitis Mukhopadhyay. "A Conversation with Ulf Grenander". Statist. Sci. Volume 21, Number 3 (2006), 404–426.

Statistics
Statistics
foundations[edit]

Anders Martin-Löf. 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Evaluation of lifetimes in time-lengths below one nanosecond"). ("Sundberg formula", according to Sundberg 1971) Per Martin-Löf. 1966. Statistics
Statistics
from the point of view of statistical mechanics. Lecture notes, Mathematical Institute, Aarhus University. ("Sundberg formula" credited to Anders Martin-Löf, according to Sundberg 1971) Per Martin-Löf. 1970. Statistika Modeller (Statistical Models): Anteckningar fran seminarier läsåret 1969–1970 (Notes from seminars in the academic year 1969–1970), with the assistance of Rolf Sundberg. Stockholm University. Martin-Löf, P. "Exact tests, confidence regions and estimates", with a discussion by A. W. F. Edwards, G. A. Barnard, D. A. Sprott, O. Barndorff-Nielsen, D. Basu
D. Basu
and G. Rasch. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), pp. 121–138. Memoirs, No. 1, Dept. Theoret. Statist., Inst. Math., Univ. Aarhus, Aarhus, 1974. Martin-Löf, P. Repetitive structures and the relation between canonical and microcanonical distributions in statistics and statistical mechanics. With a discussion by D. R. Cox
D. R. Cox
and G. Rasch and a reply by the author. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), pp. 271–294. Memoirs, No. 1, Dept. Theoret. Statist., Inst. Math., Univ. Aarhus, Aarhus, 1974. Martin-Löf, P. The notion of redundancy and its use as a quantitative measure of the deviation between a statistical hypothesis and a set of observational data. With a discussion by F. Abildgård, A. P. Dempster, D. Basu, D. R. Cox, A. W. F. Edwards, D. A. Sprott, G. A. Barnard, O. Barndorff-Nielsen, J. D. Kalbfleisch and G. Rasch and a reply by the author. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), pp. 1–42. Memoirs, No. 1, Dept. Theoret. Statist., Inst. Math., Univ. Aarhus, Aarhus, 1974. Martin-Löf, Per The notion of redundancy and its use as a quantitative measure of the discrepancy between a statistical hypothesis and a set of observational data. Scand. J. Statist. 1 (1974), no. 1, 3—18. Sverdrup, Erling. "Tests without power." Scand. J. Statist. 2 (1975), no. 3, 158—160. Martin-Löf, Per Reply to Erling Sverdrup's polemical article: ``Tests without power (Scand. J. Statist. 2 (1975), no. 3, 158–160). Scand. J. Statist. 2 (1975), no. 3, 161–165. Sverdrup, Erling. A rejoinder to: ``Tests without power (Scand. J. Statist. 2 (1975), 161—165) by P. Martin-Löf. Scand. J. Statist. 4 (1977), no. 3, 136—138. Martin-Löf, P. Exact tests, confidence regions and estimates. Foundations of probability and statistics. II. Synthese 36 (1977), no. 2, 195—206. Rolf Sundberg. 1971. Maximum likelihood theory and applications for distributions generated when observing a function of an exponential family variable. Dissertation, Institute for Mathematical Statistics, Stockholm University. Sundberg, Rolf. Maximum likelihood theory for incomplete data from an exponential family. Scand. J. Statist. 1 (1974), no. 2, 49—58. Sundberg, Rolf An iterative method for solution of the likelihood equations for incomplete data from exponential families. Comm. Statist.—Simulation Comput. B5 (1976), no. 1, 55—64. Sundberg, Rolf Some results about decomposable (or Markov-type) models for multidimensional contingency tables: distribution of marginals and partitioning of tests. Scand. J. Statist. 2 (1975), no. 2, 71—79. Höglund, Thomas. The exact estimate — a method of statistical estimation. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 29 (1974), 257—271. Lauritzen, Steffen L. Extremal families and systems of sufficient statistics. Lecture Notes in Statistics, 49. Springer-Verlag, New York, 1988. xvi+268 pp. ISBN 0-387-96872-5

Foundations of mathematics, logic, and computer science[edit]

Per Martin-Löf. A theory of types. Preprint, Stockholm University, 1971. Per Martin-Löf. An intuitionistic theory of types. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998. Reprinted version of an unpublished report from 1972. Per Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic
Logic
Colloquium ‘73, pages 73–118. North Holland, 1975. Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy
Philosophy
of Science VI, 1979. Eds. Cohen, et al. North-Holland, Amsterdam. pp. 153–175, 1982. Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984. Per Martin-Löf. Philosophical implications of type theory, Unpublished notes, 1987? Per Martin-Löf. Substitution calculus, 1992. Notes from a lecture given in Göteborg. Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990. (The book is out of print, but a free version has been made available.) Per Martin-Löf. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic, 1(1): 11–60, 1996.

External links[edit]

Per Martin-Löf
Per Martin-Löf
at the Mathematics Genealogy Project

Authority control

WorldCat Identities VIAF: 92134760 LCCN: n86081083 ISNI: 0000 0001 2030 6590 GND: 122298624 SUDOC: 086109774 BNF: cb123858392 (data) BIBSYS: 90387800 MGP: 2

.