Por Martin-Löf

Por Martin-Löf
Por Martin-Löf en 2004
Nacido	( 08-05-1942 )8 de mayo de 1942 (82 años) Estocolmo , [1] Suecia
Nacionalidad	sueco
Ciudadanía	Suecia
Alma máter	Universidad de Estocolmo
Conocido por	Secuencias aleatorias Pruebas exactas Estructura repetitiva Estadísticas suficientes Método de expectativa-maximización (EM) Teoría de tipos de Martin-Löf Aleatoriedad de Martin-Löf
Premios	Real Academia Sueca de Ciencias (1990) Conferencia Gödel (2006) Premio Rolf Schock (2020)
Carrera científica
Campos	Ciencias de la Computación Lógica Estadística matemática Filosofía
Instituciones	Universidad de Estocolmo Universidad de Chicago Universidad de Aarhus
Asesor de doctorado	Andrei N. Kolmogorov

Per Erik Rutger Martin-Löf ( ^nacido el 8 de mayo de 1942) es un lógico , filósofo y estadístico matemático sueco . Es reconocido internacionalmente por su trabajo sobre los fundamentos de ^la probabilidad , la estadística , la lógica matemática y la informática . Desde finales de la década de 1970, las publicaciones de Martin-Löf han sido principalmente sobre lógica . En lógica filosófica , Martin-Löf ha luchado con la filosofía de la consecuencia lógica y el juicio , en parte inspirado por el trabajo de Brentano , Frege y Husserl . En lógica matemática , Martin-Löf ha estado activo en el desarrollo de la teoría de tipos intuicionista como una base constructiva de las matemáticas; el trabajo de Martin-Löf sobre la teoría de tipos ha influido en la informática . ^[4]

Hasta su jubilación en 2009, ^[5] Per Martin-Löf ocupó una cátedra conjunta de Matemáticas y Filosofía en la Universidad de Estocolmo . ^[6]

Su hermano Anders Martin-Löf es ahora profesor emérito de estadística matemática en la Universidad de Estocolmo; los dos hermanos han colaborado en la investigación sobre probabilidad y estadística. La investigación de Anders y Per Martin-Löf ha influido en la teoría estadística, especialmente en lo relativo a las familias exponenciales , el método de expectativa-maximización para datos faltantes y la selección de modelos . ^[7]

Per Martin-Löf recibió su doctorado en 1970 en la Universidad de Estocolmo , bajo la dirección de Andrey Kolmogorov . ^[8]

Martin-Löf es un entusiasta observador de aves ; su primera publicación científica fue sobre las tasas de mortalidad de las aves anilladas . ^[9]

En 1964 y 1965, Martin-Löf estudió en Moscú bajo la supervisión de Andrei N. Kolmogorov . En 1966 escribió un artículo titulado The definition of random sequences (La definición de secuencias aleatorias) , que proporcionó la primera definición adecuada de una secuencia aleatoria. ^[10]

Investigadores anteriores, como Richard von Mises , habían intentado formalizar la noción de una prueba de aleatoriedad para definir una secuencia aleatoria como aquella que pasaba todas las pruebas de aleatoriedad; sin embargo, la noción precisa de una prueba de aleatoriedad quedó vaga. La idea clave de Martin-Löf fue utilizar la teoría de la computación para definir formalmente la noción de una prueba de aleatoriedad. Esto contrasta con la idea de aleatoriedad en la probabilidad ; en esa teoría, no se puede decir que ningún elemento particular de un espacio muestral sea aleatorio.

