ペール・マルティン＝レーフ

ペール・エリック・ルトガー・マルティン=レーフ（Per Erik Rutger Martin-Löf（; Does HoTT Provide a Foundation for Mathematics? by James Ladyman (University of Bristol, UK) ; Peter Dybjer on types and testing – The Type Theory Podcast）, 1942年5月8日 - ） は、スウェーデンの論理学者・哲学者・数理統計学者。 確率、統計学、数理論理学、および計算機科学の基礎に関する研究で世界的に知られる。1970年代後半以降は、マルティン=レーフの出版物は論理学に属するものが主なものとなった。

人物 哲学的論理学の分野では、ブレンターノ、フレーゲ、及びフッサールの仕事に部分的に惹起された論理的帰結（logical consequence）と判断（judgement）の哲学に取り組んだ。マルティン＝レーフは、現代論理学における直観主義の領導者であり、構成的数学の基礎として導入した直観主義型理論はその代表作である p.716。型理論に関するマルティン=レーフの仕事は計算機科学に大きな影響を与えることとなったSee e.g. .。

2009年に引退するまでPhilosophy and Foundations of Mathematics: Epistemological and Ontological Aspects. A conference dedicated to Per Martin-Löf on the occasion of his retirement . Swedish Collegium for Advanced Study, Uppsala, May 5–8, 2009. Retrieved 2014-01-26.、マルティン=レーフはストックホルム大学で数学と哲学の統合教授職（joint chair）にあったMember profile, Academia Europaea, retrieved 2014-01-26.。

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

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

マルティン＝レーフは、フレーゲ、フッサール、ラッセル、ウィトゲンシュタインに通暁した哲学者でもあり、彼の見解は、直観主義研究以外の場面でもきわめて大きな意義を持つ。マルティン＝レーフの業績は今なお論理学および理論計算機科学の研究にインスピレーションを与え続けており、彼のアイデアが持つ可能性はいまだに汲み尽くされていないといえる。

ランダムネスとコルモゴロフ複雑性

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

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

マルティン＝レーフ・ランダムネスは、元の定義とは外見上ほとんど類似していない多くの等価な特徴、すなわち、圧縮性、ランダム性検定、そして賭け事に関するもの、があることが示されている。しかし、それら特徴のそれぞれについて、ランダム列が持っているべき性質に対する直観的な感覚を満たしていなければならない。すなわち、ランダム列は非圧縮的であり、ランダム性に関する統計検定は通過するべきであるし、それで賭け事をしたとしてもお金を稼ぐことは不可能であるべきである。マルティン＝レーフ・ランダム性に複数の定義が存在することと、異なる計算モデルの下でのこれら定義の安定性は、マルティン＝レーフ・ランダムネスが数学の基本的な性質であり、マルティン＝レーフの特定のモデルによってもたらされた偶然ではないことの証拠となっている。マルティン＝レーフ・ランダムネスの定義が「正確に」ランダムネスの直観的概念を捉えているという提唱は、「マルティン＝レーフ・チャイティン提唱」と呼ばれている。これはチャーチ＝チューリングのテーゼに幾分か類似している提言であるJean-Paul Delahaye, Randomness, Unpredictability and Absence of Order, in Philosophy of Probability, p. 145–167, Springer 1993.。

マルティン＝レーフの研究の後、アルゴリズム情報理論は、ランダム文字列を、その文字列よりも短いプログラムからは生成できないものとして定義した（チャイティン＝コルモゴロフ複雑性）。すなわち、ある文字列のコルモゴロフ複雑性はその文字列の長さよりは小さいということである。これは統計学における用語の用法とは異なる意味である。統計学的ランダムネスは文字列を生成するプロセスを指す（たとえば、コインを投げて各ビットを生成するとランダム文字列が生成される）が、アルゴリズム的ランダムネスは文字列自体を指す。アルゴリズム情報理論は、用いられている計算モデルに対して比較的不変な方法で、ランダムでない文字列からランダムな文字列を分離する。

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

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

野鳥観察と性別決定

マルティン=レーフは若い頃に野鳥観察を始め、現在も続けている熱心な野鳥観察家であるGeorge A. Barnard, "Gone Birdwatching", New Scientist, 4 December 1999, magazine issue 2215.。１０代のころ、彼は、鳥類標識調査のデータをもとに鳥の死亡率を推定することに関する記事をスウェーデンの動物学雑誌に発表した。そして、この論文はすぐに国際的な雑誌に引用され、現在も継続して引用され続けている。

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

代数的構造の確率

マルティン=レーフは、ストックホルム大学におけるUlf Grenanderによって率いられる研究プログラムの対象である代数的構造、特に半群の中の確率論に関するライセンス論文を書いたMartin-Löf, P. The continuity theorem on a locally compact group. Teor. Verojatnost. i Primenen. 10 1965 367–371.Martin-Löf, Per Probability theory on discrete semigroups. Z. Wahrscheinlichkeitstheorie und Verw. Gebiete 4 1965 78–102Nitis Mukhopadhyay. A Conversation with Ulf Grenander. Statist. Sci. Volume 21, Number 3 (2006), 404–426.。

統計モデル

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

モデル選択と仮説検定

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

指数型分布族の期待値最大化法

