Per Martin-Löf
Encyclopedia
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
.
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
.
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).
, 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. As a teenager, he published an article on estimating the mortality rate
s 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.
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 model
s.
at Stockholm University.
. 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. Much of Martin-Löf's work in statistics was to provide a finite-sample foundation for statistics.
were characterized. He provided a category-theoretic
approach to nested
statistical model
s, 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 ).
. 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
.
, 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
.
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 type
s 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.
Sweden
Sweden , officially the Kingdom of Sweden , is a Nordic country on the Scandinavian Peninsula in Northern Europe. Sweden borders with Norway and Finland and is connected to Denmark by a bridge-tunnel across the Öresund....
logician, philosopher, and mathematical statistician
Mathematical statistics
Mathematical statistics is the study of statistics from a mathematical standpoint, using probability theory as well as other branches of mathematics such as linear algebra and analysis...
. 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
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
. In philosophical logic
Philosophical logic
Philosophical logic is a term introduced by Bertrand Russell to represent his idea that the workings of natural language and thought can only be adequately represented by an artificial language; essentially it was his formalization program for the natural language...
, Martin-Löf has wrestled with the philosophy of logical consequence and judgment, partly inspired by the work of Brentano
Franz Brentano
Franz Clemens Honoratus Hermann Brentano was an influential German philosopher and psychologist whose influence was felt by other such luminaries as Sigmund Freud, Edmund Husserl, Kazimierz Twardowski and Alexius Meinong, who followed and adapted his views.-Life:Brentano was born at Marienberg am...
, Frege
Gottlob Frege
Friedrich Ludwig Gottlob Frege was a German mathematician, logician and philosopher. He is considered to be one of the founders of modern logic, and made major contributions to the foundations of mathematics. He is generally considered to be the father of analytic philosophy, for his writings on...
, and Husserl
Edmund Husserl
Edmund Gustav Albrecht Husserl was a philosopher and mathematician and the founder of the 20th century philosophical school of phenomenology. He broke with the positivist orientation of the science and philosophy of his day, yet he elaborated critiques of historicism and of psychologism in logic...
. In mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, Martin-Löf has been active in developing intuitionistic type theory
Intuitionistic type theory
Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
as a constructive foundation of mathematics; Martin-Löf's work on type theory has influenced computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
.
Per Martin-Löf holds a joint chair for Mathematics and Philosophy at Stockholm University
Stockholm University
Stockholm University is a state university in Stockholm, Sweden. It has over 28,000 students at four faculties, making it one of the largest universities in Scandinavia. The institution is also frequently regarded as one of the top 100 universities in the world...
.
His brother Anders Martin-Löf
Anders Martin-Löf
Anders Martin-Löf is a Swedish physicist and mathematician. He is a professor in insurance mathematics and mathematical statistics since 1987 at the Department of Mathematics of Stockholm University....
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
Model selection
Model selection is the task of selecting a statistical model from a set of candidate models, given data. In the simplest cases, a pre-existing set of data is considered...
.
Per Martin-Löf is an enthusiastic bird-watcher, whose first scientific publication was on the mortality rates of ringed birds
Bird ringing
Bird ringing or bird banding is a technique used in the study of wild birds, by attaching a small, individually numbered, metal or plastic tag to their legs or wings, so that various aspects of the bird's life can be studied by the ability to re-find the same individual later...
.
Randomness and Kolmogorov complexity
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
Theory of computation
In theoretical computer science, the theory of computation is the branch that deals with whether and how efficiently problems can be solved on a model of computation, using an algorithm...
to formally define the notion of a test for randomness. This contrasts with the idea of randomness in probability
Probability
Probability is ordinarily used to describe an attitude of mind towards some proposition of whose truth we arenot certain. The proposition of interest is usually of the form "Will a specific event occur?" The attitude of mind is of the form "How certain are we that the event will occur?" The...
; 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
Data compression
In computer science and information theory, data compression, source coding or bit-rate reduction is the process of encoding information using fewer bits than the original representation would use....
, randomness tests, and gambling
Gambling
Gambling is the wagering of money or something of material value on an event with an uncertain outcome with the primary intent of winning additional money and/or material goods...
– 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
Gregory Chaitin
Gregory John Chaitin is an Argentine-American mathematician and computer scientist.-Mathematics and computer science:Beginning in 2009 Chaitin has worked on metabiology, a field parallel to biology dealing with the random evolution of artificial software instead of natural software .Beginning in...
Thesis"; it is somewhat similar to the Church–Turing thesis
Church–Turing thesis
In computability theory, the Church–Turing thesis is a combined hypothesis about the nature of functions whose values are effectively calculable; in more modern terms, algorithmically computable...
.
Following Martin-Löf's work, algorithmic information theory
Algorithmic information theory
Algorithmic information theory is a subfield of information theory and computer science that concerns itself with the relationship between computation and information...
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
In algorithmic information theory , the Kolmogorov complexity of an object, such as a piece of text, is a measure of the computational resources needed to specify the object...
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
Model of computation
In computability theory and computational complexity theory, a model of computation is the definition of the set of allowable operations used in computation and their respective costs...
being used.
An algorithmically random sequence
Algorithmically random sequence
Intuitively, an algorithmically random sequence is an infinite sequence ofbinary digits that appears random to any algorithm...
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
Per Martin-Löf has done important research in mathematical statisticsMathematical statistics
Mathematical statistics is the study of statistics from a mathematical standpoint, using probability theory as well as other branches of mathematics such as linear algebra and analysis...
, which (in the Swedish tradition) includes probability theory
Probability theory
Probability theory is the branch of mathematics concerned with analysis of random phenomena. The central objects of probability theory are random variables, stochastic processes, and events: mathematical abstractions of non-deterministic events or measured quantities that may either be single...
and statistics
Statistics
Statistics is the study of the collection, organization, analysis, and interpretation of data. It deals with all aspects of this, including the planning of data collection in terms of the design of surveys and experiments....
.
Bird-watching and sex determination
Mortality rate
Mortality rate is a measure of the number of deaths in a population, scaled to the size of that population, per unit time...
s of birds, using data from bird ringing
Bird ringing
Bird ringing or bird banding is a technique used in the study of wild birds, by attaching a small, individually numbered, metal or plastic tag to their legs or wings, so that various aspects of the bird's life can be studied by the ability to re-find the same individual later...
, in a Swedish zoological journal: This paper was soon cited in leading international journals, and this paper continues to be cited.
In the biology
Population biology
Population biology is a study of populations of organisms, especially the regulation of population size, life history traits such as clutch size, and extinction...
and statistics
Environmental statistics
Environmental statistics is the application of statistical methods to environmental science. It covers procedures for dealing with questions concerning both the natural environment in its undistrurbed state and the interaction of humanity with the environment...
of birds
Ornithology
Ornithology is a branch of zoology that concerns the study of birds. Several aspects of ornithology differ from related disciplines, due partly to the high visibility and the aesthetic appeal 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
The Dunlin, Calidris alpina, is a small wader, sometimes separated with the other "stints" in Erolia. It is a circumpolar breeder in Arctic or subarctic regions. Birds that breed in northern Europe and Asia are long-distance migrants, wintering south to Africa, southeast Asia and the Middle East...
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 model
Statistical model
A statistical model is a formalization of relationships between variables in the form of mathematical equations. A statistical model describes how one or more random variables are related to one or more random variables. The model is statistical as the variables are not deterministically but...
s.
Probability on algebraic structures
Martin-Löf wrote a licenciate thesis on probability on algebraic structures, particularly semigroups, a research program led by Ulf GrenanderUlf Grenander
Ulf Grenander is a statistician and a professor of applied mathematics at Brown University.His early research was in probability theory, stochastic processes, time series analysis, and statistical theory...
at Stockholm University.
Statistical models
Martin-Löf developed innovative approaches to statistical theoryStatistical theory
The theory of statistics provides a basis for the whole range of techniques, in both study design and data analysis, that are used within applications of statistics. The theory covers approaches to statistical-decision problems and to statistical inference, and the actions and deductions that...
. In his paper "On Tables of Random Numbers", Kolmogorov observed that the frequency probability
Frequency probability
Frequency probability is the interpretation of probability that defines an event's probability as the limit of its relative frequency in a large number of trials. The development of the frequentist account was motivated by the problems and paradoxes of the previously dominant viewpoint, the...
notion of the limiting
Limit (mathematics)
In mathematics, the concept of a "limit" is used to describe the value that a function or sequence "approaches" as the input or index approaches some value. The concept of limit allows mathematicians to define a new point from a Cauchy sequence of previously defined points within a complete metric...
properties of infinite sequences failed to provide a foundation for statistics, which only considers finite samples. Much of Martin-Löf's work in statistics was to provide a finite-sample foundation for statistics.
Model selection and hypothesis testing
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 familiesExponential family
In probability and statistics, an exponential family is an important class of probability distributions sharing a certain form, specified below. This special form is chosen for mathematical convenience, on account of some useful algebraic properties, as well as for generality, as exponential...
were characterized. He provided a category-theoretic
Category theory
Category theory is an area of study in mathematics that examines in an abstract way the properties of particular mathematical concepts, by formalising them as collections of objects and arrows , where these collections satisfy certain basic conditions...
approach to nested
Model selection
Model selection is the task of selecting a statistical model from a set of candidate models, given data. In the simplest cases, a pre-existing set of data is considered...
statistical model
Statistical model
A statistical model is a formalization of relationships between variables in the form of mathematical equations. A statistical model describes how one or more random variables are related to one or more random variables. The model is statistical as the variables are not deterministically but...
s, 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 ).
Expectation maximization method for exponential families
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 AndersAnders Martin-Löf
Anders Martin-Löf is a Swedish physicist and mathematician. He is a professor in insurance mathematics and mathematical statistics since 1987 at the Department of Mathematics of Stockholm University....
. Many of these results reached the international scientific community through the 1976 paper on the expectation maximization (EM) method by Arthur P. Dempster
Arthur P. Dempster
Arthur Pentland Dempster is a Professor Emeritus in the Harvard University Department of Statistics. He was one of four faculty when the department was founded in 1957.He was a Putnam Fellow in 1951. He obtained his Ph.D. from Princeton University in 1956...
, Nan Laird
Nan Laird
Nan M. Laird is a professor in Biostatistics at Harvard School of Public Health. She served as Chair of the Department from 1990 to 1999. She was the Henry Pickering Walcott Professor of Biostatistics from 1991 to 1999. Laird is a Fellow of the American Statistical Association, as well as the...
, and Donald Rubin
Donald Rubin
Donald Bruce Rubin is the John L. Loeb Professor of Statistics at Harvard University. He was hired by Harvard in 1984, and served as chair of the department from 1985-1994....
, which was published in a leading international journal, sponsored by Royal Statistical Society
Royal Statistical Society
The Royal Statistical Society is a learned society for statistics and a professional body for statisticians in the UK.-History:It was founded in 1834 as the Statistical Society of London , though a perhaps unrelated London Statistical Society was in existence at least as early as 1824...
.
Philosophical logic
In philosophical logicPhilosophical logic
Philosophical logic is a term introduced by Bertrand Russell to represent his idea that the workings of natural language and thought can only be adequately represented by an artificial language; essentially it was his formalization program for the natural language...
, Per Martin-Löf has published papers on the theory of logical consequence, on judgments, etc. He has been interested in Central-European
Central Europe
Central Europe or alternatively Middle Europe is a region of the European continent lying between the variously defined areas of Eastern and Western Europe...
philosophical traditions, especially of the German-language writings of Franz Brentano
Franz Brentano
Franz Clemens Honoratus Hermann Brentano was an influential German philosopher and psychologist whose influence was felt by other such luminaries as Sigmund Freud, Edmund Husserl, Kazimierz Twardowski and Alexius Meinong, who followed and adapted his views.-Life:Brentano was born at Marienberg am...
, Gottlob Frege
Gottlob Frege
Friedrich Ludwig Gottlob Frege was a German mathematician, logician and philosopher. He is considered to be one of the founders of modern logic, and made major contributions to the foundations of mathematics. He is generally considered to be the father of analytic philosophy, for his writings on...
, and of Edmund Husserl
Edmund Husserl
Edmund Gustav Albrecht Husserl was a philosopher and mathematician and the founder of the 20th century philosophical school of phenomenology. He broke with the positivist orientation of the science and philosophy of his day, yet he elaborated critiques of historicism and of psychologism in logic...
.
Type theory
Martin-Löf has worked in mathematical logicMathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
for many decades.
From 1968 to '69 he worked as an Assistant Professor at the University of Chicago
University of Chicago
The University of Chicago is a private research university in Chicago, Illinois, USA. It was founded by the American Baptist Education Society with a donation from oil magnate and philanthropist John D. Rockefeller and incorporated in 1890...
where he met William Alvin Howard
William Alvin Howard
William Alvin Howard is a proof theorist best known for his work demonstrating formal similarity between intuitionistic logic and the simply typed lambda calculus that has come to be known as the Curry–Howard correspondence. He has also been active in the theory of proof-theoretic ordinals. He...
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
Impredicative
In mathematics and logic, impredicativity is the property of a self-referencing definition. More precisely, a definition is said to be impredicative if it invokes the set being defined, or another set which contains the thing being defined.Russell's paradox is a famous example of an impredicative...
theory generalized Girard's
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
System F
System F
System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
. However, this system turned out to be inconsistent
Consistency proof
In logic, a consistent theory is one that does not contain a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if and only if it has a model, i.e. there exists an interpretation under which all...
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
Intuitionistic type theory
Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
, his meaning explanation, a form of proof-theoretic semantics
Proof-theoretic semantics
Proof-theoretic semantics is an approach to the semantics of logic that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the proposition or logical connective plays within the system...
, which justifies predicative
Impredicative
In mathematics and logic, impredicativity is the property of a self-referencing definition. More precisely, a definition is said to be impredicative if it invokes the set being defined, or another set which contains the thing being defined.Russell's paradox is a famous example of an impredicative...
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 type
Dependent type
In computer science and logic, a dependent type is a type that depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like ATS, Agda and Epigram....
s and directly influenced the development of the calculus of constructions
Calculus of constructions
The calculus of constructions is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.-General traits:The CoC is a...
and the logical framework LF
LF (logical framework)
In logic, a logical framework provides a means to define a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for ...
. A number of popular computer-based proof systems are based on type theory, for example NuPRL
NuPRL
NuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL....
, LEGO, Coq
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
, ALF, Agda
Agda theorem prover
Agda is a proof assistant, i.e. a computer program that can check mathematical proofs. More specifically, it is an interactive system for developing constructive proofs based on the Curry-Howard correspondence in a variant of Per Martin-Löf's Type Theory. It can also be seen as a functional...
, Twelf
Twelf
Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory.-Introduction:...
and Epigram.
See also
- Franz BrentanoFranz BrentanoFranz Clemens Honoratus Hermann Brentano was an influential German philosopher and psychologist whose influence was felt by other such luminaries as Sigmund Freud, Edmund Husserl, Kazimierz Twardowski and Alexius Meinong, who followed and adapted his views.-Life:Brentano was born at Marienberg am...
- Rudolph Carnap
- Michael DummettMichael DummettSir Michael Anthony Eardley Dummett FBA D.Litt is a British philosopher. He was, until 1992, Wykeham Professor of Logic at the University of Oxford...
- Gottlob FregeGottlob FregeFriedrich Ludwig Gottlob Frege was a German mathematician, logician and philosopher. He is considered to be one of the founders of modern logic, and made major contributions to the foundations of mathematics. He is generally considered to be the father of analytic philosophy, for his writings on...
- Jaakko HintikkaJaakko HintikkaKaarlo Jaakko Juhani Hintikka is a Finnish philosopher and logician.Hintikka was born in Vantaa. After teaching for a number of years at Florida State University, Stanford, University of Helsinki, and the Academy of Finland, he is currently Professor of Philosophy at Boston University...
- Edmund HusserlEdmund HusserlEdmund Gustav Albrecht Husserl was a philosopher and mathematician and the founder of the 20th century philosophical school of phenomenology. He broke with the positivist orientation of the science and philosophy of his day, yet he elaborated critiques of historicism and of psychologism in logic...
- Andrei N. Kolmogorov
- Anders Martin-LöfAnders Martin-LöfAnders Martin-Löf is a Swedish physicist and mathematician. He is a professor in insurance mathematics and mathematical statistics since 1987 at the Department of Mathematics of Stockholm University....
- John von NeumannJohn von NeumannJohn von Neumann was a Hungarian-American mathematician and polymath who made major contributions to a vast number of fields, including set theory, functional analysis, quantum mechanics, ergodic theory, geometry, fluid dynamics, economics and game theory, computer science, numerical analysis,...
- Peter PaginPeter PaginPeter Pagin is Professor of Philosophy at Stockholm University. He is a specialist in the philosophy of language and has worked extensively on foundational issues in semantics and on technical and philosophical problems about the compositionality of meaning.-Work:One of Pagin's principal aims is...
- Dag PrawitzDag PrawitzDag Prawitz is a Swedish philosopher and logician. He is best known for his work on proof theory and the foundations of natural deduction....
- Charles Sanders Peirce
- Frank P. RamseyFrank P. RamseyFrank Plumpton Ramsey was a British mathematician who, in addition to mathematics, made significant and precocious contributions in philosophy and economics before his death at the age of 26...
- Bertrand RussellBertrand RussellBertrand Arthur William Russell, 3rd Earl Russell, OM, FRS was a British philosopher, logician, mathematician, historian, and social critic. At various points in his life he considered himself a liberal, a socialist, and a pacifist, but he also admitted that he had never been any of these things...
- Dana ScottDana ScottDana Stewart Scott is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, California...
- Alfred TarskiAlfred TarskiAlfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
- Alan TuringAlan TuringAlan Mathison Turing, OBE, FRS , was an English mathematician, logician, cryptanalyst, and computer scientist. He was highly influential in the development of computer science, providing a formalisation of the concepts of "algorithm" and "computation" with the Turing machine, which played a...
Bird watching and missing data
- George A. Barnard, "Gone Birdwatching", New Scientist, 4 December 1999, magazine issue 2215.
Probability foundations
- 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 on algebraic structures, following Ulf Grenander
- Grenander, UlfUlf GrenanderUlf Grenander is a statistician and a professor of applied mathematics at Brown University.His early research was in probability theory, stochastic processes, time series analysis, and statistical theory...
. 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 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 foundations
- Anders Martin-LöfAnders Martin-LöfAnders Martin-Löf is a Swedish physicist and mathematician. He is a professor in insurance mathematics and mathematical statistics since 1987 at the Department of Mathematics of Stockholm University....
. 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 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. EdwardsA. W. F. EdwardsAnthony William Fairbank Edwards is a British statistician, geneticist, and evolutionary biologist, sometimes called Fisher's Edwards. He is a Life Fellow of Gonville and Caius College and retired Professor of Biometry at the University of Cambridge, and holds both the ScD and LittD degrees. A...
, G. A. Barnard, D. A. Sprott, O. Barndorff-Nielsen, D. Basu and G. RaschRasch modelRasch models are used for analysing data from assessments to measure variables such as abilities, attitudes, and personality traits. For example, they may be used to estimate a student's reading ability from answers to questions on a reading assessment, or the extremity of a person's attitude to...
. 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 and G. RaschRasch modelRasch models are used for analysing data from assessments to measure variables such as abilities, attitudes, and personality traits. For example, they may be used to estimate a student's reading ability from answers to questions on a reading assessment, or the extremity of a person's attitude to...
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. DempsterArthur P. DempsterArthur Pentland Dempster is a Professor Emeritus in the Harvard University Department of Statistics. He was one of four faculty when the department was founded in 1957.He was a Putnam Fellow in 1951. He obtained his Ph.D. from Princeton University in 1956...
, D. Basu, D. R. Cox, A. W. F. EdwardsA. W. F. EdwardsAnthony William Fairbank Edwards is a British statistician, geneticist, and evolutionary biologist, sometimes called Fisher's Edwards. He is a Life Fellow of Gonville and Caius College and retired Professor of Biometry at the University of Cambridge, and holds both the ScD and LittD degrees. A...
, D. A. Sprott, G. A. Barnard, O. Barndorff-Nielsen, J. D. Kalbfleisch and G. RaschRasch modelRasch models are used for analysing data from assessments to measure variables such as abilities, attitudes, and personality traits. For example, they may be used to estimate a student's reading ability from answers to questions on a reading assessment, or the extremity of a person's attitude to...
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
- Per Martin-Löf. Intuitionistic type theory. Napoli, Bibliopolis, 1984.
- 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 LogicNordic Journal of Philosophical LogicThe Nordic Journal of Philosophical Logic was an international journal of philosophy started in May 1996. The journal considered submissions in any of the areas associated with Philosophical Logic and with the application of logic in conceptual analysis. The journal was edited at the Department of...
", 1(1): 11–60, 1996. - Per Martin-Löf. "Constructive mathematics and computer programming." In Logic, Methodology and Philosophy of Science VI. Eds. Cohen, et al. North-Holland, Amsterdam. pp. 153–175, 1982.