Desde entonces se ha demostrado que la aleatoriedad de Martin-Löf admite muchas caracterizaciones equivalentes —en términos de compresión , pruebas de aleatoriedad y juego— que tienen poco parecido exterior con la definición original, pero cada una de las cuales satisface nuestra noción intuitiva de propiedades que deben tener las secuencias aleatorias: las secuencias aleatorias deben ser incompresibles, deben pasar pruebas estadísticas de aleatoriedad y debe ser imposible ganar dinero apostando en ellas. La existencia de estas múltiples definiciones de aleatoriedad de Martin-Löf, y la estabilidad de estas definiciones bajo diferentes modelos de computación, dan evidencia de que la aleatoriedad de Martin-Löf es una propiedad fundamental de las matemáticas y no un accidente del modelo particular de Martin-Löf. La tesis de que la definición de aleatoriedad de Martin-Löf captura "correctamente" la noción intuitiva de aleatoriedad se ha llamado la "Tesis de Martin-Löf -Chaitin "; es algo similar a la tesis de Church-Turing . ^[11]

Siguiendo el trabajo de Martin-Löf, la teoría de la información algorítmica define una cadena aleatoria como aquella que no puede ser producida por ningún programa de computadora que sea más corta que la cadena ( aleatoriedad de Chaitin-Kolmogorov ); es decir, una cadena cuya complejidad de Kolmogorov es al menos la longitud de la cadena. Este es un significado diferente del uso del término en estadística. Mientras que la aleatoriedad estadística se refiere al proceso que produce la cadena (por ejemplo, lanzar una moneda para producir cada bit producirá aleatoriamente una cadena), la aleatoriedad algorítmica se refiere a la cadena en sí . La teoría de la información algorítmica separa las cadenas aleatorias de las no aleatorias de una manera que es relativamente invariante al modelo de cálculo que se esté utilizando.

Una secuencia algorítmicamente aleatoria es una secuencia infinita de caracteres, cuyos prefijos (excepto posiblemente un número finito de excepciones) son cadenas que están "cerca de" ser algorítmicamente aleatorias (su longitud está dentro de una constante de su complejidad de Kolmogorov).

Per Martin-Löf ha realizado importantes investigaciones en estadística matemática , que (en la tradición sueca) incluye la teoría de la probabilidad y la estadística .

Per Martin-Löf comenzó a observar aves en su juventud y sigue siendo un entusiasta observador de aves. ^[12] Cuando era adolescente, publicó un artículo sobre la estimación de las tasas de mortalidad de las aves, utilizando datos del anillamiento de aves , en una revista zoológica sueca: Este artículo pronto fue citado en importantes revistas internacionales y sigue siendo citado. ^{[9] [13]}

En la biología y estadística de las aves , existen varios problemas de datos faltantes . El primer artículo de Martin-Löf abordó el problema de estimar las tasas de mortalidad de la especie Correlimos común , utilizando métodos de captura y recaptura . El problema de determinar el sexo biológico de un ave, que es extremadamente difícil para los humanos, es uno de los primeros ejemplos en las conferencias de Martin-Löf sobre modelos estadísticos .

Martin-Löf escribió una tesis de licenciatura sobre probabilidad en estructuras algebraicas, particularmente semigrupos, mientras era estudiante de Ulf Grenander en la Universidad de Estocolmo. ^{[14] [15] [16]}

Martin-Löf desarrolló enfoques innovadores para la teoría estadística . En su artículo "Sobre las tablas de números aleatorios", Kolmogorov observó que la noción de probabilidad de frecuencia de las propiedades limitantes de las secuencias infinitas no proporcionaba una base para la estadística, que solo considera muestras finitas. ^[17] Gran parte del trabajo de Martin-Löf en estadística consistió en proporcionar una base de muestras finitas para la estadística.

En la década de 1970, Per Martin-Löf realizó importantes contribuciones a la teoría estadística e inspiró investigaciones posteriores, especialmente por parte de estadísticos escandinavos como Rolf Sundberg, Thomas Höglund y Steffan Lauritzen. En este trabajo, la investigación previa de Martin-Löf sobre medidas de probabilidad en semigrupos condujo a una noción de "estructura repetitiva" y un tratamiento novedoso de las estadísticas suficientes, en el que se caracterizaron las familias exponenciales de un parámetro . Proporcionó un enfoque de teoría de categorías para los modelos estadísticos anidados , utilizando principios de muestra finita. Antes (y después) de Martin-Löf, dichos modelos anidados a menudo se han probado utilizando pruebas de hipótesis de chi-cuadrado, cuyas justificaciones son solo asintóticas (y, por lo tanto, irrelevantes para los problemas reales, que siempre tienen muestras finitas). ^[17]

