利用者:I.hidekazu/ペール・マルティン＝レーフ

ペール・マルティン=レーフ（Per Martin-Löf）
Per Martin-Löf in 2004
生誕	(1942-05-08) 1942年5月8日（83歳） スウェーデンストックホルム[1]
市民権	スウェーデン
国籍	スウェーデン
研究分野	計算機科学 論理学 数理統計学 哲学
研究機関	ストックホルム大学 シカゴ大学 オーフス大学
出身校	ストックホルム大学
博士課程 指導教員	アンドレイ・コルモゴロフ
主な業績	ランダム列 Exact tests Repetitive structure Sufficient statistics Expectation maximization method 直観主義型理論
主な受賞歴	スウェーデン王立科学アカデミー ショック賞 (2020)
プロジェクト:人物伝
テンプレートを表示

ペール・エリック・ルトガー・マルティン=レーフ（Per Erik Rutger Martin-Löf）（[lɒf]; ^[2] スウェーデン語: [ ˈmǎʈːɪn ˈløːv ]; ^[3] は、スウェーデンの論理学者、哲学者、及び数理統計学者。 確率、統計学、数理論理学、および計算機科学の基礎に関する研究で世界的に知られる。1970年代後半以降は、マルティン=レーフの出版物は論理学に属するものが主なものとなった。

哲学的論理学の分野では、ブレンターノ、フレーゲ、及びフッサールの仕事に部分的に惹起された、論理的帰結（logical consequence）と判断（judgement）の哲学に取り組んだ。数理論理学の分野では、数学の構成的な基礎として直観主義型理論の開発に積極的に取り組んだ。型理論に関するマルティン=レーフの仕事は計算機科学に影響を与えることとなった^[4]。

2009年に引退するまで^[5]、マルティン=レーフはストックホルム大学で数学と哲学の共同議長を努めた。

彼の兄弟のアンダース・マルティン=レーフ（Anders Martin-Löf）は、ストックホルム大学の数理統計学の名誉教授である。かつて兄弟二人は協力して確率と統計の分野の研究を行なった。特に、指数型分布族、欠測データの期待値最大化法、およびモデル選択に関する統計理論に影響を与えた^[6]。

ペール・マルティン=レーフは熱心な野鳥観察家であり、彼の最初の科学に関する出版物は鳥類標識調査における死亡率に関するものであった^[7]。

1964年から1965年にかけて、マルティン=レーフはアンドレイ・コルモゴロフの指導の下モスクワに留学した。1966年に論文「ランダム列の定義（The definition of random sequences）」を書き、ランダム列の初めての適切な定義を与えた^[8]。

確率論の初期の研究者であるリヒャルト・フォン・ミーゼスなどは、全てのランダム性の検定に合格するランダム列を定義するためにランダム性検定の概念を定式化することを試みたが、結局それは曖昧なままであった。マルティン=レーフの鍵となる洞察は、ランダム性の検定の概念を形式的に定義するために計算理論を用いるということであった。これは、確率のランダム性の考え方とは対照的である。ただし、その理論の中では、標本空間の特定の元をランダムであると言うことはできない。

マルティン=レーフ・ランダムネスは、データ圧縮、ランダム性検定、ギャンブルの観点で、多く等価な特徴をもつことを認められているが、元の定義とは外見的にほとんど類似していないものの、それぞれがランダム列が満たすべき性質の直観的な概念を満たしている。すなわち、ランダム列は非圧縮性でなくてはならず、ランダム性の統計的検定に合格する必要があり、そして、それらに賭けてお金を稼ぐことは不可能である必要があった。マルティン=レーフ・ランダムネスのこれらの複数の定義の存在、および異なる計算モデルの下でのこれらの定義の安定性は、マルティン=レーフ・ランダムネスが数学の基本的な特性であり、マルティン=レーフの特定のモデルの偶然ではないことの証拠を与える。 マルティン=レーフ・ランダムネスの定義がランダム性の直感的な概念を「正しく」捉えているという論文は、「マルティン=レーフ-チャイティン論文」と呼ばれています。これは、チャーチ・チューリングの論文にいくらか類似している^[9]。

