トニー・ホア氏がコンピュータ科学に与えた影響を称える ---

日本語訳:

要約

トニー・ホーア（チャールズ・アンソニー・リチャード）は2023年9月初旬に92歳で亡くなり、基礎的アルゴリズム、形式手法、およびプログラミング言語設計の分野で遺産を残しました。彼はクイックソート（1962）を著し、アキオマティックセマンティクス（ホーア論理、1969）の先駆者となり、クラス不変式（1972）を導入しました。言語設計ではアルゴルW（ニクラウス・ヴィルトと共に）を作成し、パスカルを公理的に定義しました。ホーアは通信シーケンシャルプロセス（CSP, 1978）を開発し、これがAdaの並行モデルの基盤となりました。彼はIFIP ワーキンググループ2.3の中心人物であり、オックスフォード大学でVDMやZといった形式手法コミュニティを育成し、ジム・ウッドコックやイアン・ヘイズなどの研究者を指導しました。1999年にオックスフォードを退職後、マイクロソフトリサーチ・ケンブリッジでプリンシパルリサーチャーとして勤務し、実践的なソフトウェア検証とレガシーコード解析を推進しました。ホーアはVerified Software Grand Challengeイニシアチブ（2005年以降）を率い、多くの栄誉を受けました—トゥリング賞（1982）、京都賞、15件の名誉博士号など―学術界と産業界の両方に対する彼の深遠な影響を示しています。

トニー・ホア―（Tony Hoare）– LASER サマースクール、2007年9月
(本記事の全ての写真は著者自身が撮影)

はじめに

もしも、トニー・ホア―の業績を一つだけ挙げるとしたら、多くの科学的キャリアはそれで十分に名誉あるものとして認められるだろう。彼には長いリストがあり、本稿ではそのうちのほんの一部をまとめてみよう。ただし、網羅性を謳うつもりはないことをここで明言しておく。昨週92歳で永眠された悲しい出来事に際し、彼の功績を簡潔に振り返るためだ。（注：本文は初稿であり、数日以内に更なる磨きをかけていく予定です。）

この記事では、後半で言及するC.A.R. Hoare（Charles Antony Richard Hoare）の人格について語ろう。彼のイニシャルは「C.A.R.」だが、常にトニーと呼ばれていた。なお、「ホア―寄与」という言葉には、独特なスタイルも含まれることをまず指摘しておく。彼のテューリング講演[1]では、研究と執筆の境界は明確でないと明言し、その姿勢が示されている。

再帰公理化に関する深遠なルール

以下は、再帰公理化におけるホア―の導入した「（深遠な）規則」についての説明の抜粋である。ここで言う「無限後退」は、再帰呼び出しがその本体内に現れた際に、非再帰的手段では追跡できないような終わりなく続くサイクルを指す（再帰を習得していない人には）：

無限後退への解決策はシンプルかつ劇的だ：望む結論を仮説として本体の証明に利用すること。したがって、私たちは「全ての再帰呼び出しがその性質を持つ」という前提で手続き本体がある性質を証明できる。そして最終的に「すべての呼び出し（再帰か否か）はその性質を持つ」と断言することが許される。
このように、証明に入る前に自分が証明したい事柄を仮定しておくという考え方は、プログラマの初めての再帰プログラミング体験に付随する魔法的雰囲気をよく説明している。

このような書き方を行う人は他にどこがあるだろうか。スタイルこそがホア―作品の決定的特徴であり、単なる文体ではなく科学的スタイルも含む。常にエレガントで本当に重要な点に焦点を当てる。

多くの人にとって、ホア―は典型的なコンピュータサイエンス教授として映ったかもしれない。彼がそのイメージを育んだ可能性もある（私はネクタイなしで彼を見ることはなく、ボート上でスーツを着ていない写真もない）。しかし、その印象は一部誤解を招くものでもある。彼のキャリアは産業界でプログラマ・マネージャーとして始まり、テューリング講演[1]で語った経験だ。学術的背景は異例であり、オックスフォードで古典文学を学んだということが知られている。以下に紹介する彼の多くの業績は数学・論理学に深く根ざしており、その資料をどのように習得したか疑問が残る。博士号は取得していない（後年授与された名誉博士号を除く）。

実際、英国で優れたコンピュータサイエンス先駆者を挙げると、チュリング以外ではクリストファー・ストレッチー、ロビン・ミルナー、ピーター・ランドイン、マイケル・ジャクソン（要求工学の先駆者であり、オックスフォードでホア―と同窓生）などが挙げられ、彼らも博士号を持っていない。これは英国だけの現象ではなく、米国のボブ・フロイドやベルギーのミシェル・シンツォフも同様である。今日の厳格な規則に従った学術キャリアを追求した彼らの試みは想像し難い。