El estudiante de Martin-Löf, Rolf Sundberg, desarrolló un análisis detallado del método de expectativa-maximización (EM) para la estimación utilizando datos de familias exponenciales, especialmente con datos faltantes . Sundberg atribuye una fórmula, más tarde conocida como la fórmula de Sundberg, a manuscritos anteriores de los hermanos Martin-Löf, Per y Anders . ^{[18] [19] [20] [21]} Muchos de estos resultados llegaron a la comunidad científica internacional a través del artículo de 1976 sobre el método de expectativa-maximización (EM) de Arthur P. Dempster , Nan Laird y Donald Rubin , que se publicó en una revista internacional líder, patrocinada por la Royal Statistical Society . ^[22]

En lógica filosófica , Per Martin-Löf ha publicado artículos sobre la teoría de la consecuencia lógica , sobre los juicios , etc. Se ha interesado por las tradiciones filosóficas de Europa Central , especialmente por los escritos en lengua alemana de Franz Brentano , Gottlob Frege y Edmund Husserl .

Martin-Löf ha trabajado en lógica matemática durante muchas décadas.

De 1968 a '69 trabajó como profesor asistente en la Universidad de Chicago , donde conoció a William Alvin Howard, con quien discutió cuestiones relacionadas con la correspondencia Curry-Howard . El primer borrador del artículo de Martin-Löf sobre la teoría de tipos data de 1971. Esta teoría impredicativa generalizó el Sistema F de Girard . Sin embargo, este sistema resultó ser inconsistente debido a la paradoja de Girard que fue descubierta por Girard al estudiar el Sistema U, una extensión inconsistente del Sistema F. Esta experiencia llevó a Per Martin-Löf a desarrollar los fundamentos filosóficos de la teoría de tipos , su explicación del significado , una forma de semántica de teoría de pruebas , que justifica la teoría de tipos predicativa como se presenta en su libro Bibliopolis de 1984, y se extendió en una serie de textos cada vez más filosóficos, como su influyente Sobre los significados de las constantes lógicas y las justificaciones de las leyes lógicas .

La teoría de tipos de 1984 era extensional, mientras que la teoría de tipos presentada en el libro de Nordström et al. en 1990, que estuvo fuertemente influenciada por sus ideas posteriores, era intensional y más susceptible de ser implementada en una computadora.

La teoría de tipos intuicionista de Martin-Löf desarrolló la noción de tipos dependientes e influyó directamente en el desarrollo del cálculo de construcciones y el marco lógico LF . Varios sistemas de prueba basados ​​en computadora populares se basan en la teoría de tipos, por ejemplo, NuPRL , LEGO, Coq , ALF, Agda , Twelf , Epigram e Idris .

Martin-Löf es miembro de la Real Academia Sueca de Ciencias ^[23] (elegido en 1990) y de la Academia Europaea (elegido en 1989). ^[6]

• Martín-Löf, P. (1961). «Cálculos de la tasa de mortalidad de aves anilladas con especial referencia al correlimos Calidris alpina ». Arkiv för Zoologi (Archivos de zoología), Kungliga Svenska Vetenskapsakademien (Real Academia Sueca de Ciencias) Serie 2 . Banda 13 (21).

• George A. Barnard , "Gone Birdwatching", New Scientist , 4 de diciembre de 1999, número de revista 2215.
• Seber, GAF (2002). Estimación de la abundancia animal y parámetros relacionados . Caldwel, Nueva Jersey: Blackburn Press. ISBN 1-930665-55-5.
• Royle, JA; RM Dorazio (2008). Modelado jerárquico e inferencia en ecología . Elsevier. ISBN 978-1-930665-55-2.

