Per Martin-Löf
| Per Martin-Löf | ||
|---|---|---|
![]() Per Martin-Löf en 2004 | ||
| Información personal | ||
| Nombre completo | Per Erik Rutger Martin-Löf | |
| Nacimiento |
8 de mayo de 1942 (83 años) Estocolmo (Suecia) | |
| Nacionalidad | Sueca | |
| Educación | ||
| Educado en | Universidad de Estocolmo | |
| Supervisor doctoral | Andréi Kolmogórov | |
| Información profesional | ||
| Ocupación | Ornitólogo, filósofo, estadístico y profesor universitario | |
| Área | Lógica matemática | |
| Empleador | Universidad de Estocolmo | |
| Miembro de | ||
| Distinciones |
| |
Per Erik Rutger Martin-Löf (Estocolmo, 8 de mayo de 1942) es un lógico, filósofo y estadístico matemático sueco, reconocido por sus contribuciones fundamentales a los cimientos de la probabilidad y la estadística, a la lógica matemática y a la informática teórica. Es especialmente conocido por la definición de aleatoriedad estadística (en teoría algorítmica de la información) y por la teoría de tipos intuicionista (base constructiva de las matemáticas que ha influido en múltiples asistentes de prueba [proof assistants] y lenguajes con tipos dependientes).[1]
Vida y formación
Martin-Löf nació en Estocolmo (Suecia). Estudió inicialmente probabilidad sobre estructuras algebraicas bajo la dirección de Ulf Grenander, tema al que dedicó una tesis de licenciatura (incluidas contribuciones sobre semigrupos y el teorema de continuidad en grupos localmente compactos).[2][3][4]
En 1961, siendo aún muy joven y un estusiasta observador de aves,[5] publicó su primer artículo científico sobre tasas de mortalidad de aves anilladas (con datos del correlimos común, Calidris alpina), trabajo que recibió pronto citas en revistas internacionales.[6]
En 1964 entre 1965 trabajó en Moscú bajo la supervisión de Andréi Kolmogórov, y en 1970 obtuvo el doctorado en la Universidad de Estocolmo.[7]
Su hermano Anders Martin-Löf también es estadístico. Ambos colaboraron en diversos problemas de probabilidad y estadística, con impacto en familias exponenciales, valores faltantes y selección de modelos.
Probabilidad y estadística
Aleatoriedad de Martin-Löf y complejidad de Kolmogórov
En 1966, a partir de ideas desarrolladas mientras trabajaba con Kolmogórov, publicó The definition of random sequences, que ofreció la primera formalización satisfactoria de “secuencia aleatoria” mediante pruebas efectivas de aleatoriedad (definidas con nociones de cómputo).[8] Esta propuesta superaba las aproximaciones previas de Richard von Mises, precisando qué cuenta como “test de aleatoriedad”.
Desde entonces se han establecido caracterizaciones equivalentes (por compresibilidad, por tests estadísticos o por imposibilidad de ganar dinero apostando de forma efectiva), lo que apoya la tesis —análoga a la tesis de Church-Turing— de que su noción capta correctamente la intuición de aleatoriedad (a veces llamada tesis de Martin-Löf–Chaitin).[9]
Modelos estadísticos, tests exactos y selección de modelos
En la década de 1970 impulsó un enfoque de muestra finita para los fundamentos de la estadística, en contraste con justificaciones meramente asintóticas.[10] Desarrolló la noción de estructura repetitiva, una caracterización de familias exponenciales de un parámetro y un tratamiento teórico-categorial de modelos anidados, defendiendo tests exactos y medidas de redundancia para cuantificar la discrepancia entre hipótesis y datos.[11] Su trabajo inspiró a estadísticos escandinavos como Rolf Sundberg, Thomas Höglund y Steffen Lauritzen.