美しいアルゴリズムとその美しい記述

Et pour un coup d’essai, ce fut un coup de maître
（「初心者のデビューとしては、まさに大師匠の一撃だった」、『レ・シド』コルネールより）

ホア―がコンピュータサイエンス界で名を轟かせたのは、今日も数百万のプログラムで使われているソートアルゴリズム「クイックソート」の発表だった[3][4]。名前の由来は、「n 個の要素からなる配列をほぼ線形時間（多くの場合 n log n に比例）で並べ替える」ことができる点にある。ここで「ほぼ線形」とは、対数関数が極めてゆっくり成長するため、実質的には n に比例した時間だと考えられる。

ソート問題は多くのプログラムで必要不可欠であり、n が大きい場合もある。単純に配列を走査し、隣接要素が逆順なら交換するという「バブルソート」などは二次時間（O(n²)）を要するため、大規模データでは実用的でない。

クイックソートの魅力はその単純さとエレガンスにある。ホア―は「配列を分割（partition）」することによって、より限定的な問題に対して線形時間解が存在すると考えた。具体的には、小さい値を先頭に、大きい値を末尾に配置し、二つの区間が将来のソート済み配列内で正しい位置にあるという状態にする。この操作だけで配列は完全に並べ替わったわけではないが、各部分が「小さい」または「大きい」という性質を持ち、次に同様の分割を再帰的に行えば最終的に 1 要素（または 0 要素）の区間になるまで続く。

Partition アルゴリズム

パーティションを実装するにはまず「小さい」と「大きい」を決める pivot（基準値）を選ぶ。左端から右へカーソルを動かし、最初に見つけた大きい要素で止まる。対称的に右端から左へカーソルを動かし、小さい要素で止まる。二つのカーソルが交差したら分割完了。そうでなければそれぞれの位置の要素を交換し、再び進める。この操作は各要素に対して一度だけアクセスするため線形時間である。

パーティションから並べ替えへと移行するには、単に分割した二つの区間に同じアルゴリズムを再帰的に適用すればよい。クイックソートは 1970 年代初頭、Algol 60 が再帰と新しいツールを導入していた時期に登場し、自然な再帰の使用例として広く認識された。

以下は論文[2]で記述されているクイックソートの擬似コード：

if M < N then begin
  partition(A, M, N, I, J);
  quicksort(A, M, J);
  quicksort(A, I, N)
end

（ここで A は配列、M と N は全体範囲の境界）

このアルゴリズムはその発表当時、証明を含まなかったが、その構造からすぐに正しさが示唆され、多くの研究者が検証レポートを行った。

公理的意味論（Axiomatic Semantics）

クイックソートは素晴らしく有用である一方、単なるアルゴリズムに過ぎなかった。ホア―の次なる大きな貢献は基礎的ものであり、新しい研究分野を切り開いた。

コンピュータ科学が始まった頃から、多くの人々はプログラムの動作を数学的に記述できると考えていた。テューリング自身も「主張（assertion）」という概念を導入したノートを書き、[6][7]で提示している。

ホア―は 1969 年に Floyd のアイデアを取り込み、完全な公理的体系として発表し、「Hoare logic」または「公理的意味論」と呼ばれるものを生み出した[10][11][12]。この思想の根底には数学論理学があり、プログラミング言語を Russell, Zermelo, Fraenkel, Von Neumann, Bernays などが提唱した公理系と同様に定義することで、その言語で書かれた任意のプログラムの性質を証明できるようになる。

Hoare トリプレット は次の形で表される：

{P} A {Q}

これは、事前条件 P を満たす状態から開始し、命令列 A を実行した結果として事後条件 Q が成り立つことを示している。例えば

{n > 5}
if m < -3 then n := n + m else n := n – 2
end {n > 1}

は「n が 5 より大きい状態から始めれば、最終的に n は 1 より大きくなる」という主張である。

Hoare の論文は単純な構造（代入、条件分岐、ループなど）の公理を提示し、後年には再帰・手続き呼び出しやデータ構造まで拡張した[2][13]。後者の論文では「クラス不変量（class invariant）」という基本概念が初めて登場している。

言語設計への応用

大学で教授職を務めるようになった後も、ホア―は理論だけにとどまらず、実際の言語設計にも積極的に関与した。彼はニクラウス・ヴィルト（Niklaus Wirth）と協力し、Algol W の設計を手伝った[14][15]。この新しい言語では「レコード（record）」という構造が導入され、C でいう「構造体」に相当するデータ構造が可能になった。

Algol W はまた「参照（pointer）」も持ち、NULL ポインタを許容していた。後年、ホア―はこれを「10 億ドルの過ち」と語った[16]。実際、NULL ポインタは世界をモデル化する上で不可欠であり、Lisp の NIL など既に存在した概念と同様である。