• Per Martin-Löf. "La definición de secuencias aleatorias". Información y control , 9(6): 602–619, 1966.
• Li, Ming y Vitányi, Paul, Introducción a la complejidad de Kolmogorov y sus aplicaciones , Springer, 1997. Texto completo del capítulo de introducción.

• Grenander, Ulf . Probabilidad en estructuras algebraicas . (Reimpresión de Dover)
• Martin-Löf, P. El teorema de continuidad en un grupo localmente compacto. Teor. Verojatnost. i Primenen. 10 1965 367–371.
• Martín-Löf, Per. Teoría de la probabilidad sobre semigrupos discretos. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 4 1965 78—102
• Nitis Mukhopadhyay. "Una conversación con Ulf Grenander". Statist. Sci. Volumen 21, Número 3 (2006), 404–426.

• Anders Martin-Löf . 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Evaluación de vidas en períodos de tiempo inferiores a un nanosegundo"). ("Fórmula de Sundberg", según Sundberg 1971)
• Per Martin-Löf. 1966. Estadísticas desde el punto de vista de la mecánica estadística . Apuntes de clase, Instituto de Matemáticas, Universidad de Aarhus. ("Fórmula de Sundberg" atribuida a Anders Martin-Löf, según Sundberg 1971)
• Según Martin-Löf. 1970. Statistika Modeller (Modelos estadísticos): Anteckningar fran seminarier läsåret 1969–1970 (Notas de seminarios del año académico 1969–1970), con la ayuda de Rolf Sundberg. Universidad de Estocolmo.
• Martin-Löf, P. "Pruebas exactas, regiones de confianza y estimaciones", con una discusión de AWF Edwards , GA Barnard , DA Sprott, O. Barndorff-Nielsen, D. Basu y G. Rasch . Actas de la Conferencia sobre Cuestiones Fundamentales en Inferencia Estadística (Aarhus, 1973), págs. 121-138. Memorias, n.º 1, Dept. Theoret. Statist., Inst. Math., Univ. Aarhus, Aarhus, 1974.
• Martin-Löf, P. Estructuras repetitivas y la relación entre distribuciones canónicas y microcanónicas en estadística y mecánica estadística. Con una discusión de DR Cox y G. Rasch y una respuesta del autor. Actas de la Conferencia sobre Cuestiones Fundamentales en Inferencia Estadística (Aarhus, 1973), págs. 271–294. Memorias, n.º 1, Dept. Theoret. Statist., Inst. Math., Univ. Aarhus, Aarhus, 1974.
• Martin-Löf, P. La noción de redundancia y su uso como medida cuantitativa de la desviación entre una hipótesis estadística y un conjunto de datos observacionales. Con una discusión de F. Abildgård, AP Dempster , D. Basu , DR Cox , AWF Edwards , DA Sprott, GA Barnard , O. Barndorff-Nielsen, JD Kalbfleisch y G. Rasch y una respuesta del autor. Actas de la Conferencia sobre Cuestiones Fundamentales en Inferencia Estadística (Aarhus, 1973), págs. 1–42. Memorias, n.º 1, Dept. Theoret. Statist., Inst. Math., Univ. Aarhus, Aarhus, 1974.
• Martin-Löf, Per La noción de redundancia y su uso como medida cuantitativa de la discrepancia entre una hipótesis estadística y un conjunto de datos observacionales. Scand. J. Statist. 1 (1974), no. 1, 3—18.
• Sverdrup, Erling. "Pruebas sin potencia". Scand. J. Statist. 2 (1975), núm. 3, 158–160.
• Martin-Löf, Per Respuesta al artículo polémico de Erling Sverdrup: Pruebas sin poder ( Scand. J. Statist. 2 (1975), no. 3, 158–160). Scand. J. Statist. 2 (1975), no. 3, 161–165.
• Sverdrup, Erling. Una réplica a: Pruebas sin poder ( Scand. J. Statist. 2 (1975), 161—165) por P. Martin-Löf. Scand. J. Statist. 4 (1977), no. 3, 136—138.
• Martin-Löf, P. Pruebas exactas, regiones de confianza y estimaciones. Fundamentos de probabilidad y estadística. II. Synthese 36 (1977), núm. 2, 195—206.
• Rolf Sundberg. 1971. Teoría de máxima verosimilitud y aplicaciones para distribuciones generadas al observar una función de una variable de la familia exponencial . Tesis doctoral, Instituto de Estadística Matemática, Universidad de Estocolmo.
• Sundberg, Rolf. Teoría de máxima verosimilitud para datos incompletos de una familia exponencial. Scand. J. Statist. 1 (1974), núm. 2, 49—58.
• Sundberg, Rolf Un método iterativo para la solución de ecuaciones de verosimilitud para datos incompletos de familias exponenciales. Comm. Statist.—Simulation Comput. B5 (1976), no. 1, 55—64.
• Sundberg, Rolf Algunos resultados sobre modelos descomponibles (o de tipo Markov) para tablas de contingencia multidimensionales: distribución de marginales y partición de pruebas. Scand. J. Statist. 2 (1975), no. 2, 71—79.
• Höglund, Thomas. La estimación exacta — el método de la estimación estadística. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 29 (1974), 257—271.
• Lauritzen, Steffen L. Familias extremas y sistemas de estadísticas suficientes . Lecture Notes in Statistics, 49. Springer-Verlag, Nueva York, 1988. xvi+268 pp. ISBN 0-387-96872-5 

