Per Martin-Löf

Per Martin-Löf
Per MartinLoef.jpg
Per Martin-Löf 2004
Född ( 1942-05-08 ) 8 maj 1942 (80 år)
Stockholm , Sverige
Nationalitet svenska
Medborgarskap Sverige
Alma mater Stockholms universitet
Känd för





Slumpsekvenser Exakta tester Repetitiv struktur Tillräcklig statistik Förväntningsmaximeringsmetod Martin-Löf typteori Martin-Löf slumpmässighet
Utmärkelser
Vetenskaplig karriär
Fält


Datavetenskap Logik Matematisk statistik Filosofi
institutioner

Stockholm University University of Chicago Aarhus University
Doktorand rådgivare Andrei N. Kolmogorov

Per Erik Rutger Martin-Löf ( / l ɒ f / ; svenska: [ˈmǎʈːɪn ˈløːv] ; född 8 maj 1942) är en svensk logiker , filosof och matematisk statistiker . Han är internationellt känd för sitt arbete med grunderna för sannolikhet , statistik, matematisk logik och datavetenskap . Sedan slutet av 1970-talet har Martin-Löfs publikationer huvudsakligen varit logiska . Inom filosofisk logik har Martin-Löf brottats med filosofin om logisk konsekvens och bedömning , delvis inspirerad av Brentanos , Freges och Husserls verk . Inom matematisk logik har Martin-Löf varit aktiv i att utveckla intuitionistisk typteori som en konstruktiv grund för matematiken; Martin-Löfs arbete med typteori har påverkat datavetenskapen .

Fram till sin pensionering 2009 hade Per Martin-Löf en gemensam professur för matematik och filosofi vid Stockholms universitet .

Hans bror Anders Martin-Löf är numera emeritusprofessor i matematisk statistik vid Stockholms universitet; de två bröderna har samarbetat i forskning inom sannolikhet och statistik. Anders och Per Martin-Löfs forskning har påverkat statistisk teori, särskilt när det gäller exponentiella familjer , förväntningsmaximeringsmetoden för saknad data och modellval .

Per Martin-Löf disputerade 1970 vid Stockholms universitet under Andrey Kolmogorov .

Martin-Löf är en entusiastisk fågelskådare ; hans första vetenskapliga publikation handlade om dödligheten för ringmärkta fåglar .

Slumpmässighet och Kolmogorov-komplexitet

Huvudartikel: Algoritmiskt slumpmässig sekvens
Se även: Kolmogorovs komplexitet och Algoritmisk informationsteori

1964 och 1965 studerade Martin-Löf i Moskva under ledning av Andrei N. Kolmogorov . Han skrev en artikel 1966 Definitionen av slumpmässiga sekvenser som gav den första lämpliga definitionen av en slumpmässig sekvens.

Tidigare forskare som Richard von Mises hade försökt att formalisera uppfattningen om ett test för slumpmässighet för att definiera en slumpmässig sekvens som en som klarade alla tester för slumpmässighet; den exakta uppfattningen om ett slumpmässigt test lämnades dock vagt. Martin-Löfs nyckelinsikt var att använda beräkningsteorin för att formellt definiera begreppet ett test för slumpmässighet. Detta står i kontrast till idén om slumpmässighet i sannolikhet ; i den teorin kan inget särskilt element i ett urvalsutrymme sägas vara slumpmässigt.

Martin-Löfs slumpmässighet har sedan dess visat sig medge många likvärdiga karaktäriseringar - i termer av komprimering , slumpmässighetstester och spel - som inte har några yttre likheter med den ursprungliga definitionen, men som var och en tillfredsställer vår intuitiva uppfattning om egenskaper som slumpmässiga sekvenser borde har: slumpmässiga sekvenser ska vara inkompressibla, de ska klara statistiska tester för slumpmässighet och det ska vara omöjligt att tjäna pengar på att satsa på dem. Förekomsten av dessa multipla definitioner av Martin-Löfs slumpmässighet, och stabiliteten hos dessa definitioner under olika beräkningsmodeller, ger bevis för att Martin-Löfs slumpmässighet är en grundläggande egenskap hos matematiken och inte en tillfällighet av Martin-Löfs speciella modell. Tesen att definitionen av Martin-Löfs slumpmässighet "korrekt" fångar den intuitiva föreställningen om slumpmässighet har kallats "Martin-Löf– Chaitin- uppsatsen"; den liknar något av avhandlingen Church–Turing .