マルティン=レーフの学生のロルフ・サンドバーグ（Rolf Sundberg）は、特に欠測データを伴う指数型分布族由来のデータを見積もるため、期待値最大化法であるEMアルゴリズムの詳細な分析法を開発した。 サンドバーグは、後にサンドバーグの公式として知られる一つの公式をマルティン=レーフ兄弟であるペールとアンダースによる昔の原稿に載せました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.Anders Martin-Löf. 1963. "Utvärdering av livslängder i subnanosekundsområdet" ("Evaluation of lifetimes in time-lengths below one nanosecond"). ("Sundberg formula")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).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. ("Sundberg formula")。 これら結果の多くは、1976年に王立統計学会が資本の有力国際雑誌に掲載されたアーサー・P・デンプスター（Arthur P. Dempster）、ナン・レアード（Nan Laird）、そしてドナルド・ルービン（Donald Rubin）による期待値最大化法（EMアルゴリズム）に関する論文を通じて国際科学界で知られることとなった。

論理学

哲学的論理学

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

型理論

マルティン＝レーフは数理論理学の分野で長年研究を行ってきた。1968年から69年まで、シカゴ大学にて准教授として働いた。彼はそこでウィリアム・アルヴィン・ハワード（William Alvin Howard）と出会い、カリー＝ハワード同型対応に関連する問題について議論し合った。マルティン＝レーフの最初の型理論に関する草稿が発表されたのは1971年にまで遡る。この非可述的な理論はジャン＝イヴ・ジラールのシステムFを一般化したものであった。しかしながら、このシステムはジラールのパラドックスによって矛盾していることがシステムUとシステムFの矛盾した拡張を研究しているジラールによって発見された。この経験はマルティン＝レーフに型理論の哲学的基盤を開発することに導いた。すなわち、意味説明、1984年のBibliopolisの本で提示された述語的型理論の正当化を行う証明論的意味論の形式、次第に哲学的となるテキストの数を増やしていった。そのようなテキストの中で影響を与えたものとしては「On the Meanings of the Logical Constants and the Justifications of the Logical Laws」がある。

1984年のの型理論は拡張であった一方でノードストロームらの1990年の本の中で型理論は紹介された。これはかれの後期のアイディアに大きく影響されたもので、内包的であり、コンピュータ上で実装することにより適したものであった。

マルティン＝レーフによる直観主義型理論は、依存型の概念を発展させ、構築計算と、論理的フレームワークのLFの開発に直接影響を与えた。多数の人気の計算機ベースの証明支援系が型理論に基づいている。例えば、NuPRL、LEGO、Coq、ALF、Agda、Twelf、Epigram、そしてIdrisなどである。

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

関連項目 アルゴリズム的ランダムな無限列 アルゴリズム情報理論 コルモゴロフ複雑性 マルティン=レーフ・チャイティンのテーゼ ホモトピー型理論

関連人物

フランツ・ブレンターノ ルドルフ・カルナップ マイケル・ダメット ゴットロープ・フレーゲ Ulf Grenander ヤーッコ・ヒンティッカ エトムント・フッサール アンドレイ・コルモゴロフ Anders Martin-Löf ジョン・フォン・ノイマン Peter Pagin ダグ・プラウィッツ チャールズ・サンダース・パース フランク・ラムジー バートランド・ラッセル デイナ・スコット アルフレッド・タルスキ アラン・チューリング グレゴリー・チャイティン ピーター・アクゼル ヨラン・スントホルム ジャン＝イヴ・ジラール

年表 1964年 - 1965年:モスクワのアンドレイ・コルモゴロフのもとで学び、ランダム系列に関する研究Per Martin-Löf, "The definition of random sequences," Information and Control, Vol.9, pp. 602-619, 1966.を行う。 1968年 - 1969年:シカゴ大学助教授を務め、ここでウィリアム・ハワードとカリー＝ハワード対応に関して議論している。 1971年: 型理論に関する最初の草稿を書き上げる。しかし、この最初の非可述体系はジャン＝イヴ・ジラールによって矛盾していることが示された（ジラールのパラドックス）。これをきっかけに型理論の概念的基礎の探求へと導かれていったマルティン＝レーフは、1984年の著作Per Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984 (ISBN 8870881059).で提示した可述型理論を正当化するための証明論的意味論を展開し、またこれに関連していくつかの哲学的著作Per Martin-Löf, "On the meanings of the logical constants and the justifications of the logical laws ", Atti degli Incontri di Logica Matematica, Vol.2, 1985, pp. 203-281; Reprinted in Nordic Journal of Philosophical Logic, Vol.1, 1996, pp. 11-60. Per Martin-Löf, "Analytic and synthetic judgements in type theory" in Paolo Parrini (ed.), Kant and Contemporary Epistemology, Kluwer, 1994, pp. 87-99 (ISBN 0792326814).も発表している。

脚注

参考文献 野鳥観察と欠測データ

確率論の基礎付け

Ulf Grenanderに始まる代数的構造の確率

統計学の基礎付け ("Sundberg formula", according to Sundberg 1971) ("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.

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. 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.

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: https://doi.org/10.15496/publikation-35319. University of Tübingen 2019.

その他

外部リンク