• Per Martin-Löf. Una teoría de tipos. Preimpresión, Universidad de Estocolmo, 1971.
• Per Martin-Löf. Una teoría intuicionista de los tipos. En G. Sambin y J. Smith, editores, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998. Versión reimpresa de un informe inédito de 1972.
• Per Martin-Löf. Una teoría intuicionista de los tipos: parte predicativa. En HE Rose y JC Shepherdson, editores, Logic Colloquium '73, páginas 73-118. Holanda Septentrional, 1975.
• Per Martin-Löf. Matemáticas constructivas y programación informática. En Logic, Methodology and Philosophy of Science VI, 1979. Eds. Cohen, et al. North-Holland, Amsterdam. pp. 153–175, 1982.
• Según Martin-Löf. Teoría de tipos intuicionista. (Notas de Giovanni Sambin sobre una serie de conferencias pronunciadas en Padua, junio de 1980). Nápoles, Bibliopolis, 1984.
• Per Martin-Löf. Implicaciones filosóficas de la teoría de tipos , Notas inéditas, 1987.
• Según Martin-Löf. Cálculo de sustitución , 1992. Apuntes de una conferencia impartida en Gotemburgo.
• Bengt Nordström, Kent Petersson y Jan M. Smith. Programming in Martin-Löf's Type Theory . Oxford University Press, 1990. (El libro está agotado, pero hay una versión gratuita disponible).
• Per Martin-Löf. Sobre los significados de las constantes lógicas y las justificaciones de las leyes lógicas. Nordic Journal of Philosophical Logic , 1(1): 11–60, 1996.
• Per Martin-Löf. Lógica y ética. En T. Piecha y P. Schroeder-Heister, editores, Proof-Theoretic Semantics: Assessment and Future Perspectives. Actas de la Tercera Conferencia de Tubinga sobre Semántica de la Teoría de la Prueba, 27-30 de marzo de 2019 , páginas 227-235. URI: http://dx.doi.org/10.15496/publikation-35319 . Universidad de Tubinga 2019.

• Per Martin-Löf en el Proyecto de Genealogía Matemática