Per Martin-Löf - Per Martin-Löf

Per Martin-Löf
Per Martin-Löf em 2004
Nascer	( 08/05/1942 )8 de maio de 1942 (79 anos) Estocolmo , Suécia
Nacionalidade	sueco
Cidadania	Suécia
Alma mater	Universidade de Estocolmo
Conhecido por	Sequências aleatórias Testes exatos Estrutura repetitiva Estatísticas suficientes Método de maximização de expectativas Teoria de tipo de Martin-Löf
Prêmios	Prêmio Rolf Schock da Academia Real Sueca de Ciências (2020)
Carreira científica
Campos	Lógica da Ciência da Computação Estatística matemática Filosofia
Instituições	Stockholm University University of Chicago Aarhus University
Orientador de doutorado	Andrei N. Kolmogorov

Per Erik Rutger Martin-Löf ( / l ɒ f / ; sueco:  [ˈmǎʈːɪn ˈløːv] ; nascido em 8 de maio de 1942) é um lógico , filósofo e estatístico matemático sueco . Ele é internacionalmente conhecido por seu trabalho sobre os fundamentos da probabilidade , estatística, lógica matemática e ciência da computação . Desde o final dos anos 1970, as publicações de Martin-Löf foram principalmente em lógica . Na lógica filosófica , Martin-Löf lutou com a filosofia da consequência lógica e do julgamento , em parte inspirada na obra de Brentano , Frege e Husserl . Na lógica matemática , Martin-Löf foi ativo no desenvolvimento da teoria dos tipos intuicionista como uma base construtiva da matemática; O trabalho de Martin-Löf sobre a teoria dos tipos influenciou a ciência da computação .

Até sua aposentadoria em 2009, Per Martin-Löf ocupou uma cadeira conjunta de Matemática e Filosofia na Universidade de Estocolmo .

Seu irmão Anders Martin-Löf é agora professor emérito de estatística matemática na Universidade de Estocolmo; os dois irmãos colaboraram em pesquisas de probabilidade e estatística. A pesquisa de Anders e Per Martin-Löf influenciou a teoria estatística, especialmente no que diz respeito às famílias exponenciais , o método de maximização da expectativa para dados perdidos e a seleção de modelos .

Per Martin-Löf é um entusiasta observador de pássaros ; sua primeira publicação científica foi sobre as taxas de mortalidade de pássaros anilhados .

Aleatoriedade e complexidade de Kolmogorov

Em 1964 e 1965, Martin-Löf estudou em Moscou sob a supervisão de Andrei N. Kolmogorov . Ele escreveu um artigo de 1966, A definição de sequências aleatórias, que deu a primeira definição adequada de uma sequência aleatória.

Pesquisadores anteriores, como Richard von Mises , tentaram formalizar a noção de um teste de aleatoriedade para definir uma sequência aleatória como aquela que passou em todos os testes de aleatoriedade; no entanto, a noção precisa de um teste de aleatoriedade foi deixada vaga. O insight principal de Martin-Löf foi usar a teoria da computação para definir formalmente a noção de um teste de aleatoriedade. Isso contrasta com a ideia de aleatoriedade na probabilidade ; nessa teoria, nenhum elemento particular de um espaço amostral pode ser considerado aleatório.

A aleatoriedade de Martin-Löf já demonstrou admitir muitas caracterizações equivalentes - em termos de compressão , testes de aleatoriedade e jogos de azar - que têm pouca semelhança externa com a definição original, mas cada uma das quais satisfaz nossa noção intuitiva de propriedades que as sequências aleatórias devem têm: as sequências aleatórias devem ser incompressíveis, devem passar por testes estatísticos de aleatoriedade e deve ser impossível ganhar dinheiro apostando nelas. A existência dessas múltiplas definições de aleatoriedade de Martin-Löf e a estabilidade dessas definições sob diferentes modelos de computação dão evidências de que a aleatoriedade de Martin-Löf é uma propriedade fundamental da matemática e não um acidente do modelo particular de Martin-Löf. A tese de que a definição de aleatoriedade de Martin-Löf "corretamente" captura a noção intuitiva de aleatoriedade foi chamada de " Tese de Martin-Löf– Chaitin "; é um tanto semelhante à tese de Church-Turing .