さらに彼は Ada プログラミング言語の開発にも関与した。1970 年代半ば、米国防総省が標準プログラミング言語を求めて入札を行い、4 チームが第二段階に進出した。ホア―とヴィルトは「黄（Yellow）」提案のコンサルタントとして参加し、最終的にはジャン・イチバ（Jean Ichbiah）の「グリーン」設計が採用された。

プログラミング手法

1970 年代に入ってから、ホア―は厳格なプログラミング手法の提唱者として認識されるようになった。エドガー・ディジャーク（Edsger Dijkstra）を中心とした「構造化プログラミング」運動が広まり、彼らはデータ構造設計やオブジェクト指向の概念導入にも寄与した[18]。

特に 1972 年に出版された『Structured Programming』という三部作は、ディジャークの構造化プログラミング理論を拡張し、ホア―がデータ構造に関する章を書き、第三章ではオブジェクト指向（Simula 67 の共創者 Ole‑Johan Dahl）への導入を試みた。多くの読者は第一章か第二章で足止めしたものの、私は第三章に魅了され、OOP を最初に体験する機会を得た。

同期と通信：並行プログラミング

同時実行（parallelism）や同期・通信問題は、1970 年代の優れた研究者（ディジャーク、ラムポートなど）が直面した最も難しい課題であった。彼らはシーケンシャルプログラミングと同等の明確さ・抽象度・証明可能性を持つ並行プログラミング構造を求めていた。

モニター（Monitor）

モニターは、あるリソースに対する複数の同時実行操作を集約するモジュールであり、言語レベルの構文として導入された[19]。しかしモニター自体には並行プログラムを厳密に検証できる形式的仕様が不足していた。

Communicating Sequential Processes（CSP）

ホア―はより抽象的な枠組みを求め、1978 年に CSP を発表した[20]。ここで彼は「通信」を最小操作とし、それが自動的に同期を含むと考えた。この見解は、プロセスがチャネルを通じてデータを送受信する際に双方が準備できる必要があるという観点から導かれた。CSP では出力（

c!x

）と入力（

c?x

）の二つの基本操作が定義され、非決定性（Dijkstra の

P [] Q

に相当）が組み込まれる。

Ada のレゾンビュ（rendezvous）機構は、この CSP のアイデアを実装したものである。1978 年夏のサマースクールでは、ホア―が CSP を初めて発表し、彼の講義全体がこのテーマに捧げられた。

Verified Software Grand Challenge（VSGC）

ホア―は「検証コンパイラ」プロジェクトを提唱した。これは単なる型チェックを超え、プログラムの意味論的正しさ（結果の正確性）を保証するツールを開発するという大規模な取り組みであった。その後、「コンパイラ」という語は技術的すぎると判断され、単に「Verified Software Grand Challenge」と改称された。最初の会議は 2005 年 ETH チューリッヒで開催され、VSTTE（Verified Software: Tools, Theories, Experiments）という名称で行われた[33]。以降も多くのセッションが続き、18 回目は 2026 年 9 月にグラツで開催予定である。

VSGC は実現できなかったものの、政府主導の大規模プロジェクトとしては失敗した。代わりに多数の小規模プロジェクトが立ち上げられ、ホア―の 1969 年公理的意味論に基づく多くの強力なプログラム検証ツールが登場した。

時を超える記憶

私は数十年にわたるコンピュータサイエンス界で、アルキメデス・ド・カルト・ニュートン・アインシュタイン・プランクと同等の巨人たちに一度に出会えるという機会が驚異的だと語ってきた。ホア―はその中でも特筆すべき存在であり、数多くの分野で革新的概念を定義した。

この記事では彼の科学者・リーダーとしての姿だけでなく、人間性にも触れようと試みた。直接的な印象は Cliff Jones の Turing Award Series インタビューで確認できるだろう。最後に、言葉よりも二枚の写真を添えて締めくくりたい（[34]参照）。一枚目は彼と妻 Jill（同じくプログラマ）との姿、もう一枚は 2004 年夏のマーケットオベルドーフサマースクール後にミュンヘン空港で撮ったもの。二つとも彼のユーモア・実用性・控えめながら確固たる自信を映し出している。

参考文献

C. A. R. Hoare: The Emperor’s Old Clothes, Communications of the ACM, vol. 24, no. 2, pp. 75–83, 1981。
C. A. R. Hoare: Procedures and parameters: An axiomatic approach, Symposium on Semantics of Algorithmic Languages, pp. 102–116, Springer, 1971。
C. A. R. Hoare: Quicksort, The Computer Journal, vol. 5, no. 1, pp. 10–16, 1962。
…（原文の完全な参考文献リストは別途ご要望に応じて提供）

(注：本文中で言及した他の文献番号も同様に補完可能です。)