デイナ・スコット

提供: miniwiki
移動先:案内検索

デイナ・スチュアート・スコット (Dana Stewart Scott, 1932年- ) はアメリカの計算機科学者、数学者論理学者。数学的に難しい問題についての素養に基づき、非形式的だが厳格な方法で計算機科学・論理学・哲学にまたがる領域の根本的概念を明確化させてきた。オートマトン理論についての業績により1976年にチューリング賞を受賞。1970年代にはクリストファー・ストレイチーと共同でプログラム意味論への新たなアプローチを基礎付けた。様相論理位相幾何学圏論などでも業績を残している。

2012年現在は、カーネギーメロン大学計算機科学哲学数理論理学の名誉教授を務めている。事実上引退しており、カリフォルニア州バークレー在住。2005年に創刊した学術誌 Logical Methods in Computer Science の編集長を務めている。

学生時代まで

1954年カリフォルニア大学バークレー校にて学士号を取得。その後、同大学院でアルフレト・タルスキの指導を受けるが、タルスキとの間でトラブルが発生し、プリンストン大学へ移ることを余儀なくされる(ただしタルスキとはその後、和解している)。1958年、プリンストン大学にてアロンゾ・チャーチの指導のもと、Convergent Sequences of Complete Theories という論文を完成させ博士号を取得。ソロモン・フェファーマンは後にこのころについて次のように記している。

50年代前半、まだ学部学生のころスコットはバークレーで研究を開始した。ずば抜けた才能がすぐに認められ、大学院に進学して私やリチャード・モンタギューと共にタルスキの講座に属するようになった。だから私たちが友人になったのはそのころのことだ。スコットはタルスキの指導で博士号を目指していたが、私たちの伝記[1]に説明されている理由で落第することになった。動揺したスコットはプリンストンに移り、アロンゾ・チャーチの下で博士号を目指すことになった。しかしその後、タルスキが彼に「君を私の学生と呼びたい」と言い、彼らの関係が修復された。[2]

博士号を取得するとシカゴ大学に移り、1960年まで講師として勤務。1959年にはプリンストンでの同僚マイケル・ラビンと共同で Finite Automata and Their Decision Problem という論文を発表し、非決定性有限オートマトンのアイデアを明らかにした。これが計算複雑性理論の基礎概念となったことから、ラビンと共にチューリング賞を受賞した。

カリフォルニア大学バークレー校 1960–1963

彼の業績はオートマトン理論、公理的集合論プログラミング言語意味論言語哲学等、多岐にわたっており、1959年にマイケル・ラビンと共同で発表したオートマトン理論に関する研究 [1] により、1976年チューリング賞を受賞している。

カリフォルニア大学バークレー校で数学助教授の職を得てバークレーに戻ると、数理論理学の古典的問題、特に集合論とタルスキ的モデル理論の研究を行うようになった。

"Measurable cardinals and constructible sets" (1961) という論文[3]において、

可測基数が存在するならば、V≠L

を証明した。

このころから博士号を目指す学生を指導するようになる。このころの指導学生としては James Halpern や Edgar Lopez-Escobar がいる。

様相論理と時相論理

このころジョン・レモンと共同で様相論理の研究を始めている。レモンは1963年にカリフォルニア州クレアモントに移った。スコットは特にアーサー・プライアーEnglish版時相論理と自然言語の意味論における時間の扱い方との関係に興味を持ち、バークレーの学部学生だったころからの友人であるリチャード・モンタギューと共同研究を始めた[4]。後にスコットとモンタギューはそれぞれ独自にクリプキ意味論English版の様相論理および時相論理への重要な一般化を発見し、スコット-モンタギュー意味論English版と呼ばれるようになった[5]

レモンと共に様相論理の教科書を執筆していたが、1966年にレモンが亡くなったため中断した。スコットは未完成な論文を同僚らに回覧した。それはモデル理論の意味論の重要な技法をいくつか導入したもので、特にカノニカルモデルの改良と "filterations" を通してモデルを構築する重要な技法がある。それらは現代クリプキ意味論English版の中核概念となっている[6]。スコットは、最終的にレモンとの共著 An Introduction to Modal Logic を出版した[7]

スタンフォード、アムステルダム、プリンストン 1963–1972

ロバート・ソロヴェイEnglish版の初期の観測に続き、ソロヴェイやペトル・ヴォピェンカとほぼ同時期にスコットはブール値モデルEnglish版の概念を定式化した。1967年の論文 A Proof of the Independence of the Continuum Hypothesis で、ブール値モデルを使い、ポール・コーエン連続体仮説の独立性を証明したのとは別の証明を与えた。この業績により1972年にスティール賞を受賞している。

オックスフォード大学 1972–1981

1972年、オックスフォード大学哲学科の数理論理学教授の職を得た。

プログラミング言語の意味論

このころクリストファー・ストレイチーと共同研究しており、管理職としてのプレッシャーにも関わらず、プログラミング言語の意味論の数学的基盤を築く根本的な仕事をなしとげ、この業績でスコットは最もよく知られるようになった。全体として表示的意味論へのスコットとストレイチーのアプローチを構成している。それは理論計算機科学における最も有力な業績の1つであり、計算機科学の主要な学派の基盤となった見ることもできる。中でも領域理論の定式化への貢献が大きく[8]、再帰関数とループ制御構造を持つプログラミング言語の表示的意味論を与えることを可能にした。さらに、領域理論と彼の information system の理論を通して無限かつ連続な情報を理解する基盤を提供した。

この時期の業績から、以下のような賞を受賞している。

カーネギーメロン大学 1981–2003

カーネギー・メロン大学に移ると、領域理論の後継として equilogical spaces の理論を提唱。様々な長所があるが、特に equilogical spaces の圏はデカルト閉圏だが、領域の圏はそうではない。1994年、Association for Computing Machineryフェローに選ばれた。

主要著作

  • Michael Rabin and Dana Scott, "Finite automata and their decision problems," IBM Journal of Research and Development 3, 1959, pp. 114-125.
  • Scott, Dana (1961), “Measurable cardinals and constructible sets”, Bulletin de l'Académie Polonaise des Sciences, Série des Sciences Mathématiques, Astronomiques et Physiques 9: 521-524, http://www.worldscientific.com/doi/abs/10.1142/9789812564894_0020 
  • 1967. A proof of the independence of the continuum hypothesis. Mathematical Systems Theory 1:89–111.
  • Scott, Dana (1970), “Advice in modal logic”, in Lambert, K., Philosophical Problems in Logic, pp. 143–173 
  • Scott, Dana (1975), “Data types as lattices”, in G. Muller et al., Proceedings of the International Summer Institute and Logic Colloquium, Kiel, Lecture Notes in Mathematics, 499, Springer, pp. 579-651 
  • Scott, Dana; Lemmon, John (1977), An Introduction to Modal Logic, Oxford: Blackwell 

参考文献

脚注

外部リンク

テンプレート:Persondata

テンプレート:チューリング賞