Martin-Löfの研究に続いて、アルゴリズム情報理論は、ランダムな文字列を、文字列よりも短いコンピュータプログラムから生成できないものとして定義しています（Chaitin–Kolmogorovのランダム性）。つまり、コルモゴロフの複雑さが少なくとも文字列の長さである文字列。これは、統計での用語の使用法とは異なる意味です。統計的ランダムネスは文字列を生成するプロセスを指しますが（たとえば、コインを投げて各ビットを生成するとランダムに文字列が生成されます）、アルゴリズム的ランダムネスは文字列自体を指します。アルゴリズム情報理論は、使用されている計算モデルに対して比較的不変な方法で、ランダムな文字列と非ランダムな文字列を分離します。

アルゴリズム的ランダムな無限列は文字の「無限」列であり、その全ての接頭部（おそらく有限の数を除いて）は、アルゴリズム的ランダムに極めて近い文字列である（その長さはコルモゴロフ複雑性の定数以下となる）。

Martin-Löf randomness has since been shown to admit many equivalent characterizations — in terms of compression, randomness tests, and gambling — that bear little outward resemblance to the original definition, but each of which satisfies our intuitive notion of properties that random sequences ought to have: random sequences should be incompressible, they should pass statistical tests for randomness, and it should be impossible to make money betting on them. The existence of these multiple definitions of Martin-Löf randomness, and the stability of these definitions under different models of computation, give evidence that Martin-Löf randomness is a fundamental property of mathematics and not an accident of Martin-Löf's particular model. The thesis that the definition of Martin-Löf randomness "correctly" captures the intuitive notion of randomness has been called the "Martin-Löf–Chaitin Thesis"; it is somewhat similar to the Church–Turing thesis.^[10]

Following Martin-Löf's work, algorithmic information theory defines a random string as one that cannot be produced from any computer program that is shorter than the string (Chaitin–Kolmogorov randomness); i.e. a string whose Kolmogorov complexity is at least the length of the string. This is a different meaning from the usage of the term in statistics. Whereas statistical randomness refers to the process that produces the string (e.g. flipping a coin to produce each bit will randomly produce a string), algorithmic randomness refers to the string itself. Algorithmic information theory separates random from nonrandom strings in a way that is relatively invariant to the model of computation being used.

An algorithmically random sequence is an infinite sequence of characters, all of whose prefixes (except possibly a finite number of exceptions) are strings that are "close to" algorithmically random (their length is within a constant of their Kolmogorov complexity).

マルティン=レーフは、確率論と統計学を（スウェーデンの伝統では）含む数理統計学の分野で重要な研究を行なってきた。

マルティン=レーフは若い頃に野鳥観察を始め、現在も続けている熱心な野鳥観察家です^[11]。１０代のころ、彼は、鳥類標識調査のデータをもとに鳥の死亡率を推定することに関する記事をスウェーデンの動物学雑誌に発表した。そして、この論文はすぐに国際的な雑誌に引用され、現在も継続して引用され続けている^[7][12]。

鳥に関する生物学と統計学の分野では、欠測データにまつわる幾つかの問題がある。マルティン=レーフの最初の論文では、捕獲再捕獲法のデータを用いて、ハマシギ種の死亡率の推定にまつわる問題について議論した。欠測データにまつわる第二の問題は鳥の性別の研究において発生した。鳥の生物学的性別を決定するという人間にとっては非常に難しい問題は、統計モデルに関するマルティン=レーフの講義において用いられる最初の例の一つである。

マルティン=レーフは、ストックホルム大学におけるen:Ulf_Grenanderによって率いられる研究プログラムの対象である代数的構造、特に半群の中の確率論に関するライセンス論文を書いた^[13][14][15]。

マルティン=レーフは、統計理論への革新的なアプローチを開発した。彼の論文「乱数表について（"On Tables of Random Numbers）」において、アンドレイ・コルモゴロフは、無限列の極限特性に関する頻度確率（frequency probability）概念は、ただ有限個の標本についてだけ考慮する統計学の基礎にはならないという意見を述べた^[16]。統計学におけるマルティン=レーフの仕事の多くは、有限標本ベースの統計学の基盤を提供している。

1970年代、マルティン=レーフは統計理論とそれに惹起された将来的な研究、特にロルフ サンドバーグ（en:Rolf Sundberg）、Thomas Höglund、そしてSteffan Lauritzenを含むスカンジナビアの統計学者によるもの、に重大な貢献をした。この仕事において、マルティン=レーフの半群を用いた確率測度に関する以前の研究により、「反復構造（repetitive structure）」と十分統計量の新しい取り扱い方が導かれ、それにより１径数指数型分布族が特徴付けられることとなった。彼はネストされた統計モデル（nested statistical model）に、有限標本の原理（finite-sample principle）を用いた上で、圏論的アプローチを提供した。マルティン=レーフ以前（そして以後も）、そのようなネスとされたモデルはカイ２乗仮説検定を用いることで検定されることが多く、その正当性は漸近的であるだけであった（かつ有限の標本を常に持つような実際の問題とは全く無関係であった）^[16]。

マルティン=レーフの学生のロルフ・サンドバーグ（Rolf Sundberg）は、特に欠測データを伴う指数型分布族由来のデータを見積もるため、期待値最大化法であるEMアルゴリズムの詳細な分析法を開発した。 サンドバーグは、後にサンドバーグの公式として知られる一つの公式をマルティン=レーフ兄弟であるペールとアンダースによる昔の原稿に載せました^{[17][18][19][20]}。 これら結果の多くは、1976年に王立統計学会が資本の有力国際雑誌に掲載されたアーサー・P・デンプスター（Arthur P.Dempster）、ナン・レアード（Nan Laird）、そしてドナルド・ルービン（Donald Rubin）による期待値最大化法（EMアルゴリズム）に関する論文を通じて国際科学界で知られることとなった^[21]。

Per Martin-Löf has done important research in mathematical statistics, which (in the Swedish tradition) includes probability theory and statistics.

Per Martin-Löf began bird watching in his youth and remains an enthusiastic bird-watcher.^[22] As a teenager, he published an article on estimating the mortality rates of birds, using data from bird ringing, in a Swedish zoological journal: This paper was soon cited in leading international journals, and this paper continues to be cited.^[7][23]

In the biology and statistics of birds, there are several problems of missing data. Martin-Löf's first paper discussed the problem of estimating the mortality rates of the Dunlin species, using capture-recapture methods. A second problem of missing data arises with studying the sex of birds. The problem of determining the biological sex of a bird, which is extremely difficult for humans, is one of the first examples in Martin-Löf's lectures on statistical models.

Martin-Löf wrote a licenciate thesis on probability on algebraic structures, particularly semigroups, a research program led by Ulf Grenander at Stockholm University.^[24][25][26]

Martin-Löf developed innovative approaches to statistical theory. In his paper "On Tables of Random Numbers", Kolmogorov observed that the frequency probability notion of the limiting properties of infinite sequences failed to provide a foundation for statistics, which considers only finite samples.^[16] Much of Martin-Löf's work in statistics was to provide a finite-sample foundation for statistics.

In the 1970s, Per Martin-Löf made important contributions to statistical theory and inspired further research, especially by Scandinavian statisticians including Rolf Sundberg, Thomas Höglund, and Steffan Lauritzen. In this work, Martin-Löf's previous research on probability measures on semigroups led to a notion of "repetitive structure" and a novel treatment of sufficient statistics, in which one-parameter exponential families were characterized. He provided a category-theoretic approach to nested statistical models, using finite-sample principles. Before (and after) Martin-Löf, such nested models have often been tested using chi-square hypothesis tests, whose justifications are only asymptotic (and so irrelevant to real problems, which always have finite samples).^[16]