Efter Martin-Löfs arbete definierar algoritmisk informationsteori en slumpmässig sträng som en som inte kan produceras från något datorprogram som är kortare än strängen ( Chaitin–Kolmogorov randomness ) ; dvs en sträng vars Kolmogorov-komplexitet är åtminstone strängens längd. Detta är en annan betydelse än användningen av termen i statistik. Medan statistisk slumpmässighet hänvisar till processen som producerar strängen (t.ex. att vända ett mynt för att producera varje bit kommer slumpmässigt att producera en sträng), hänvisar algoritmisk slumpmässighet till själva strängen . Algoritmisk informationsteori separerar slumpmässiga från icke-slumpmässiga strängar på ett sätt som är relativt oföränderligt för den beräkningsmodell som används.

En algoritmiskt slumpmässig sekvens är en oändlig sekvens av tecken, vars alla prefix (förutom möjligen ett ändligt antal undantag) är strängar som är "nära" algoritmiskt slumpmässigt (deras längd ligger inom en konstant av deras Kolmogorov-komplexitet).

Matematisk statistik

Per Martin-Löf har gjort viktig forskning inom matematisk statistik , som (i svensk tradition) omfattar sannolikhetsteori och statistik .

Fågelskådning och könsbestämning

Dunlin (Calidris alpina )
Se även: Fågelskådning , Fågelringning , Markera och återfånga och Ornitologi

Per Martin-Löf började fågelskådning i sin ungdom och är fortfarande en entusiastisk fågelskådare. Som tonåring publicerade han en artikel om att uppskatta dödligheten hos fåglar, med hjälp av data från fågelringningar , i en svensk zoologisk tidskrift: Denna artikel citerades snart i ledande internationella tidskrifter, och denna artikel fortsätter att citeras.

Inom fåglarnas biologi och statistik finns det flera problem med att data saknas . Martin-Löfs första artikel diskuterade problemet med att uppskatta dödligheten för Dunlin -arterna med metoder för fångst-återfångst . Problemet med att bestämma det biologiska könet på en fågel, som är extremt svårt för människor, är ett av de första exemplen i Martin-Löfs föreläsningar om statistiska modeller .

Sannolikhet på algebraiska strukturer

Se även: sannolikhetsfördelning , övertonsanalys , Haarmått , Laplacetransform och semigroup

Martin-Löf skrev en licensuppsats om sannolikhet för algebraiska strukturer, särskilt semigrupper, medan han studerade till Ulf Grenander vid Stockholms universitet.

Statistiska modeller

Se även: Exponentiell familj och statistisk modell

Martin-Löf utvecklade innovativa metoder för statistisk teori . I sin artikel "On Tables of Random Numbers" Kolmogorov att frekvenssannolikhetsuppfattningen om de begränsande egenskaperna hos oändliga sekvenser misslyckades med att ge en grund för statistik, som endast beaktar ändliga prover. Mycket av Martin-Löfs arbete inom statistik var att tillhandahålla ett ändligt urvalsunderlag för statistik.

Modellval och hypotesprövning

Stegen för EM-algoritmen på en tvåkomponents Gaussisk blandningsmodell på Old Faithful- datauppsättningen
Se även: Modellval , Tillräcklig statistik , hypotestest och Exakt test

På 1970-talet gjorde Per Martin-Löf viktiga bidrag till statistisk teori och inspirerade till vidare forskning, särskilt av skandinaviska statistiker inklusive Rolf Sundberg, Thomas Höglund och Steffan Lauritzen. I detta arbete ledde Martin-Löfs tidigare forskning om sannolikhetsmått på semigrupper till en föreställning om "repetitiv struktur" och en ny behandling av tillräcklig statistik, där enparameters exponentiella familjer karakteriserades . Han tillhandahöll ett kategoriteoretiskt tillvägagångssätt för kapslade statistiska modeller , med hjälp av principer med ändliga urval. Före (och efter) Martin-Löf har sådana kapslade modeller ofta testats med hjälp av chi-kvadrathypotestest, vars motiveringar bara är asymptotiska (och så irrelevanta för verkliga problem, som alltid har finita stickprov).

Förväntningsmaximeringsmetod för exponentiella familjer

Se även: Saknade data och Förväntningsmaximeringsmetod

