デイナ・スチュアート・スコット (英語:Dana Stewart Scott、1932年10月11日 - )はアメリカの計算機科学者、数学者、論理学者。数学的に難しい問題についての素養に基づき、非形式的だが厳格な方法で計算機科学・論理学・哲学にまたがる領域の根本的概念を明確化させてきた。オートマトン理論についての業績により1976年にチューリング賞を受賞。1970年代にはクリストファー・ストレイチーと共同でプログラム意味論への新たなアプローチを基礎付けた。様相論理、位相幾何学、圏論などでも業績を残している。
2012年現在は、カーネギーメロン大学で計算機科学と哲学と数理論理学の名誉教授を務めている。事実上引退しており、カリフォルニア州バークレー在住。2005年に創刊した学術誌 Logical Methods in Computer Science の編集長を務めている。
学生時代まで 1954年、カリフォルニア大学バークレー校にて学士号を取得。その後、同大学院でアルフレト・タルスキの指導を受けるが、タルスキとの間でトラブルが発生し、プリンストン大学へ移ることを余儀なくされる（ただしタルスキとはその後、和解している）。1958年、プリンストン大学にてアロンゾ・チャーチの指導のもと、Convergent Sequences of Complete Theories という論文を完成させ博士号を取得。ソロモン・フェファーマンは後にこのころについて次のように記している。
博士号を取得するとシカゴ大学に移り、1960年まで講師として勤務。1959年にはプリンストンでの同僚マイケル・ラビンと共同で Finite Automata and Their Decision Problem という論文を発表し、非決定性有限オートマトンのアイデアを明らかにした。これが計算複雑性理論の基礎概念となったことから、ラビンと共にチューリング賞を受賞した。
カリフォルニア大学バークレー校 1960–1963 彼の業績はオートマトン理論、公理的集合論、プログラミング言語の意味論、言語哲学等、多岐にわたっており、1959年にマイケル・ラビンと共同で発表したオートマトン理論に関する研究 により、1976年度チューリング賞を受賞している。
カリフォルニア大学バークレー校で数学助教授の職を得てバークレーに戻ると、数理論理学の古典的問題、特に集合論とタルスキ的モデル理論の研究を行うようになった。
"Measurable cardinals and constructible sets" (1961) という論文において、 可測基数が存在するならば、V≠L を証明した。
このころから博士号を目指す学生を指導するようになる。このころの指導学生としては James Halpern や Edgar Lopez-Escobar がいる。
様相論理と時相論理 このころジョン・レモンと共同で様相論理の研究を始めている。レモンは1963年にカリフォルニア州クレアモントに移った。スコットは特にの時相論理と自然言語の意味論における時間の扱い方との関係に興味を持ち、バークレーの学部学生だったころからの友人であるリチャード・モンタギューと共同研究を始めた。後にスコットとモンタギューはそれぞれ独自にクリプキ意味論の様相論理および時相論理への重要な一般化を発見し、スコット-モンタギュー意味論と呼ばれるようになった。
レモンと共に様相論理の教科書を執筆していたが、1966年にレモンが亡くなったため中断した。スコットは未完成な論文を同僚らに回覧した。それはモデル理論の意味論の重要な技法をいくつか導入したもので、特にカノニカルモデルの改良と "filterations" を通してモデルを構築する重要な技法がある。それらは現代クリプキ意味論の中核概念となっている。スコットは、最終的にレモンとの共著 An Introduction to Modal Logic を出版した。
スタンフォード、アムステルダム、プリンストン 1963–1972 の初期の観測に続き、ソロヴェイやペトル・ヴォピェンカとほぼ同時期にスコットはブール値モデルの概念を定式化した。1967年の論文 A Proof of the Independence of the Continuum Hypothesis で、ブール値モデルを使い、ポール・コーエンが連続体仮説の独立性を証明したのとは別の証明を与えた。この業績により1972年にスティール賞を受賞している。
オックスフォード大学 1972–1981 1972年、オックスフォード大学哲学科の数理論理学教授の職を得た。
プログラミング言語の意味論 このころクリストファー・ストレイチーと共同研究しており、管理職としてのプレッシャーにもかかわらず、プログラミング言語の意味論の数学的基盤を築く根本的な仕事をなしとげ、この業績でスコットは最もよく知られるようになった。全体として表示的意味論へのスコットとストレイチーのアプローチを構成している。それは理論計算機科学における最も有力な業績の1つであり、計算機科学の主要な学派の基盤となった見ることもできる。中でも領域理論の定式化への貢献が大きく、再帰関数とループ制御構造を持つプログラミング言語の表示的意味論を与えることを可能にした。さらに、領域理論と彼の information system の理論を通して無限かつ連続な情報を理解する基盤を提供した。
この時期の業績から、以下のような賞を受賞している。 1990年 - ハロルド・ペンダー賞（ペンシルベニア大学） 1997年 - ショック賞（スウェーデン王立科学アカデミー） 2001年 - Bolzano Prize for Merit in the Mathematical Sciences（） 2007年 - EATCS Award
カーネギーメロン大学 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.
1967. A proof of the independence of the continuum hypothesis. Mathematical Systems Theory 1:89–111.
参考文献
Joseph E. Stoy (1977). Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press. ISBN 0-262-19147-4
脚注
外部リンク Dana S. Scott home page DOMAIN 2002 Workshop on Domain Theory — held in honor of Scott's 70th birthday.