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

Per Martin-Löf
Per Martin-Löf w 2004 r.
Urodzić się	( 1942-05-08 )8 maja 1942 (wiek 79) Sztokholm , Szwecja
Narodowość	szwedzki
Obywatelstwo	Szwecja
Alma Mater	Uniwersytet Sztokholmski
Znany z	Ciągi losowe Dokładne testy Struktura powtarzalna Statystyka dostateczna Metoda maksymalizacji oczekiwań Teoria typu Martina-Löfa
Nagrody	Nagroda Królewskiej Szwedzkiej Akademii Nauk im. Rolfa Schocka (2020)
Kariera naukowa
Pola	Informatyka Logika Statystyka matematyczna Filozofia
Instytucje	Uniwersytet Sztokholmski Uniwersytet w Chicago Uniwersytet Aarhus
Doradca doktorski	Andrei N. Kołmogorowa

Per Erik Rutger Martin-Löf ( / l ɒ f / ; szwedzki:  [ˈmǎʈːɪn ˈløːv] ; ur. 8 maja 1942) to szwedzki logik , filozof i statystyk matematyczny . Jest znany na całym świecie ze swojej pracy nad podstawami rachunku prawdopodobieństwa , statystyki, logiki matematycznej i informatyki . Od późnych lat 70. publikacje Martina-Löfa były głównie logiczne . W logice filozoficznej Martin-Löf zmagał się z filozofią logicznej konsekwencji i osądu , częściowo inspirowaną twórczością Brentano , Fregego i Husserla . W logice matematycznej Martin-Löf aktywnie rozwijał intuicjonistyczną teorię typów jako konstruktywną podstawę matematyki; Praca Martina-Löfa nad teorią typów wpłynęła na informatykę .

Do czasu przejścia na emeryturę w 2009 r. Per Martin-Löf pełnił funkcję wspólnej katedry matematyki i filozofii na Uniwersytecie Sztokholmskim .

Jego brat Anders Martin-Löf jest obecnie emerytowanym profesorem statystyki matematycznej na Uniwersytecie Sztokholmskim; obaj bracia współpracowali w badaniach prawdopodobieństwa i statystyki. Badania Andersa i Pera Martina-Löfa wpłynęły na teorię statystyczną, zwłaszcza dotyczącą rodzin wykładniczych , metody maksymalizacji oczekiwań dla brakujących danych oraz doboru modelu .

Per Martin-Löf jest zapalonym obserwatorem ptaków ; jego pierwsza publikacja naukowa dotyczyła śmiertelności ptaków obrączkowanych .

Losowość i złożoność Kołmogorowa

W latach 1964 i 1965 Martin-Löf studiował w Moskwie pod kierunkiem Andrieja N. Kołmogorowa . W 1966 r. napisał artykuł Definicja ciągów losowych, który podał pierwszą odpowiednią definicję ciągu losowego.

Wcześniejsi badacze, tacy jak Richard von Mises, próbowali sformalizować pojęcie testu na losowość , aby zdefiniować ciąg losowy jako taki, który przeszedł wszystkie testy na losowość; jednak dokładne pojęcie testu losowości pozostało niejasne. Kluczowym spostrzeżeniem Martina-Löfa było wykorzystanie teorii obliczeń do formalnego zdefiniowania pojęcia testu na losowość. Kontrastuje to z ideą losowości w prawdopodobieństwie ; w tej teorii o żadnym konkretnym elemencie przestrzeni próbki nie można powiedzieć, że jest losowy.

Od tego czasu wykazano, że losowość Martina-Löfa dopuszcza wiele równoważnych charakteryzacji — pod względem kompresji , testów losowości i hazardu — które mają niewielkie zewnętrzne podobieństwo do pierwotnej definicji, ale każda z nich spełnia nasze intuicyjne wyobrażenie o właściwościach, jakie powinny mieć ciągi losowe. posiadają: losowe sekwencje powinny być nieściśliwy, powinni przechodzić testy statystyczne dla losowości, a powinno być niemożliwe, aby zarabiać pieniądze zakłady na nich. Istnienie tych wielu definicji losowości Martina-Löfa oraz stabilność tych definicji w różnych modelach obliczeniowych, dostarczają dowodów, że losowość Martina-Löfa jest fundamentalną właściwością matematyki, a nie przypadkiem konkretnego modelu Martina-Löfa. Tezę, że definicja losowości Martina-Löfa „poprawnie” oddaje intuicyjne pojęcie losowości, została nazwana „Tezą Martina-Löfa- Chaitina ”; jest ona nieco podobna do tezy Kościoła-Turinga .

