トップQs
タイムライン
チャット
視点
ペール・マルティン＝レーフ
ウィキペディアから
Remove ads
ペール・エリック・ルトガー・マルティン=レーフ（Per Erik Rutger Martin-Löf（[lɒf]; [2] スウェーデン語: [ ˈmǎʈːɪn ˈløːv ]; [3]）, 1942年5月8日 - ） は、スウェーデンの論理学者・哲学者・数理統計学者。 確率、統計学、数理論理学、および計算機科学の基礎に関する研究で世界的に知られる。1970年代後半以降は、マルティン=レーフの出版物は論理学に属するものが主なものとなった。
Remove ads
人物
哲学的論理学の分野では、ブレンターノ、フレーゲ、及びフッサールの仕事に部分的に惹起された論理的帰結（logical consequence）と判断（judgement）の哲学に取り組んだ。マルティン＝レーフは、現代論理学における直観主義の領導者であり、構成的数学の基礎として導入した直観主義型理論はその代表作である[4]。型理論に関するマルティン=レーフの仕事は計算機科学に大きな影響を与えることとなった[5]。
2009年に引退するまで[6]、マルティン=レーフはストックホルム大学で数学と哲学の統合教授職（joint chair）にあった[7]。
彼の兄弟のアンダース・マルティン=レーフ（Anders Martin-Löf）は、ストックホルム大学の数理統計学の名誉教授である。かつて兄弟二人は協力して確率と統計の分野の研究を行なった。特に、指数型分布族、欠測データの期待値最大化法、およびモデル選択に関する統計理論に影響を与えた[8]。
ペール・マルティン=レーフは熱心な野鳥観察家であり、彼の最初の科学に関する出版物は鳥類標識調査における死亡率に関するものであった[9]。
マルティン＝レーフは、フレーゲ、フッサール、ラッセル、ウィトゲンシュタインに通暁した哲学者でもあり、彼の見解は、直観主義研究以外の場面でもきわめて大きな意義を持つ[4]。マルティン＝レーフの業績は今なお論理学および理論計算機科学の研究にインスピレーションを与え続けており、彼のアイデアが持つ可能性はいまだに汲み尽くされていないといえる。
Remove ads
ランダムネスとコルモゴロフ複雑性
要約
視点
→詳細は「アルゴリズム的ランダムな無限列」を参照
→「コルモゴロフ複雑性」および「アルゴリズム情報理論」を参照
1964年から1965年にかけて、マルティン=レーフはアンドレイ・コルモゴロフの指導の下モスクワに留学した。1966年に論文「ランダム列の定義（The definition of random sequences）」を書き、ランダム列の初めての適切な定義を与えた[10]。
確率論の初期の研究者であるリヒャルト・フォン・ミーゼスなどは、全てのランダム性の検定に合格するランダム列を定義するためにランダム性検定の概念を定式化することを試みたが、結局それは曖昧なままであった。マルティン=レーフの鍵となる洞察は、ランダム性の検定の概念を形式的に定義するために計算理論を用いるということであった。これは、確率のランダム性の考え方とは対照的である。ただし、その理論の中では、標本空間の特定の元をランダムであると言うことはできない。
マルティン＝レーフ・ランダムネスは、元の定義とは外見上ほとんど類似していない多くの等価な特徴、すなわち、圧縮性、ランダム性検定、そして賭け事に関するもの、があることが示されている。しかし、それら特徴のそれぞれについて、ランダム列が持っているべき性質に対する直観的な感覚を満たしていなければならない。すなわち、ランダム列は非圧縮的であり、ランダム性に関する統計検定は通過するべきであるし、それで賭け事をしたとしてもお金を稼ぐことは不可能であるべきである。マルティン＝レーフ・ランダム性に複数の定義が存在することと、異なる計算モデルの下でのこれら定義の安定性は、マルティン＝レーフ・ランダムネスが数学の基本的な性質であり、マルティン＝レーフの特定のモデルによってもたらされた偶然ではないことの証拠となっている。マルティン＝レーフ・ランダムネスの定義が「正確に」ランダムネスの直観的概念を捉えているという提唱は、「マルティン＝レーフ・チャイティン提唱」と呼ばれている。これはチャーチ＝チューリングのテーゼに幾分か類似している提言である[11]。
マルティン＝レーフの研究の後、アルゴリズム情報理論は、ランダム文字列を、その文字列よりも短いプログラムからは生成できないものとして定義した（チャイティン＝コルモゴロフ複雑性）。すなわち、ある文字列のコルモゴロフ複雑性はその文字列の長さよりは小さいということである。これは統計学における用語の用法とは異なる意味である。統計学的ランダムネスは文字列を生成するプロセスを指す（たとえば、コインを投げて各ビットを生成するとランダム文字列が生成される）が、アルゴリズム的ランダムネスは文字列自体を指す。アルゴリズム情報理論は、用いられている計算モデルに対して比較的不変な方法で、ランダムでない文字列からランダムな文字列を分離する。
アルゴリズム的ランダムな無限列は文字の「無限」列であり、その全ての接頭部（おそらく有限の数を除いて）は、アルゴリズム的ランダムに極めて近い文字列である（その長さはコルモゴロフ複雑性の定数以下となる）。
Remove ads
数理統計学
要約
視点
マルティン=レーフは、確率論と統計学を（スウェーデンの伝統では）含む数理統計学（mathmatical statistics）の分野で重要な研究を行なってきた。
野鳥観察と性別決定
マルティン=レーフは若い頃に野鳥観察を始め、現在も続けている熱心な野鳥観察家である[12]。１０代のころ、彼は、鳥類標識調査のデータをもとに鳥の死亡率を推定することに関する記事をスウェーデンの動物学雑誌に発表した。そして、この論文はすぐに国際的な雑誌に引用され、現在も継続して引用され続けている[9][13]。
鳥に関する生物学と統計学の分野では、欠測データにまつわる幾つかの問題がある。マルティン=レーフの最初の論文では、捕獲再捕獲法のデータを用いて、ハマシギ種の死亡率の推定にまつわる問題について議論した。欠測データにまつわる第二の問題は鳥の性別の研究において発生した。鳥の生物学的性別を決定するという人間にとっては非常に難しい問題は、統計モデルに関するマルティン=レーフの講義において用いられる最初の例の一つである。
代数的構造の確率
マルティン=レーフは、ストックホルム大学におけるUlf Grenanderによって率いられる研究プログラムの対象である代数的構造、特に半群の中の確率論に関するライセンス論文を書いた[14][15][16]。
統計モデル
マルティン=レーフは、統計理論への革新的なアプローチを開発した。彼の論文「乱数表について（"On Tables of Random Numbers）」において、アンドレイ・コルモゴロフは、無限列の極限特性に関する頻度確率（frequency probability）概念は、ただ有限個の標本についてだけ考慮する統計学の基礎にはならないという意見を述べた[17]。統計学におけるマルティン=レーフの仕事の多くは、有限標本ベースの統計学の基盤を提供している。
モデル選択と仮説検定
1970年代、マルティン=レーフは統計理論とそれに惹起された将来的な研究、特にロルフ サンドバーグ（Rolf Sundberg）、Thomas Höglund、そしてSteffan Lauritzenを含むスカンジナビアの統計学者によるもの、に重大な貢献をした。この仕事において、マルティン=レーフの半群を用いた確率測度に関する以前の研究により、「反復構造（repetitive structure）」と十分統計量の新しい取り扱い方が導かれ、それにより１径数指数型分布族が特徴付けられることとなった。彼はネストされた統計モデル（nested statistical model）に、有限標本の原理（finite-sample principle）を用いた上で、圏論的アプローチを提供した。マルティン=レーフ以前（そして以後も）、そのようなネスとされたモデルはカイ２乗仮説検定を用いることで検定されることが多く、その正当性は漸近的であるだけであった（かつ有限の標本を常に持つような実際の問題とは全く無関係であった）[17]。
指数型分布族の期待値最大化法
マルティン=レーフの学生のロルフ・サンドバーグ（Rolf Sundberg）は、特に欠測データを伴う指数型分布族由来のデータを見積もるため、期待値最大化法であるEMアルゴリズムの詳細な分析法を開発した。 サンドバーグは、後にサンドバーグの公式として知られる一つの公式をマルティン=レーフ兄弟であるペールとアンダースによる昔の原稿に載せました[18][19][20][21]。 これら結果の多くは、1976年に王立統計学会が資本の有力国際雑誌に掲載されたアーサー・P・デンプスター（Arthur P. Dempster）、ナン・レアード（Nan Laird）、そしてドナルド・ルービン（Donald Rubin）による期待値最大化法（EMアルゴリズム）に関する論文を通じて国際科学界で知られることとなった[22]。
論理学
哲学的論理学
哲学的論理学の分野においては、マルティン=レーフは論理的帰結、判断の理論などについての論文を発表している。彼は中央ヨーロッパの哲学的伝統、特にドイツ語圏の書き物、フランツ・ブレンターノ、ゴットロープ・フレーゲ、そしてエトムント・フッサールに強い関心を抱き続けている。
型理論
→詳細は「型理論」を参照
マルティン＝レーフは数理論理学の分野で長年研究を行ってきた。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などである。
Remove ads
受賞歴
- 1989年:ヨーロッパ・アカデミー（Academia Europaea）会員[7]
- 1990年:スウェーデン王立科学アカデミー会員[23]
- 2020年:ショック賞論理学・哲学部門受賞（ダグ・プラウィッツと同時受賞）
関連項目
- アルゴリズム的ランダムな無限列
- アルゴリズム情報理論
- コルモゴロフ複雑性
- マルティン=レーフ・チャイティンのテーゼ
- ホモトピー型理論
関連人物
年表
- 1964年 - 1965年:モスクワのアンドレイ・コルモゴロフのもとで学び、ランダム系列に関する研究[24]を行う。
- 1968年 - 1969年:シカゴ大学助教授を務め、ここでウィリアム・ハワードとカリー＝ハワード対応に関して議論している。
- 1971年: 型理論に関する最初の草稿を書き上げる。しかし、この最初の非可述体系はジャン＝イヴ・ジラールによって矛盾していることが示された（ジラールのパラドックス）。これをきっかけに型理論の概念的基礎の探求へと導かれていったマルティン＝レーフは、1984年の著作[25]で提示した可述型理論を正当化するための証明論的意味論を展開し、またこれに関連していくつかの哲学的著作[26][27]も発表している。
脚注
参考文献
外部リンク
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads