Tarski's influence on computer science [pdf]
This paper explores the profound impact of Alfred Tarski's work in logic and model theory on the foundations of computer science. It examines how Tarski's semantic methods, particularly his definition of truth and model-theoretic semantics, have shaped programming language theory, database theory, and formal verification.
背景メモ
アルフレッド・タルスキ（1901–1983）は20世紀を代表する論理学者・数学者。ポーランド生まれで後に米国に移住し、カリフォルニア大学バークレー校で長く教鞭をとった。彼の「真理の意味論的定義」（公理的体系において「真」とは何かを厳密に定式化した概念）や「不動点定理」（自己言及的な定義を許すための数学的枠組み）は、後にコンピュータサイエンスの基盤に大きな影響を与える。
本PDF（著者：ソロモン・フェファーマン、スタンフォード大学の著名な数理論理学者）は、タルスキの業績が形式検証・プログラミング言語理論・データベース理論など、CSの複数の分野にどう浸透したかを歴史的に解説している。特に、タルスキの「Knaster–Tarskiの定理」（完備束上の単調関数は最小不動点を持つ）がプログラムの意味論や再帰的定義の理論へと応用された経緯が注目される。フェファーマン自身もタルスキの弟子筋にあたるため、一次資料に近い視点で書かれている。