Martin-Löfs student, Rolf Sundberg, utvecklade en detaljerad analys av förväntningsmaximeringsmetoden ( EM) för skattning med hjälp av data från exponentiella familjer, speciellt med saknade data . Sundberg tillskriver en formel, senare kallad Sundbergsformeln, till tidigare manuskript av bröderna Martin-Löf, Per och Anders . Många av dessa resultat nådde det internationella forskarsamhället genom 1976 års artikel om förväntningsmaximeringsmetoden ( EM) av Arthur P. Dempster , Nan Laird och Donald Rubin , som publicerades i en ledande internationell tidskrift, sponsrad av Royal Statistical Society .

Logik

Franz Brentano

Filosofisk logik

Se även: Logisk konsekvens , Entailment , Analytisk filosofi , Kontinentalfilosofi , Intuitionism och Fenomenologi (filosofi)

Inom filosofisk logik har Per Martin-Löf publicerat artiklar om teorin om logisk konsekvens , om bedömningar etc. Han har intresserat sig för centraleuropeiska filosofiska traditioner, särskilt av de tyskspråkiga skrifterna av Franz Brentano , Gottlob Frege och Edmund Husserl .

Typteori

Huvudartikel: Typteori
Se även: Intuitionistisk typteori , Bevisteoretisk semantik och Beroende typ

Martin-Löf har arbetat med matematisk logik i många decennier.

Från 1968 till '69 arbetade han som biträdande professor vid University of Chicago där han träffade William Alvin Howard med vilken han diskuterade frågor relaterade till Curry-Howard-korrespondensen . Martin-Löfs första utkast till artikel om typteori går tillbaka till 1971. Denna impredikativa teori generaliserade Girards System F . Detta system visade sig dock vara inkonsekvent på grund av Girards paradox som upptäcktes av Girard när han studerade System U, en inkonsekvent förlängning av System F. Denna erfarenhet ledde till att Per Martin-Löf utvecklade de filosofiska grunderna för typteorin , hans meningsförklaring , en form av bevisteoretisk semantik , som motiverar predikativ typteori som presenteras i hans Bibliopolis-bok från 1984, och utvidgas i ett antal alltmer filosofiska texter, såsom hans inflytelserika On the Meanings of the Logical Constants and the Justifications of the Logical Laws .

Typteorin från 1984 var extensionell medan typteorin som presenterades i boken av Nordström et al. 1990, som var starkt influerad av hans senare idéer, intensivt och mer mottagligt för att implementeras på en dator.

Martin-Löfs intuitionistiska typteori utvecklade föreställningen om beroende typer och påverkade direkt utvecklingen av konstruktionskalkylen och det logiska ramverket LF . Ett antal populära datorbaserade bevissystem är baserade på typteori, till exempel NuPRL , LEGO, Coq , ALF, Agda , Twelf , Epigram och Idris .

Utmärkelser

Martin-Löf är ledamot av Kungliga Vetenskapsakademien och i Academia Europaea .

Se även

Anteckningar

Fågelskådning och saknade data

  • Martin-Löf, P. (1961). "Dödlighetsberäkningar på ringmärkta fåglar med särskild hänvisning till Dunlin Calidris alpina ". Arkiv för Zoologi (Zoology Files), Kungliga Svenska Vetenskapsakademien (Kungliga Vetenskapsakademien) Serie 2 . Band 13 (21).

Sannolikhetsgrunder

  • Per Martin-Löf. "Definitionen av slumpmässiga sekvenser." Information and Control , 9(6): 602–619, 1966.
  • Li, Ming och Vitányi, Paul, An Introduction to Kolmogorov Complexity and Its Applications , Springer, 1997. Introduktionskapitlet i fulltext .

Sannolikhet på algebraiska strukturer, efter Ulf Grenander

  • Grenander, Ulf . Sannolikhet på algebraiska strukturer . (Dover reprint)
  • Martin-Löf, P. Kontinuitetssatsen om en lokalt kompakt grupp. Teor. Verojatnost. i Primenen. 10 1965 367–371.
  • Martin-Löf, Per. Sannolikhetsteori om diskreta semigrupper. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 4 1965 78—102
  • Nitis Mukhopadhyay. "Ett samtal med Ulf Grenander". Statistik. Sci. Volym 21, nummer 3 (2006), 404–426.