Idąc za pracą Martina-Löfa, algorytmiczna teoria informacji definiuje ciąg losowy jako taki, którego nie można wytworzyć z żadnego programu komputerowego, który jest krótszy niż ciąg ( losowość Chaitina-Kolmogorova ); tj. ciąg, którego złożoność Kołmogorowa jest co najmniej długością ciągu. Jest to inne znaczenie niż użycie tego terminu w statystykach. Podczas gdy losowość statystyczna odnosi się do procesu, w którym powstaje ciąg (np. rzucanie monetą w celu wytworzenia każdego bitu spowoduje losowe wytworzenie ciągu), losowość algorytmiczna odnosi się do samego ciągu . Algorytmiczna teoria informacji oddziela ciągi losowe od nielosowych w sposób, który jest względnie niezmienny w stosunku do używanego modelu obliczeń .

Algorytmicznie losowy ciąg jest nieskończony ciąg znaków, którego wszystkie prefiksy (z wyjątkiem ewentualnie skończonej liczby wyjątkami) są ciągi, które są „blisko” algorytmicznie losowej (ich długość jest w stałej ich złożoność Kołmogorowa).

Statystyki matematyczne

Per Martin-Löf przeprowadził ważne badania w dziedzinie statystyki matematycznej , która (w tradycji szwedzkiej) obejmuje teorię prawdopodobieństwa i statystykę .

Obserwacja ptaków i determinacja płci

Per Martin-Löf zaczął obserwować ptaki w młodości i pozostaje entuzjastycznym obserwatorem ptaków. Jako nastolatek opublikował w szwedzkim czasopiśmie zoologicznym artykuł na temat szacowania współczynników śmiertelności ptaków na podstawie danych z obrączkowania ptaków : Artykuł ten został wkrótce zacytowany w wiodących międzynarodowych czasopismach i ten artykuł jest cytowany nadal.

W biologii i statystyk z ptakami , istnieje kilka problemów z brakującymi danymi . Pierwszy artykuł Martina-Löfa omawiał problem szacowania współczynników śmiertelności gatunków Dunlin przy użyciu metod wychwytu-odzyskania . Drugi problem braku danych pojawia się przy badaniu płci ptaków. Niezwykle trudny dla człowieka problem określenia płci biologicznej ptaka jest jednym z pierwszych przykładów w wykładach Martina-Löfa o modelach statystycznych .

Prawdopodobieństwo na strukturach algebraicznych

Martin-Löf napisał pracę licencjacką na temat prawdopodobieństwa struktur algebraicznych, zwłaszcza półgrup, programu badawczego prowadzonego przez Ulfa Grenandera na Uniwersytecie Sztokholmskim.

Modele statystyczne

Martin-Löf opracował innowacyjne podejście do teorii statystycznej . W swoim artykule „On Tables of Random Numbers” Kołmogorow zauważył, że pojęcie prawdopodobieństwa częstości ograniczających własności ciągów nieskończonych nie stanowi podstawy dla statystyki, która uwzględnia tylko próbki skończone. Znaczna część pracy Martina-Löfa w statystyce polegała na stworzeniu podstawy dla statystyki opartej na skończonej próbie.

Wybór modelu i testowanie hipotez

W latach siedemdziesiątych Per Martin-Löf wniósł ważny wkład w teorię statystyczną i zainspirował dalsze badania, zwłaszcza ze strony statystyków skandynawskich, w tym Rolfa Sundberga, Thomasa Höglunda i Steffana Lauritzena. W tej pracy, wcześniejsze badania Martina-Löfa nad miarami prawdopodobieństwa na półgrupach doprowadziły do ​​pojęcia „struktury powtarzalnej” i nowatorskiego traktowania wystarczających statystyk, w których scharakteryzowano jednoparametrowe rodziny wykładnicze . Przedstawił podejście oparte na teorii kategorii do zagnieżdżonych modeli statystycznych , wykorzystując zasady próby skończonej. Przed (i po) Martin-Löf takie zagnieżdżone modele były często testowane za pomocą testów hipotez chi-kwadrat, których uzasadnienia są jedynie asymptotyczne (a więc nieistotne dla rzeczywistych problemów, które zawsze mają skończone próbki).