Martin-Löf's student, Rolf Sundberg, developed a detailed analysis of the expectation-maximization (EM) method for estimation using data from exponential families, especially with missing data. Sundberg credits a formula, later known as the Sundberg formula, to previous manuscripts of the Martin-Löf brothers, Per and Anders.^{[27][28][29][30]} Many of these results reached the international scientific community through the 1976 paper on the expectation maximization (EM) method by Arthur P. Dempster, Nan Laird, and Donald Rubin, which was published in a leading international journal, sponsored by the Royal Statistical Society.^[31]

哲学的論理学の分野においては、マルティン=レーフは論理的帰結、判断の理論などについての論文を発表している。彼は中央ヨーロッパの哲学的伝統、特にドイツ語圏の書き物、フランツ・ブレンターノ、ゴットロープ・フレーゲ、そしてエトムント・フッサールに強い関心を抱き続けている。

Martin-Löf has worked in mathematical logic for many decades.

From 1968 to '69 he worked as an Assistant Professor at the University of Chicago where he met William Alvin Howard with whom he discussed issues related to the Curry–Howard correspondence. Martin-Löf's first draft article on type theory dates back to 1971. This impredicative theory generalized Girard's System F. However, this system turned out to be inconsistent due to Girard's paradox which was discovered by Girard when studying System U, an inconsistent extension of System F. This experience led Per Martin-Löf to develop the philosophical foundations of type theory, his meaning explanation, a form of proof-theoretic semantics, which justifies predicative type theory as presented in his 1984 Bibliopolis book, and extended in a number of increasingly philosophical texts, such as his influential On the Meanings of the Logical Constants and the Justifications of the Logical Laws.

The 1984 type theory was extensional while the type theory presented in the book by Nordström et al. in 1990, which was heavily influenced by his later ideas, intensional, and more amenable to being implemented on a computer.

Martin-Löf's intuitionistic type theory developed the notion of dependent types and directly influenced the development of the calculus of constructions and the logical framework LF. A number of popular computer-based proof systems are based on type theory, for example NuPRL, LEGO, Coq, ALF, Agda, Twelf, Epigram, and Idris.

• スウェーデン王立科学アカデミー会員^[32]
• ヨーロッパ・アカデミー（Academia Europaea）会員^[33]
• 2020年:ショック賞論理学・哲学部門受賞（ダグ・プラウィッツと同時受賞）。

• Per Martin-Löf (1961). “Mortality rate calculations on ringed birds with special reference to the Dunlin Calidris alpina”. Arkiv för Zoologi (Zoology Files), Kungliga Svenska Vetenskapsakademien (The Royal Swedish Academy of Sciences) Serie 2 Band 13 (21). 
• George A. Barnard (4 December 1999), “Gone Birdwatching”, New Scientist (magazine issue 2215), https://www.newscientist.com/article/mg16422156.600-gone-birdwatching.html 
• Seber, G.A.F. (2002). The Estimation of Animal Abundance and Related Parameters. Caldwel, New Jersey: Blackburn Press. ISBN 1-930665-55-5 
• Royle, J. A.; R. M. Dorazio (2008). Hierarchical Modeling and Inference in Ecology. Elsevier. ISBN 978-1-930665-55-2 

• Per Martin-Löf (1966), “The Definition of Random Sequences”, Information and Control (9(6)): 602–619 
• Li, Ming and Vitányi, Paul (1997). An Introduction to Kolmogorov Complexity and Its Applications. Springer 

• Ulf Grenander. Probability on Algebraic Structures. Dover reprint 
• Per Martin-Löf (1965), “The continuity theorem on a locally compact group”, Teor. Verojatnost. i Primenen (10): 367–371 
• Per Martin-Löf (1965), “Probability theory on discrete semigroups”, Z. Wahrscheinlichkeitstheorie und Verw. Gebiete (4): 78-102 
• Nitis Mukhopadhyay (2006), “A Conversation with Ulf Grenander”, Statist. Sci 21 (Number 3): 404–426 