Seguindo o trabalho de Martin-Löf, a teoria da informação algorítmica define uma string aleatória como aquela que não pode ser produzida a partir de nenhum programa de computador que seja mais curto do que a string ( aleatoriedade de Chaitin – Kolmogorov ); ou seja, uma string cuja complexidade de Kolmogorov é de pelo menos o comprimento da string. Este é um significado diferente do uso do termo em estatísticas. Enquanto a aleatoriedade estatística se refere ao processo que produz a string (por exemplo, jogar uma moeda para produzir cada bit produzirá aleatoriamente uma string), a aleatoriedade algorítmica se refere à própria string . A teoria da informação algorítmica separa strings aleatórias de não aleatórias de uma forma que é relativamente invariável em relação ao modelo de computação que está sendo usado.

Uma sequência algorítmica aleatória é uma sequência infinita de caracteres, todos cujos prefixos (exceto possivelmente um número finito de exceções) são strings que são "perto de" algoritmicamente aleatórios (seu comprimento está dentro de uma constante de sua complexidade de Kolmogorov).

Estatística matemática

Per Martin-Löf fez pesquisas importantes em estatística matemática , que (na tradição sueca) inclui teoria da probabilidade e estatística .

Observação de pássaros e determinação do sexo

O Dunlin (Calidris alpina)

Per Martin-Löf começou a observar pássaros na juventude e continua sendo um observador entusiasta. Na adolescência, ele publicou um artigo sobre como estimar as taxas de mortalidade de pássaros, usando dados de anilhagem de pássaros , em um periódico zoológico sueco: Este artigo logo foi citado nas principais revistas internacionais, e este artigo continua a ser citado.

Na biologia e nas estatísticas das aves , existem vários problemas de falta de dados . O primeiro artigo de Martin-Löf discutiu o problema de estimar as taxas de mortalidade das espécies Dunlin , usando métodos de captura-recaptura . Um segundo problema de falta de dados surge com o estudo do sexo dos pássaros. O problema de determinar o sexo biológico de um pássaro, que é extremamente difícil para os humanos, é um dos primeiros exemplos nas palestras de Martin-Löf sobre modelos estatísticos .

Probabilidade em estruturas algébricas

Martin-Löf escreveu uma tese de licenciatura sobre probabilidade em estruturas algébricas, particularmente semigrupos, um programa de pesquisa liderado por Ulf Grenander na Universidade de Estocolmo.

Modelos estatísticos

Martin-Löf desenvolveu abordagens inovadoras para a teoria estatística . Em seu artigo "On Tables of Random Numbers", Kolmogorov observou que a noção de frequência de probabilidade das propriedades limitantes de sequências infinitas falhou em fornecer uma base para estatísticas, que considera apenas amostras finitas. Muito do trabalho de Martin-Löf em estatística foi fornecer uma base de amostra finita para estatísticas.

Seleção de modelo e teste de hipótese

As etapas do algoritmo EM em um modelo de mistura gaussiana de dois componentes no conjunto de dados Old Faithful

Na década de 1970, Per Martin-Löf fez contribuições importantes para a teoria estatística e inspirou pesquisas adicionais, especialmente por estatísticos escandinavos, incluindo Rolf Sundberg, Thomas Höglund e Steffan Lauritzen. Neste trabalho, a pesquisa anterior de Martin-Löf sobre medidas de probabilidade em semigrupos levou a uma noção de "estrutura repetitiva" e um novo tratamento de estatísticas suficientes, em que famílias exponenciais de um parâmetro foram caracterizadas. Ele forneceu uma abordagem teórica de categorias para modelos estatísticos aninhados , usando princípios de amostra finita. Antes (e depois) de Martin-Löf, esses modelos aninhados muitas vezes foram testados usando testes de hipótese do qui-quadrado, cujas justificativas são apenas assintóticas (e, portanto, irrelevantes para problemas reais, que sempre têm amostras finitas).

Método de maximização de expectativa para famílias exponenciais

O aluno de Martin-Löf, Rolf Sundberg, desenvolveu uma análise detalhada do método de maximização de expectativa (EM) para estimativa usando dados de famílias exponenciais, especialmente com dados ausentes . Sundberg credita uma fórmula, mais tarde conhecida como fórmula de Sundberg, a manuscritos anteriores dos irmãos Martin-Löf, Per e Anders . Muitos desses resultados alcançaram a comunidade científica internacional por meio do artigo de 1976 sobre o método de maximização de expectativa (EM) de Arthur P. Dempster , Nan Laird e Donald Rubin , que foi publicado em um importante jornal internacional, patrocinado pela Royal Statistical Society .

Lógica

Franz Brentano

Lógica filosófica

Na lógica filosófica , Per Martin-Löf publicou artigos sobre a teoria da consequência lógica , sobre julgamentos , etc. Ele se interessou pelas tradições filosóficas da Europa Central , especialmente dos escritos em língua alemã de Franz Brentano , Gottlob Frege e de Edmund Husserl .

Teoria de tipo