Metoda maksymalizacji oczekiwań dla rodzin wykładniczych

Uczeń Martina-Löfa, Rolf Sundberg, opracował szczegółową analizę metody maksymalizacji oczekiwań (EM) do estymacji przy użyciu danych z rodzin wykładniczych, zwłaszcza z brakującymi danymi . Sundberg przypisuje formułę, później znaną jako formuła Sundberga, poprzednim rękopisom braci Martin-Löf, Pera i Andersa . Wiele z tych wyników dotarło do międzynarodowej społeczności naukowej w artykule z 1976 roku na temat metody maksymalizacji oczekiwań (EM) autorstwa Arthura P. Dempstera , Nan Laird i Donalda Rubina , opublikowanym w wiodącym międzynarodowym czasopiśmie sponsorowanym przez Królewskie Towarzystwo Statystyczne .

Logika

Logika filozoficzna

W dziedzinie logiki filozoficznej Per Martin-Löf publikował prace na temat teorii konsekwencji logicznej , sądów itp. Interesował się środkowoeuropejskimi tradycjami filozoficznymi, zwłaszcza niemieckojęzycznymi pismami Franza Brentano , Gottloba Fregego i Edmunda Husserla .

Teoria typów

Martin-Löf od dziesięcioleci zajmuje się logiką matematyczną .

W latach 1968-69 pracował jako adiunkt na Uniwersytecie w Chicago, gdzie poznał Williama Alvina Howarda, z którym omawiał kwestie związane z korespondencją Curry–Howard . Pierwszy projekt artykułu Martina-Löfa na temat teorii typów pochodzi z 1971 roku. Ta implikacyjna teoria uogólniła system F Girarda . Jednak ten system okazał się niespójny z powodu paradoksu Girarda, który został odkryty przez Girarda podczas badania Systemu U, niespójnego rozszerzenia Systemu F. To doświadczenie doprowadziło Pera Martina-Löfa do opracowania filozoficznych podstaw teorii typów , jego wyjaśnienia znaczenia , forma semantyki dowodowo -teoretycznej , która uzasadnia teorię typów predykatywnych przedstawioną w jego książce Bibliopolis z 1984 r. i rozszerzoną w wielu coraz bardziej filozoficznych tekstach, takich jak jego wpływowe „ O znaczeniach stałych logicznych i uzasadnieniach praw logicznych” .

Teoria typów z 1984 roku była ekstensjonalna, podczas gdy teoria typów przedstawiona w książce Nordströma et al. w 1990 roku, na który duży wpływ miały jego późniejsze pomysły, zamierzone i bardziej podatne na implementację na komputerze.

Intuicjonistyczna teoria typów Martina-Löfa rozwinęła pojęcie typów zależnych i bezpośrednio wpłynęła na rozwój rachunku konstrukcji i ramy logicznej LF . Wiele popularnych komputerowych systemów dowodowych opiera się na teorii typów, na przykład NuPRL , LEGO, Coq , ALF, Agda , Twelf , Epigram i Idris .

Nagrody

Martin-Löf jest członkiem Królewskiej Szwedzkiej Akademii Nauk i Academia Europaea .

Zobacz też

Uwagi

Bibliografia

Obserwacja ptaków i brakujące dane

• Martin-Löf, P. (1961). „Obliczenia śmiertelności ptaków obrączkowanych ze szczególnym uwzględnieniem Dunlin Calidris alpina ”. Arkiv för Zoologi (pliki zoologiczne), Kungliga Svenska Vetenskapsakademien (Królewska Szwedzka Akademia Nauk) Serie 2 . Zespół 13 (21).

