Per Martin -Löf - Per Martin-Löf
Per Martin-Löf | |
---|---|
narozený |
Stockholm , Švédsko
|
08.05.1942
Státní příslušnost | švédský |
Státní občanství | Švédsko |
Alma mater | Stockholmská univerzita |
Známý jako |
Náhodné sekvence Přesné testy Opakovaná struktura Dostatečná statistika Metoda maximalizace očekávání Martin-Löfova teorie typu |
Ocenění |
Cena Švédské královské akademie věd Rolfa Schocka (2020) |
Vědecká kariéra | |
Pole |
Počítačová věda Logika Matematická statistika Filozofie |
Instituce |
Univerzita Stockholm University of Chicago Aarhus University |
Doktorský poradce | Andrej N. Kolmogorov |
Per Erik Rutger Martin-Löf ( / l ɒ f / ; švédsky: [ˈmǎʈːɪn ˈløːv] ; narozen 08.5.1942 ) je švédský logik , filozof a matematický statistik . Je mezinárodně uznávaný svou prací na základech pravděpodobnosti , statistiky, matematické logiky a informatiky . Od konce 70. let byly publikace Martina-Löfa hlavně v logice . Ve filozofické logice Martin-Löf zápasil s filozofií logických důsledků a úsudku , částečně inspirovanou dílem Brentana , Frege a Husserla . V matematické logice se Martin-Löf aktivně podílel na vývoji intuicionistické teorie typů jako konstruktivního základu matematiky; Práce Martina-Löfa na teorii typů ovlivnila informatiku .
Až do svého odchodu do důchodu v roce 2009 zastával Per Martin-Löf společnou židli pro matematiku a filozofii na Stockholmské univerzitě .
Jeho bratr Anders Martin-Löf je nyní emeritním profesorem matematické statistiky na Stockholmské univerzitě; oba bratři spolupracovali na výzkumu pravděpodobnosti a statistiky. Výzkum Anderse a Per Martin-Löf ovlivnilo statistické teorii, zejména pokud jde o exponenciální rodiny , na způsob očekávání-zvětšení pro chybějící data a výběr modelu .
Per Martin-Löf je nadšený pozorovatel ptáků ; jeho první vědecká publikace byla o úmrtnosti prstencových ptáků .
Náhodnost a Kolmogorovova složitost
V letech 1964 a 1965 studoval Martin-Löf v Moskvě pod dohledem Andreje N. Kolmogorova . Napsal článek z roku 1966 Definice náhodných sekvencí, který dal první vhodnou definici náhodné sekvence.
Dřívější výzkumníci, jako například Richard von Mises, se pokusili formalizovat pojem testu náhodnosti , aby definovali náhodnou sekvenci jako sekvenci, která prošla všemi testy náhodnosti; přesná představa testu náhodnosti však zůstala vágní. Klíčovým vhledem Martina-Löfa bylo použít teorii výpočtu k formálnímu definování pojmu testu náhodnosti. To kontrastuje s představou náhodnosti v pravděpodobnosti ; v této teorii nelze o žádném konkrétním prvku prostoru vzorku říci, že je náhodný.
Od té doby bylo prokázáno, že náhodnost Martina-Löfa připouští mnoho ekvivalentních charakteristik-z hlediska komprese , testů náhodnosti a hazardu-, které se jen málo podobají původní definici, ale každá z nich splňuje naši intuitivní představu o vlastnostech, které by náhodné sekvence měly mít: náhodné sekvence by měly být nestlačitelné, měly by projít statistickými testy náhodnosti a nemělo by být možné vydělat na nich sázením . Existence těchto vícenásobných definic Martin-Löfovy náhodnosti a stabilita těchto definic v různých modelech výpočtu svědčí o tom, že Martin-Löfova náhodnost je základní vlastností matematiky, a nikoli náhodou konkrétního modelu Martina-Löfa. Teze, že definice Martin-Löf nahodilosti „korektně“ zachycuje intuitivní pojem náhodnosti byl nazýván „Martin-Löf- Chaitin práce“; je poněkud podobný tezi Church – Turing .
Po práci Martina-Löfa definuje algoritmická teorie informací náhodný řetězec jako řetězec, který nelze vytvořit z žádného počítačového programu, který je kratší než řetězec ( náhodnost Chaitin – Kolmogorov ); tj. řetězec, jehož Kolmogorovova složitost je alespoň délka řetězce. To je jiný význam, než je používání výrazu ve statistikách. Zatímco statistická náhodnost se týká procesu, který produkuje řetězec (např. Převrácení mince k produkci každého bitu náhodně vytvoří řetězec), algoritmická náhodnost se týká samotného řetězce . Algoritmická informační teorie odděluje náhodné od náhodných řetězců způsobem, který je relativně neměnný vůči použitému modelu výpočtu .
Algoritmicky náhodná sekvence je nekonečná posloupnost znaků, jejíž všechny předpony (s výjimkou případně určitým počtem výjimky) jsou řetězce, které jsou „v blízkosti“ algoritmicky náhodné (jejich délka je v konstantou jejich složitosti Kolmogorov).
Matematická statistika
Per Martin-Löf provedl důležitý výzkum v matematické statistice , která (ve švédské tradici) zahrnuje teorii pravděpodobnosti a statistiku .
Pozorování ptáků a určování pohlaví
Per Martin-Löf začal pozorování ptáků v mládí a zůstává nadšeným pozorovatelem ptáků. Jako teenager publikoval článek o odhadování úmrtnosti ptáků pomocí údajů z kroužkování ptáků ve švédském zoologickém časopise: Tento článek byl brzy citován v předních mezinárodních časopisech a tento dokument je citován i nadále.
V biologii a statistiky z ptáků , existuje několik problémů s chybějícími údaji . Martin-Löfův první článek pojednal o problému odhadování úmrtnosti druhů Dunlin pomocí metod zachycení a opětovného zachycení . Druhý problém chybějících údajů vzniká studiem pohlaví ptáků. Problém stanovení biologického pohlaví ptáka, který je pro člověka extrémně obtížný, je jedním z prvních příkladů přednášek Martina-Löfa o statistických modelech .
Pravděpodobnost na algebraických strukturách
Martin-Löf napsal licenční práci o pravděpodobnosti algebraických struktur, zejména pologrup, výzkumného programu vedeného Ulfem Grenanderem na Stockholmské univerzitě.
Statistické modely
Martin-Löf vyvinul inovativní přístupy ke statistické teorii . Ve své knize „na stoly náhodných čísel“, Kolmogorov poznamenal, že četnost pravděpodobnost představa o omezujících vlastností nekonečných posloupností neposkytla základ pro statistiku, který bere v úvahu pouze konečných vzorků. Hodně z práce Martina-Löfa ve statistice bylo poskytnout základ pro konečný vzorek statistik.
Výběr modelu a testování hypotéz
V sedmdesátých letech Per Martin-Löf významně přispěl ke statistické teorii a inspiroval další výzkum, zejména skandinávskými statistiky včetně Rolfa Sundberga, Thomase Höglunda a Steffana Lauritzena. V této práci vedl předchozí výzkum Martina-Löfa o měření pravděpodobnosti na pologrupách k pojmu „opakující se struktura“ a k novému zpracování dostatečné statistiky, ve které byly charakterizovány jednoparametrické exponenciální rodiny . Poskytl kategoriálně teoretický přístup k vnořeným statistickým modelům pomocí principů konečných vzorků. Před (a po) Martinovi-Löfovi byly takovéto vnořené modely často testovány pomocí testů chi-square hypotéz, jejichž ospravedlnění je pouze asymptotické (a tak nepodstatné pro skutečné problémy, které mají vždy konečné vzorky).
Metoda maximalizace očekávání pro exponenciální rodiny
Martin-Löfův student, Rolf Sundberg, vyvinul podrobnou analýzu metody maximalizace očekávání (EM) pro odhad pomocí dat z exponenciálních rodin, zejména s chybějícími daty . Sundberg připisuje vzorec, později známý jako Sundbergův vzorec, předchozím rukopisům bratrů Martin-Löfů, Per a Anders . Mnoho z těchto výsledků dosáhlo mezinárodní vědecké komunity prostřednictvím článku z roku 1976 o metodě maximalizace očekávání (EM) od Arthura P. Dempstera , Nan Lairda a Donalda Rubina , který byl publikován v předním mezinárodním časopise sponzorovaném Královskou statistickou společností .
Logika
Filozofická logika
Ve filozofické logice Per Martin-Löf publikoval články o teorii logických důsledků , o soudech atd. Zajímal se o středoevropské filozofické tradice, zejména o německy psané spisy Franze Brentana , Gottlob Frege a Edmund Husserl .
Teorie typů
Martin-Löf pracuje v matematické logice po mnoho desetiletí.
V letech 1968 až 69 pracoval jako odborný asistent na Chicagské univerzitě, kde se setkal s Williamem Alvinem Howardem, s nímž diskutoval o problémech souvisejících s korespondencí Curry -Howarda . Martin-Löf první návrh článku o datech typu teorie zpět do roku 1971. Tato impredicative teorii všeobecný Girard je System F . Tento systém se však ukázal být nekonzistentní kvůli Girardovu paradoxu, který objevil Girard při studiu systému U, což je nekonzistentní rozšíření systému F. Tato zkušenost vedla Per Martina-Löfa k rozvoji filozofických základů teorie typů , jeho vysvětlení významu , forma důkaz-teoretické sémantiky , která ospravedlňuje teorii predikativního typu, jak je představena v jeho knize Bibliopolis z roku 1984, a rozšířila se v řadě stále filozofičtějších textů, jako je například jeho vlivný Na významy logických konstant a ospravedlnění logických zákonů .
Teorie typů z roku 1984 byla extenzivní, zatímco teorie typů představená v knize Nordström et al. v roce 1990, což bylo silně ovlivněno jeho pozdějšími myšlenkami, intenzivními a přístupnějšími pro implementaci na počítači.
Martin-Löfova intuicionistická teorie typů rozvinula pojem závislých typů a přímo ovlivnila vývoj počtu konstrukcí a logického rámce LF . Řada populárních počítačově ověřených systémů je založena na teorii typů, například NuPRL , LEGO, Coq , ALF, Agda , Twelf , Epigram a Idris .
Ocenění
Martin-Löf je členem Královské švédské akademie věd a Academia Europaea .
Viz také
Poznámky
Reference
Pozorování ptáků a chybějící data
- Martin-Löf, P. (1961). „Výpočty úmrtnosti na prstencových ptácích se zvláštním zřetelem na Dunlin Calidris alpina “. Arkiv för Zoologi (Zoology Files), Kungliga Svenska Vetenskapsakademien (The Royal Swedish Academy of Sciences) Serie 2 . Pásmo 13 (21).
- George A. Barnard , „Gone Birdwatching“ , New Scientist , 4. prosince 1999, číslo časopisu 2215.
- Seber, GAF (2002). Odhad hojnosti zvířat a souvisejících parametrů . Caldwel, New Jersey: Blackburn Press. ISBN 1-930665-55-5.
- Royle, JA; RM Dorazio (2008). Hierarchické modelování a odvozování v ekologii . Elsevier. ISBN 978-1-930665-55-2.
Základy pravděpodobnosti
- Per Martin-Löf. "Definice náhodných sekvencí." Informace a kontrola , 9 (6): 602–619, 1966.
- Li, Ming a Vitányi, Paul, An Introduction to Kolmogorov Complexity and its Applications , Springer, 1997. Úvod kapitoly full-text .
Pravděpodobnost na algebraických strukturách, následovat Ulf Grenander
- Grenander, Ulf . Pravděpodobnost na algebraických strukturách . (Dover dotisk)
- Martin-Löf, P. Věta o kontinuitě na lokálně kompaktní skupině. Teor. Verojatnost. i Primenen. 10 1965 367–371.
- Martin-Löf, Per. Teorie pravděpodobnosti na diskrétních poloskupinách. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 4 1965 78—102
- Nitis Mukhopadhyay. „Rozhovor s Ulfem Grenanderem“. Statistik Sci. Svazek 21, číslo 3 (2006), 404–426.
Statistické nadace
- Anders Martin-Löf . 1963. „Utvärdering av livslängder i subnanosekundsområdet“ („Hodnocení životů v časových délkách pod jednu nanosekundu“). („Sundbergův vzorec“, podle Sundberg 1971)
- Per Martin-Löf. 1966. Statistiky z pohledu statistické mechaniky . Přednášky, Matematický ústav, Aarhuská univerzita. („Sundbergův vzorec“ připsán Andersovi Martinovi-Löfovi, podle Sundberga 1971)
- Per Martin-Löf. 1970. Statistika Modeller (Statistické modely): Anteckningar fran seminarier läsåret 1969–1970 (Poznámky ze seminářů v akademickém roce 1969–1970), za pomoci Rolfa Sundberga. Stockholmská univerzita.
- Martin-Löf, P. „Přesné testy, oblasti spolehlivosti a odhady“, s diskusí AWF Edwards , GA Barnard , DA Sprott, O. Barndorff-Nielsen, D. Basu a G. Rasch . Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), s. 121–138. Vzpomínky, č. 1, oddělení teoretik. Statist., Inst. Matematika, Univ. Aarhus, Aarhus, 1974.
- Martin-Löf, P. Repetitivní struktury a vztah mezi kanonickými a mikrokanonickými distribucemi ve statistice a statistické mechanice. S diskusí DR Coxe a G. Rascha a odpovědí autora. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), str. 271–294. Vzpomínky, č. 1, odd. Teoretik. Statist., Inst. Matematika, Univ. Aarhus, Aarhus, 1974.
- Martin-Löf, P. Pojem redundance a její použití jako kvantitativní měřítko odchylky mezi statistickou hypotézou a souborem pozorovacích dat. S diskusí F. Abildgård, AP Dempster , D. Basu , DR Cox , AWF Edwards , DA Sprott, GA Barnard , O. Barndorff-Nielsen, JD Kalbfleisch a G. Rasch a odpovědí autora. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), s. 1–42. Vzpomínky, č. 1, odd. Teoretik. Statist., Inst. Matematika, Univ. Aarhus, Aarhus, 1974.
- Martin-Löf, Per Pojem redundance a jeho použití jako kvantitativní měřítko rozporu mezi statistickou hypotézou a souborem pozorovacích dat. Skandovat. J. Statist. 1 (1974), č. 1, 3—18.
- Sverdrup, Erling. "Testy bez proudu." Skandovat. J. Statist. 2 (1975), č. 3, 158–160.
- Martin-Löf, Per Reply to the Erling Sverdrup's polemical article: `` Tests without power ( Scand. J. Statist. 2 (1975), no. 3, 158–160). Skandovat. J. Statist. 2 (1975), č. 3, 161–165.
- Sverdrup, Erling. Opakování : `` Testy bez napájení ( Scand. J. Statist. 2 (1975), 161-165) od P. Martin-Löf. Skandovat. J. Statist. 4 (1977), č. 3, 136—138.
- Martin-Löf, P. Přesné testy, oblasti spolehlivosti a odhady. Základy pravděpodobnosti a statistiky. II. Synthese 36 (1977), č. 2, 195—206.
- Rolf Sundberg. 1971. Teorie maximální pravděpodobnosti a aplikace pro distribuce generované při pozorování funkce exponenciální rodinné proměnné . Disertační práce, Institute for Mathematical Statistics, Stockholm University.
- Sundberg, Rolf. Teorie maximální pravděpodobnosti pro neúplná data z exponenciální rodiny. Skandovat. J. Statist. 1 (1974), č. 2, 49—58.
- Sundberg, Rolf iterační metoda pro řešení rovnic pravděpodobnosti pro neúplná data z exponenciálních rodin. Comm. Statist — Simulation Comput. B5 (1976), č. 1, 55—64.
- Sundberg, Rolf Některé výsledky o rozložitelných (nebo Markovově typu) modelech pro vícerozměrné kontingenční tabulky: rozdělení okrajů a rozdělení testů. Skandovat. J. Statist. 2 (1975), č. 2, 71—79.
- Höglund, Thomas. Přesný odhad - metoda statistického odhadu. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 29 (1974), 257—271.
- Lauritzen, Steffen L. Extrémní rodiny a systémy dostatečné statistiky . Lecture Notes in Statistics, 49. Springer-Verlag, New York, 1988. xvi+268 s. ISBN 0-387-96872-5
Základy matematiky, logiky a informatiky
- Per Martin-Löf. Teorie typů. Preprint, Stockholm University, 1971.
- Per Martin-Löf. Intuicionistická teorie typů . V G. Sambin a J. Smith, redaktoři, Dvacet pět let konstruktivní teorie typu. Oxford University Press, 1998. Přetištěná verze nepublikované zprávy z roku 1972.
- Per Martin-Löf. Intuicionistická teorie typů: Predikativní část. V HE Rose a JC Shepherdsonovi, redaktoři, Logic Colloquium '73, strany 73–118. Severní Holandsko, 1975.
- Per Martin-Löf. Konstruktivní matematika a počítačové programování . In Logika, metodologie a filozofie vědy VI, 1979 . Eds. Cohen a kol. Severní Holandsko, Amsterdam. s. 153–175, 1982.
- Per Martin-Löf. Intuicionalistická teorie typů . (Poznámky Giovanni Sambina ze série přednášek pořádaných v Padově, červen 1980). Neapol, Bibliopolis, 1984.
- Per Martin-Löf. Filozofické implikace teorie typů , nepublikované poznámky, 1987?
- Per Martin-Löf. Substituční kalkul , 1992. Poznámky z přednášky v Göteborgu.
- Bengt Nordström, Kent Petersson a Jan M. Smith. Programování v Martinově-Löfově teorii typů . Oxford University Press, 1990. (Kniha se již nevydává, ale byla zpřístupněna bezplatná verze .)
- Per Martin-Löf. O významech logických konstant a ospravedlnění logických zákonů . Nordic Journal of Philosophical Logic , 1 (1): 11–60, 1996.
- Per Martin-Löf. Logika a etika . 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.