Martin-Löf trabalhou com lógica matemática por muitas décadas.

De 1968 a 1969, ele trabalhou como professor assistente na Universidade de Chicago, onde conheceu William Alvin Howard, com quem discutiu questões relacionadas à correspondência Curry-Howard . O primeiro rascunho do artigo de Martin-Löf sobre a teoria dos tipos data de 1971. Essa teoria impredicativa generalizou o Sistema F de Girard . No entanto, este sistema acabou por ser inconsistente devido ao paradoxo de Girard que foi descoberto por Girard ao estudar o Sistema U, uma extensão inconsistente do Sistema F. Esta experiência levou Per Martin-Löf a desenvolver os fundamentos filosóficos da teoria dos tipos , sua explicação de significado , uma forma de semântica teórica da prova , que justifica a teoria dos tipos predicativos conforme apresentada em seu livro Bibliopolis de 1984, e estendida em uma série de textos cada vez mais filosóficos, como seu influente On the Meanings of the Logical Constants and the Justifications of the Logical Laws .

A teoria dos tipos de 1984 era extensional, enquanto a teoria dos tipos apresentada no livro de Nordström et al. em 1990, que foi fortemente influenciado por suas ideias posteriores, intensional e mais passível de ser implementado em um computador.

A teoria dos tipos intuicionistas de Martin-Löf desenvolveu a noção de tipos dependentes e influenciou diretamente o desenvolvimento do cálculo de construções e do arcabouço lógico LF . Vários sistemas de prova baseados em computador populares são baseados na teoria dos tipos, por exemplo NuPRL , LEGO, Coq , ALF, Agda , Twelf , Epigram e Idris .

Prêmios

Martin-Löf é membro da Royal Swedish Academy of Sciences e da Academia Europaea .

Veja também

Notas

Referências

Observação de pássaros e dados ausentes

• Martin-Löf, P. (1961). "Cálculos da taxa de mortalidade em aves anilhadas com referência especial ao Dunlin Calidris alpina ". Arkiv för Zoologi (Arquivos de Zoologia), Kungliga Svenska Vetenskapsakademien (A Real Academia Sueca de Ciências) Série 2 . Banda 13 (21).

• George A. Barnard , "Gone Birdwatching" , New Scientist , 4 de dezembro de 1999, edição da revista 2215.
• Seber, GAF (2002). A estimativa da abundância animal e parâmetros relacionados . Caldwel, New Jersey: Blackburn Press. ISBN 1-930665-55-5.
• Royle, JA; RM Dorazio (2008). Modelagem Hierárquica e Inferência em Ecologia . Elsevier. ISBN 978-1-930665-55-2.

Fundamentos de probabilidade

• Per Martin-Löf. "A definição de sequências aleatórias." Information and Control , 9 (6): 602–619, 1966.
• Li, Ming e Vitányi, Paul, uma introdução à complexidade de Kolmogorov e suas aplicações , Springer, 1997. Texto completo do capítulo de introdução .

Probabilidade em estruturas algébricas, seguindo Ulf Grenander

• Grenander, Ulf . Probabilidade em estruturas algébricas . (Reimpressão de Dover)
• Martin-Löf, P. O teorema da continuidade em um grupo localmente compacto. Teor. Verojatnost. i Primenen. 10 1965 367–371.
• Martin-Löf, Per. Teoria de probabilidade em semigrupos discretos. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 4 1965 78—102
• Nitis Mukhopadhyay. "Uma conversa com Ulf Grenander". Estatista. Sci. Volume 21, Número 3 (2006), 404-426.

Fundações de estatísticas