Datos faltantes y el método EM
Dentro del marco de familias exponenciales con datos incompletos, Sundberg desarrolló un análisis detallado del método de esperanza-maximización (EM), atribuyendo una fórmula clave (conocida como fórmula de Sundberg) a manuscritos previos de los hermanos Martin-Löf.[12][13][14][15] Estos resultados circularon internacionalmente a partir del célebre artículo de Dempster–Laird–Rubin (1977) sobre EM.[16]
Probabilidad sobre estructuras algebraicas
Antes de su giro principal hacia la lógica, Martin-Löf estudió probabilidad en semigrupos y grupos localmente compactos (continuidad de medidas, análisis armónico y herramientas afines), siguiendo la escuela de Grenander.
Lógica, filosofía y teoría de tipos
Filosofía de la lógica
En lógica filosófica examinó la noción de consecuencia lógica y la teoría del juicio, con afinidades a tradiciones centroeuropeas (inspirado por Franz Brentano, Gottlob Frege y Edmund Husserl). También es conocido por su teoría de tipos dependientes, base de la teoría homotópica de tipos y usada en demostradores de teoremas como Coq o Lean.

Teoría de tipos de Martin-Löf
Tras un periodo como profesor asistente en la Universidad de Chicago (1968–1969), donde dialogó con William Alvin Howard sobre la correspondencia de Curry–Howard, elaboró en 1971 un primer borrador de una teoría de tipos impredicativa (generalizando el Sistema F de Girard). El sistema resultó inconsistente por la paradoja de Girard –pues incluía un tipo de todos los tipos, lo que llevó a Martin-Löf a reconstruir el fundamento filosófico de su enfoque mediante sus “explicaciones de significado” (una forma de semántica teórica de la prueba) y a presentar en 1984 su teoría de tipos predicativa.[17] La versión de 1990 (de Nordström–Petersson–Smith), influida por sus ideas posteriores, es intensional y más apta para implementación computacional.[1]
Su teoría de tipos intuicionista introdujo y popularizó los tipos dependientes e influyó directamente en el cálculo de construcciones y en el marco lógico LF. Su teoría de tipos ocupa una lógica intuicionista y constructiva gracias a la correspondcncia de Curry-Howard. Numerosos asistentes de prueba y lenguajes se basan o inspiran en esta tradición: NuPRL, LEGO, Coq, Lean, ALF, Agda, Twelf, Epigram, Idris, entre otros.
Carrera académica e instituciones
Además de su larga vinculación con la Universidad de Estocolmo, trabajó en la Universidad de Chicago y en la Universidad de Aarhus. Hasta su jubilación en 2009,[18] ocupó una cátedra conjunta de Matemáticas y Filosofía en la Universidad de Estocolmo.[19]
Reconocimientos
Es miembro de la Academia Europea (desde 1989)[19] y de la Real Academia de las Ciencias de Suecia (desde 1990).[20] Recibió en 2004 su doctorado honoris causa por la Universidad de Aix-Marsella II.[21] Ha impartido la Gödel Lecture (2006)[22] y recibió el Premio Schock (2020).[23]
Material de profundización
Observación de aves y datos faltantes
- Martin-Löf, P. (1961). «Mortality rate calculations on ringed birds with special reference to the Dunlin Calidris alpina». 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. (2002). 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 978-1-930665-55-2.
Fundamentos de la probabilidad
- 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.
Probabilidad en estructuras algebraicas (siguiendo a Ulf Grenander)
- Grenander, Ulf. 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.
Fundamentos estadísticos
- 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 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 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 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
Fundamentos de matemáticas, lógica e informática
- 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 Colloquium ‘73, pages 73–118. North Holland, 1975.
- Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and 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.
- Per Martin-Löf. Logic and Ethics. In T. Piecha and P. Schroeder-Heister, editors, Proof-Theoretic Semantics: Assessment and Future Perspectives. Proceedings of the Third Tübingen Conference on Proof-Theoretic Semantics, 27–30 March 2019, pages 227-235. URI: http://dx.doi.org/10.15496/publikation-35319. University of Tübingen 2019.
Véase también
- Teoría de tipos
- Andréi Kolmogórov
- Richard von Mises
- Teoría de categorías
- Franz Brentano
- Gottlob Frege
- Edmund Husserl
- Correspondencia de Curry–Howard
Referencias
- ↑ a b Nordström, Bengt; Petersson, Kent; Smith, Jan M. (1990), Programming in Martin-Löf 's Type Theory: An Introduction, Oxford University Press..
- ↑ Martin-Löf, P. (1965-01). «The Continuity Theorem on a Locally Compact Group». Theory of Probability & Its Applications 10 (2): 338-341. ISSN 0040-585X. doi:10.1137/1110040. Consultado el 17 de agosto de 2025.
- ↑ Martin-Löf, Per (1 de marzo de 1965). «Probability theory on discrete semigroups». Zeitschrift für Wahrscheinlichkeitstheorie und Verwandte Gebiete (en inglés) 4 (1): 78-102. ISSN 1432-2064. doi:10.1007/BF00535486. Consultado el 17 de agosto de 2025.
- ↑ Grenander, Ulf; Mukhopadhyay, Nitis (2006). «A Conversation with Ulf Grenander». Statistical Science 21 (3): 404-426. ISSN 0883-4237. Consultado el 17 de agosto de 2025.
- ↑ George A. Barnard, "Gone Birdwatching", New Scientist, 4 December 1999, magazine issue 2215.
- ↑ Taylor, S. M. (1966). «Recent Quantitative Work on British Bird Populations. A Review». Journal of the Royal Statistical Society. Series D (The Statistician) 16 (2): 119-170. ISSN 0039-0526. doi:10.2307/2986734. Consultado el 17 de agosto de 2025.
- ↑ «Mathematics Genealogy Project: Per Martin-Löf».
- ↑ Martin-Löf, Per (1 de diciembre de 1966). «The definition of random sequences». Information and Control 9 (6): 602-619. ISSN 0019-9958. doi:10.1016/S0019-9958(66)80018-9. Consultado el 17 de agosto de 2025.
- ↑ Delahaye, Jean-Paul (1993). Dubucs, Jacques-Paul, ed. Randomness, Unpredictability and Absence of Order: The Identification by the Theory of Recursivity of the Mathematical Notion of Random Sequence (en inglés). Springer Netherlands. pp. 145-167. ISBN 978-90-481-4301-6. doi:10.1007/978-94-015-8208-7_8. Consultado el 17 de agosto de 2025.
- ↑ Kolmogorov, A. N. On tables of random numbers. Sankhya, the Indian Journal of Statistics: Series A, 25(4):369-376, 1963.
- ↑ Martin-L�f, Per (1974). «The Notion of Redundancy and Its Use as a Quantitative Measure of the Discrepancy between a Statistical Hypothesis and a Set of Observational Data [with Discussion]». Scandinavian Journal of Statistics 1 (1): 3-18. ISSN 0303-6898. Consultado el 17 de agosto de 2025.
- ↑ Sundberg, Rolf (1974). «Maximum Likelihood Theory for Incomplete Data from an Exponential Family». Scandinavian Journal of Statistics 1 (2): 49-58. ISSN 0303-6898. Consultado el 17 de agosto de 2025.
- ↑ 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 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.
- ↑ 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 (Methodological) 39 (1): 1-38. ISSN 0035-9246. Consultado el 17 de agosto de 2025.
- ↑ Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984.
- ↑ «Conference: Philosophy and Foundations of Mathematics - Epistemological and Ontological Aspects, Uppsala May 5-8, 2009». filosofia.fi (en finés). 2 de diciembre de 2008. Consultado el 17 de agosto de 2025.
- ↑ a b «Academy of Europe: Martin-Löf Per». www.ae-info.org. Consultado el 17 de agosto de 2025.
- ↑ «Per Martin-Löf». Kungl. Vetenskapsakademien (en inglés británico). Consultado el 17 de agosto de 2025.
- ↑ «Base de données des doctorats Honoris Causa en France». honoris-causa.geobib.fr (en francés). Consultado el 17 de agosto de 2025.
- ↑ «Gödel Lecturers – Association for Symbolic Logic» (en inglés estadounidense). Consultado el 17 de agosto de 2025.
- ↑ «Per Martin-Löf». Kungl. Vetenskapsakademien (en inglés británico). Consultado el 17 de agosto de 2025.
