# Robert W. Floyd ## 概要 1967年、Carnegie Tech(その翌年にCarnegie Mellon Universityへ改称)に在籍していた頃、不変条件原理(Invariant Principle)——状態機械の保存される不変条件が開始状態で真であればすべての到達可能な状態で真である、という原理——を定式化した計算機科学者。この原理は帰納法を段階的プロセス(状態機械)向けに再定式化したものであり、プログラム検証を部分正当性(partial correctness)と停止性(termination)の2性質に分解する枠組みとあわせて、プログラム検証という分野の基礎を築いた。プログラミング言語の構文解析を一変させた形式文法の研究でも既に著名で、博士号を持たないまま(10代の神童として博士課程に入学したが中退した)教授職に就いた経歴を持つ。1967年に当時Carnegie Tech計算機科学科の新任助教授だったAlbert R. Meyer(本書の共著者)と出会い、不変条件原理を説明した際、Meyerは当初その「明白さ」に価値を見出せなかったが、Floydが示した数々の応用例を通じて、単純な観察が広く容易に適用できることの重要性を理解したという逸話が本書に記されている。翌1968年にStanford大学へ移り、1970年代後半に形式文法とプログラム検証の基礎への貢献でチューリング賞(計算機科学のノーベル賞と称される)を受賞した。2001年9月にStanfordで死去。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] §5.4.3) 第6章の「Expression Parsing」コラムは、Floydの受賞理由の一つとして、式の評価順序を決める括弧を自動的に正しく挿入する簡潔な手続き(式の構文解析アルゴリズム)を発見したことを挙げている。1950〜60年代のコンパイラ開発における中心課題だった式の構文解析は、70〜80年代にコンパイラコンパイラによる自動化が進んだ結果、90年代までに計算機科学のカリキュラムからほぼ姿を消したと本書は述べる。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]] §6.2) ## 関連 - 概念: [[不変条件]]、[[状態機械]]、[[再帰的データ型]] - 章: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]]、[[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]] ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 5, §5.4.3. - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 6, §6.2.