• Anders Martin-Löf . 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Avaliação de vidas em durações de tempo abaixo de um nanossegundo"). ("Fórmula de Sundberg", de acordo com Sundberg 1971)
• Per Martin-Löf. 1966. Estatísticas do ponto de vista da mecânica estatística . Notas de aula, Mathematical Institute, Aarhus University. ("Fórmula de Sundberg" creditada a Anders Martin-Löf, de acordo com Sundberg 1971)
• Per Martin-Löf. 1970. Statistika Modeller (Modelos Estatísticos): Anteckningar fran seminarier läsåret 1969–1970 (Notas de seminários no ano acadêmico de 1969–1970), com a assistência de Rolf Sundberg. Universidade de Estocolmo.
• Martin-Löf, P. "Testes exatos, regiões de confiança e estimativas", com uma discussão por AWF Edwards , GA Barnard , DA Sprott, O. Barndorff-Nielsen, D. Basu e 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. estruturas repetitivas e a relação entre distribuições canônicas e microcanônicas em estatística e mecânica estatística. Com uma discussão de DR Cox e G. Rasch e uma resposta do autor. 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. A noção de redundância e seu uso como uma medida quantitativa do desvio entre uma hipótese estatística e um conjunto de dados observacionais. Com uma discussão por F. Abildgård, AP Dempster , D. Basu , DR Cox , AWF Edwards , DA Sprott, GA Barnard , O. Barndorff-Nielsen, JD Kalbfleisch e G. Rasch e uma resposta do autor. 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 A noção de redundância e seu uso como uma medida quantitativa da discrepância entre uma hipótese estatística e um conjunto de dados observacionais. Scand. J. Statist. 1 (1974), no. 1, 3—18.
• Sverdrup, Erling. "Testes sem energia." Scand. J. Statist. 2 (1975), no. 3, 158–160.
• Martin-Löf, por resposta ao polêmico artigo de Erling Sverdrup: `` Testes sem poder ( Scand. J. Statist. 2 (1975), no. 3, 158–160). Scand. J. Statist. 2 (1975), no. 3, 161–165.
• Sverdrup, Erling. Uma tréplica a: `` Testes sem energia ( 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. Testes exatos, regiões de confiança e estimativas. Fundamentos de probabilidade e estatística. II. Synthese 36 (1977), no. 2, 195–206.
• Rolf Sundberg. 1971. Teoria da máxima verossimilhança e aplicações para distribuições geradas ao observar uma função de uma variável de família exponencial . Dissertação, Instituto de Estatística Matemática, Universidade de Estocolmo.
• Sundberg, Rolf. Teoria da máxima verossimilhança para dados incompletos de uma família exponencial. Scand. J. Statist. 1 (1974), no. 2, 49—58.
• Sundberg, Rolf Um método iterativo para solução das equações de verossimilhança para dados incompletos de famílias exponenciais. Com. Statist. — Simulation Comput. B5 (1976), no. 1, 55-64.
• Sundberg, Rolf Alguns resultados sobre modelos decomponíveis (ou tipo Markov) para tabelas de contingência multidimensionais: distribuição de marginais e partição de testes. Scand. J. Statist. 2 (1975), no. 2, 71-79.
• Höglund, Thomas. A estimativa exata - um método de estimativa estatística. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 29 (1974), 257-271.
• Lauritzen, Steffen L. Famílias extremas e sistemas de estatísticas suficientes . Lecture Notes in Statistics, 49. Springer-Verlag, New York, 1988. xvi + 268 pp. ISBN  0-387-96872-5

Fundamentos da matemática, lógica e ciência da computação

• Per Martin-Löf. Uma teoria de tipos. Preprint, Stockholm University, 1971.
• Per Martin-Löf. Uma teoria intuicionista de tipos . Em G. Sambin e J. Smith, editores, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998. Versão reimpressa de um relatório não publicado de 1972.
• Per Martin-Löf. Uma teoria intuicionista de tipos: parte predicativa. Em HE Rose e JC Shepherdson, editores, Logic Colloquium '73, páginas 73-118. North Holland, 1975.
• Per Martin-Löf. Matemática construtiva e programação de computadores . Em Logic, Methodology and Philosophy of Science VI, 1979 . Eds. Cohen, et al. Holanda do Norte, Amsterdã. pp. 153–175, 1982.
• Per Martin-Löf. Teoria dos tipos intuicionistas . (Notas de Giovanni Sambin de uma série de palestras proferidas em Pádua, junho de 1980). Napoli, Bibliopolis, 1984.
• Per Martin-Löf. Implicações filosóficas da teoria dos tipos , notas não publicadas, 1987?
• Per Martin-Löf. Cálculo de substituição , 1992. Notas de uma palestra proferida em Gotemburgo.
• Bengt Nordström, Kent Petersson e Jan M. Smith. Programação na Teoria de Tipos de Martin-Löf . Oxford University Press, 1990. (O livro está esgotado, mas uma versão gratuita foi disponibilizada.)
• Per Martin-Löf. Sobre os significados das constantes lógicas e as justificativas das leis lógicas . Nordic Journal of Philosophical Logic , 1 (1): 11-60, 1996.
• Per Martin-Löf. Lógica e ética . Em T. Piecha e P. Schroeder-Heister, editores, Proof-Theoretic Semantics: Assessment and Future Perspectives. Proceedings of the Third Tübingen Conference on Proof-Theoretic Semantics, 27-30 de março de 2019 , páginas 227-235. URI: http://dx.doi.org/10.15496/publikation-35319 . Universidade de Tübingen 2019.

links externos

• Per Martin-Löf no Projeto Genealogia da Matemática