• Anders Martin-Löf (1963), Utvärdering av livslängder i subnanosekundsområdet ("Evaluation of lifetimes in time-lengths below one nanosecond")  ("Sundberg formula", according to Sundberg 1971)
• Per Martin-Löf (1966), “Statistics from the point of view of statistical mechanics”, Lecture notes, Mathematical Institute, Aarhus University  ("Sundberg formula" credited to Anders Martin-Löf, according to Sundberg 1971)
• Per Martin-Löf. 1970. Statistika Modeller (Statistical Models): Anteckningar fran seminarier läsåret 1969–1970 (Notes from seminars in the academic year 1969–1970), with the assistance of Rolf Sundberg. Stockholm University.
• Martin-Löf, P. "Exact tests, confidence regions and estimates", with a discussion by A. W. F. Edwards, G. A. Barnard, D. A. Sprott, O. Barndorff-Nielsen, D. Basu and 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. Repetitive structures and the relation between canonical and microcanonical distributions in statistics and statistical mechanics. With a discussion by D. R. Cox and G. Rasch and a reply by the author. 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. The notion of redundancy and its use as a quantitative measure of the deviation between a statistical hypothesis and a set of observational data. With a discussion by F. Abildgård, A. P. Dempster, D. Basu, D. R. Cox, A. W. F. Edwards, D. A. Sprott, George A. Barnard, O. Barndorff-Nielsen, J. D. Kalbfleisch and G. Rasch and a reply by the author. 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.
• Per Martin-Löf (1974), “The notion of redundancy and its use as a quantitative measure of the discrepancy between a statistical hypothesis and a set of observational data”, Scand. J. Statist. 1 1: 3-18 
• Sverdrup, Erling (1975), “Tests without power”, Scand. J. Statist. 2 3: 158–160 
• Martin-Löf, Per Reply to Erling Sverdrup's polemical article: ``Tests without power (Scand. J. Statist. 2 (1975), no. 3, 158–160). Scand. J. Statist. 2 (1975), no. 3, 161–165.
• Sverdrup, Erling. A rejoinder to: ``Tests without power (Scand. J. Statist. 2 (1975), 161—165) by P. Martin-Löf. Scand. J. Statist. 4 (1977), no. 3, 136—138.
• Per Martin-Löf (1977), “Exact tests, confidence regions and estimates. Foundations of probability and statistics. II”, Synthese 36 (no. 2): 195-206 
• Rolf Sundberg (1971), “Maximum likelihood theory and applications for distributions generated when observing a function of an exponential family variable”, Dissertation, Institute for Mathematical Statistics (Stockholm University) 
• Rolf Sundberg (1974), “Maximum likelihood theory for incomplete data from an exponential family”, Scand. J. Statist 1 (no.2): 49-58 
• Rolf Sundberg (1976), “An iterative method for solution of the likelihood equations for incomplete data from exponential families”, Comm. Statist.—Simulation Comput. B5 (no.1): 55—64 
• Rolf Sundberg (1975), “Some results about decomposable (or Markov-type) models for multidimensional contingency tables: distribution of marginals and partitioning of tests”, Scand. J. Statist 2 (no. 2): 71—79 
• Thomas Höglund (1974), “The exact estimate — a method of statistical estimation”, Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 29: 257—271 
• Steffen L. Lauritzen (1988), “Extremal families and systems of sufficient statistics”, Lecture Notes in Statistics (Springer-Verlag, New York) 49: xvi+268 pp, ISBN 0-387-96872-5 

• Per Martin-Löf. A theory of types. Preprint, Stockholm University, 1971.
• Per Martin-Löf. An intuitionistic theory of types. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998. Reprinted version of an unpublished report from 1972.
• Per Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium ‘73, pages 73–118. North Holland, 1975.
• Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science VI, 1979. Eds. Cohen, et al. North-Holland, Amsterdam. pp. 153–175, 1982.
• Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984.
• Per Martin-Löf. Philosophical implications of type theory, Unpublished notes, 1987?
• Per Martin-Löf. Substitution calculus, 1992. Notes from a lecture given in Göteborg.
• Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990. (The book is out of print, but a free version has been made available.)
• Per Martin-Löf. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic, 1(1): 11–60, 1996.
• Per Martin-Löf. Logic and Ethics. 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.

• I.hidekazu/ペール・マルティン＝レーフ - Mathematics Genealogy Project