• George A. Barnard , „Gone Birdwatching” , New Scientist , 4 grudnia 1999, numer 2215.
• Seber, GAF (2002). Szacowanie liczebności zwierząt i powiązanych parametrów . Caldwel, New Jersey: Blackburn Press. Numer ISBN 1-930665-55-5.
• Royle, JA; RM Dorazio (2008). Modelowanie hierarchiczne i wnioskowanie w ekologii . Elsevier. Numer ISBN 978-1-930665-55-2.

Podstawy prawdopodobieństwa

• Według Martina-Löfa. „Definicja losowych sekwencji”. Informacja i kontrola , 9(6): 602–619, 1966.
• Li, Ming i Vitányi, Paul, An Introduction to Kolmogorov Complexity and Its Applications , Springer, 1997. Pełny tekst rozdziału wprowadzającego .

Prawdopodobieństwo na strukturach algebraicznych, za Ulfem Grenanderem

• Grenander, Ulf . Prawdopodobieństwo na strukturach algebraicznych . (Przedruk Dover)
• Martin-Löf, P. Twierdzenie o ciągłości na grupie lokalnie zwartej. Teor. Verojatnost. w Primenen. 10 1965 367-371.
• Martin-Löf, Per. Teoria prawdopodobieństwa na półgrupach dyskretnych. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 4 1965 78—102
• Nitis Mukhopadhyay. „Rozmowa z Ulfem Grenanderem”. Statystyk. Nauka. Tom 21, Numer 3 (2006), 404-426.

Podstawy statystyki

• Andersa Martina-Löfa . 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Ocena długości życia w czasie poniżej jednej nanosekundy"). („Formuła Sundberga”, według Sundberga 1971)
• Według Martina-Löfa. 1966. Statystyka z punktu widzenia mechaniki statystycznej . Notatki z wykładów, Instytut Matematyczny, Uniwersytet w Aarhus. („Formuła Sundberga” przypisywana Andersowi Martinowi-Löfowi, według Sundberg 1971)
• Według Martina-Löfa. 1970. Statistika Modeller (Modele statystyczne): Anteckningar fran seminarier läsåret 1969–1970 (Notatki z seminariów w roku akademickim 1969–1970), z pomocą Rolfa Sundberga. Uniwersytet Sztokholmski.
• Martin-Löf, P. „Dokładne testy, regiony ufności i szacunki”, z dyskusją AWF Edwards , GA Barnarda , DA Sprotta, O. Barndorffa-Nielsena, D. Basu i G. Rascha . Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), s. 121–138. Pamiętniki, nr 1, Wydział Teorii. Statystyka, Inst. Matematyka, Uniw. Aarhus, Aarhus, 1974.
• Martin-Löf, P. Struktury powtarzalne i związek między rozkładami kanonicznymi i mikrokanonicznymi w statystyce i mechanice statystycznej. Z dyskusją DR Coxa i G. Rascha oraz odpowiedzią autora. Proceedings of Conference on Fundamental Questions in Statistical Inference (Aarhus, 1973), s. 271–294. Pamiętniki, nr 1, Wydział Teorii. Statystyka, Inst. Matematyka, Uniw. Aarhus, Aarhus, 1974.
• Martin-Löf, P. Pojęcie redundancji i jego zastosowanie jako ilościowej miary odchylenia hipotezy statystycznej od zbioru danych obserwacyjnych. Z dyskusją F. Abildgårda, AP Dempstera , D. Basu , DR Coxa , AWF Edwardsa , DA Sprotta, GA Barnarda , O. Barndorffa-Nielsena, JD Kalbfleischa i G. Rascha oraz odpowiedzi autora. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), s. 1-42. Pamiętniki, nr 1, Wydział Teorii. Statystyka, Inst. Matematyka, Uniw. Aarhus, Aarhus, 1974.
• Martin-Löf, Per Pojęcie redundancji i jego zastosowanie jako ilościowej miary rozbieżności między hipotezą statystyczną a zbiorem danych obserwacyjnych. Skanowanie. J. Statysta. 1 (1974), nr. 1, 3-18.
• Sverdrup, Erling. „Testy bez zasilania”. Skanowanie. J. Statysta. 2 (1975), nr. 3, 158–160.
• Martin-Löf, Per Reply na artykuł polemiczny Erlinga Sverdrupa: „Tests without power” ( Scand. J. Statist. 2 (1975), nr 3, 158–160). Skanowanie. J. Statysta. 2 (1975), nr. 3, 161-165.
• Sverdrup, Erling. Odpowiedź na: „Testy bez mocy” ( Scand. J. Statist. 2 (1975), 161-165) P. Martin-Löf. Skanowanie. J. Statysta. 4 (1977), nr. 3, 136-138.
• Martin-Löf, P. Dokładne testy, obszary ufności i szacunki. Podstawy rachunku prawdopodobieństwa i statystyki. II. Synteza 36 (1977), nr. 2, 195-206.
• Rolfa Sundberga. 1971. Teoria największej wiarogodności i zastosowania rozkładów generowanych podczas obserwacji funkcji wykładniczej zmiennej rodziny . Praca doktorska, Instytut Statystyki Matematycznej, Uniwersytet Sztokholmski.
• Sundberg, Rolf. Teoria największej wiarygodności dla niekompletnych danych z rodziny wykładniczej. Skanowanie. J. Statysta. 1 (1974), nr. 2, 49-58.
• Sundberg, Rolf Iteracyjna metoda rozwiązywania równań wiarygodności dla niekompletnych danych z rodzin wykładniczych. Komunik. Statist. — Obliczenia symulacyjne. B5 (1976), nr. 1, 55-64.
• Sundberg, Rolf Niektóre wyniki dotyczące modeli dekompozycyjnych (lub typu Markowa) dla wielowymiarowych tablic kontyngencji: rozkłady marginesów i podział testów. Skanowanie. J. Statysta. 2 (1975), nr. 2, 71-79.
• Hoglund, Thomas. Dokładne oszacowanie — metoda estymacji statystycznej. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 29 (1974), 257-271.
• Lauritzen, Steffen L. Ekstremalne rodziny i systemy statystyki wystarczającej . Wykład Uwagi w Statystyce, 49. Springer-Verlag, New York, 1988. xvi + 268 pp. ISBN  0-387-96872-5