Statistikstiftelser

  • Anders Martin-Löf . 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Evaluation of lifetimes in time-lengths below one nanosecond"). ("Sundbergs formel", enligt Sundberg 1971)
  • Per Martin-Löf. 1966. Statistik ur statistisk mekaniks synvinkel . Föreläsningsanteckningar, Mathematical Institute, Aarhus Universitet. ("Sundbergs formel" tillskrivs Anders Martin-Löf, enligt Sundberg 1971)
  • Per Martin-Löf. 1970. Statistika Modeller (Statistiska modeller): Anteckningar fran seminarier läsåret 1969–1970 (Anteckningar från seminarier läsåret 1969–1970), med hjälp av Rolf Sundberg. Stockholms universitet.
  • Martin-Löf, P. "Exakta tester, konfidensregioner och uppskattningar", med en diskussion av AWF Edwards , GA Barnard , DA Sprott, O. Barndorff-Nielsen, D. Basu och G. Rasch . Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), s. 121–138. Memoarer, nr 1, Avd. Teoret. Statist., Inst. Math., Univ. Århus, Århus, 1974.
  • Martin-Löf, P. Repetitiva strukturer och sambandet mellan kanoniska och mikrokanoniska fördelningar i statistik och statistisk mekanik. Med en diskussion av DR Cox och G. Rasch och ett svar av författaren. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), s. 271–294. Memoarer, nr 1, Avd. Teoret. Statist., Inst. Math., Univ. Århus, Århus, 1974.
  • Martin-Löf, P. Begreppet redundans och dess användning som ett kvantitativt mått på avvikelsen mellan en statistisk hypotes och en uppsättning observationsdata. Med en diskussion av F. Abildgård, AP Dempster , D. Basu , DR Cox , AWF Edwards , DA Sprott, GA Barnard , O. Barndorff-Nielsen, JD Kalbfleisch och G. Rasch och ett svar av författaren. Proceedings of Conference on Foundational Questions in Statistical Inference (Aarhus, 1973), s. 1–42. Memoarer, nr 1, Avd. Teoret. Statist., Inst. Math., Univ. Århus, Århus, 1974.
  • Martin-Löf, Per Begreppet redundans och dess användning som ett kvantitativt mått på diskrepansen mellan en statistisk hypotes och en uppsättning observationsdata. Scand. J. Statist. 1 (1974), nr. 1, 3—18.
  • Sverdrup, Erling. "Tester utan ström." Scand. J. Statist. 2 (1975), nr. 3, 158-160.
  • Martin-Löf, Per Svar på Erling Sverdrups polemiska artikel: ``Tester utan kraft ( Scand. J. Statist. 2 (1975), nr 3, 158–160). Scand. J. Statist. 2 (1975), nr. 3, 161-165.
  • Sverdrup, Erling. En replik till: ``Tester utan makt ( Scand. J. Statist. 2 (1975), 161—165) av P. Martin-Löf. Scand. J. Statist. 4 (1977), nr. 3, 136—138.
  • Martin-Löf, P. Exakta tester, konfidensregioner och uppskattningar. Grunder för sannolikhet och statistik. II. Synthese 36 (1977), nr. 2, 195—206.
  • Rolf Sundberg. 1971. Maximal likelihood-teori och tillämpningar för distributioner som genereras när en funktion av en exponentiell familjevariabel observeras . Avhandling, Institutet för matematisk statistik, Stockholms universitet.
  • Sundberg, Rolf. Maximal likelihood-teori för ofullständiga data från en exponentiell familj. Scand. J. Statist. 1 (1974), nr. 2, 49—58.
  • Sundberg, Rolf En iterativ metod för lösning av likelihood-ekvationerna för ofullständiga data från exponentialfamiljer. Comm. Statist.—Simulation Comput. B5 (1976), nr. 1, 55—64.
  • Sundberg, Rolf Några resultat om nedbrytbara (eller Markov-typ) modeller för flerdimensionella beredskapstabeller: fördelning av marginaler och uppdelning av tester. Scand. J. Statist. 2 (1975), nr. 2, 71—79.
  • Höglund, Thomas. Den exakta uppskattningen — en metod för statistisk uppskattning. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 29 (1974), 257—271.
  •   Lauritzen, Steffen L. Extremala familjer och system med tillräcklig statistik . Lecture Notes in Statistics, 49. Springer-Verlag, New York, 1988. xvi+268 s. ISBN 0-387-96872-5

Grunderna för matematik, logik och datavetenskap

externa länkar

Hämtad från " https://sv.wikipedia.org/w/index.php?title=Per_Martin-Löf&oldid=1133260167 "