Podstawy matematyki, logiki i informatyki

• Według Martina-Löfa. Teoria typów. Preprint, Uniwersytet Sztokholmski, 1971.
• Według Martina-Löfa. Intuicjonistyczna teoria typów . W G. Sambin i J. Smith, redaktorzy, Dwadzieścia pięć lat konstruktywnej teorii typów. Oxford University Press, 1998. Przedrukowana wersja niepublikowanego raportu z 1972 roku.
• Według Martina-Löfa. Intuicjonistyczna teoria typów: Część predykacyjna. W HE Rose i JC Shepherdson, redaktorzy, Logic Colloquium '73, strony 73–118. Holandia Północna, 1975.
• Według Martina-Löfa. Matematyka konstruktywna i programowanie komputerowe . W Logic, Methodology and Philosophy of Science VI, 1979 . Wyd. Cohen i in. Północna Holandia, Amsterdam. s. 153-175, 1982.
• Według Martina-Löfa. Teoria typów intuicjonistycznych . (Notatki Giovanniego Sambina z serii wykładów wygłoszonych w Padwie, czerwiec 1980). Neapol, Bibliopolis, 1984.
• Według Martina-Löfa. Filozoficzne implikacje teorii typów , Notatki niepublikowane, 1987?
• Według Martina-Löfa. Rachunek podstawień , 1992. Notatki z wykładu wygłoszonego w Göteborgu.
• Bengt Nordström, Kent Petersson i Jan M. Smith. Programowanie w teorii typów Martina-Löfa . Oxford University Press, 1990. (Książka jest wyczerpana, ale udostępniono darmową wersję ).
• Według Martina-Löfa. O znaczeniach stałych logicznych i uzasadnieniach praw logicznych . Nordic Journal of Philosophical Logic , 1(1): 11-60, 1996.
• Według Martina-Löfa. Logika i Etyka . W redakcjach T. Piecha i P. Schroeder-Heister, Proof-Theoretic Semantics: Assessment and Future Perspectives. Proceedings of the Third Tübingen Conference on Proof-Theoretic Semantics, 27-30 marca 2019 , s. 227-235. URI: http://dx.doi.org/10.15496/publikation-35319 . Uniwersytet w Tybindze 2019.

Linki zewnętrzne

• Per Martin-Löf na projekcie Genealogia Matematyki