Mirroring Call-by-Need, or Values Acting Silly

あなたは、忙しい厨房で複雑な料理を準備するための最も効率的な方法を考えあぐねている、あるシェフだと想像してください。コンピュータサイエンスの世界、特に「プログラミング言語理論」と呼ばれる分野では、シェフたちは実際には数学者や論理学者であり、コンピュータがコードを実行する際にどのように「考える」のかを研究しています。彼らは食べ物を料理しているのではなく、記号や命令を操作しているのです。彼らが問いかける中心的な質問は、「コンピュータがあるタスクに直面したとき、すぐに作業を行うべきか、それとも絶対に必要な時まで待つべきか？」というものです。

これを理解するために、2つの異なる調理スタイルを想像してみてください。最初のスタイルは「コール・バイ・ネーム（名前による呼び出し）」と呼ばれ、レシピが明示的に要求するまで玉ねぎを切ることを拒む、怠け者のシェフのようなものです。もしレシピに「玉ねぎを捨てなさい」と書かれていれば、怠け者のシェブはナイフさえ手に取りません。これにより、時間と労力を節約できます。これは「捨てること（消去）」については「賢い」のですが、「切ること（複製）」については「愚か」です。なぜなら、もしレシピが2回玉ねぎを求めた場合、怠け者のシェフは2回切ってしまうからです。2番目のスタイルは「コール・バイ・バリュー（値による呼び出し）」と呼ばれ、レシピが始まる前に、あらゆる食材を即座に刻んでしまう、超準備万端なシェフのようなものです。これは「切ること」については「賢い」のですが（一度だけ切るため）、「捨てること」については「愚か」です（レシピが後に無視するように指示した玉ねぎまで切ってしまう可能性があるため）。

数十年にわたり、科学者たちは「コール・バイ・ニード（必要に応じた呼び出し）」と呼ばれる第3のスタイル、つまり完璧なシェフであろうとするスタイルに魅了されてきました。このシェフは、必要になるまで切るのを待ち（消去に対して賢い）、かつ、もし何度も必要になったとしても一度しか切りません（複製に対して賢い）。しかし、もし私たちがその正反対を研究したいとしたらどうでしょうか？ つまり、シェフが切ることと捨てることの両方において、いかに下手であるかを調べたいとしたら？ これが、論文『Mirroring Call-by-Need, or Values Acting Silly（コール・バイ・ニードの鏡像、あるいは愚かに行動する値）』が答えを出そうとしている、奇妙で愉快な問いです。

著者であるベニアミーノ・アッカートリとアドリアン・ランセルは、彼らが「コール・バイ・シリー（愚かさによる呼び出し）」と名付けた、意図的に非効率な新しい調理スタイルを設計することに決めました。この世界では、シェフは使われない食材であっても刻み（複製に対して愚か）、まだ切られていない食材であっても捨ててしまいます（消去に対して愚か）。これは災難へのレシピのように聞こえますし、著者自身もそれが「絶望的に非効率」であることを認めています。しかし、彼らは良い料理を作ることには関心がありません。彼らは、厨房のルールそのものを理解することに関心があるのです。この「愚かな」システムを構築することで、彼らは「賢い」システム（コール・バイ・ニード）が、確かにレイジーなもの（コール・バイ・ネーム）の完璧な最適化であることを証明し、さらに「準備万端な」システム（コール・バイ・バリュー）について驚くべき発見をしました。

この論文は、料理の最終的な結果を見る限り、「準備万端な」シェフ（コール・バイ・バリュー）と「愚かな」シェフ（コール・バイ・シリー）は、全く同じ結果を生み出すことを証明しています。たとえ愚かなシェフが大量の不要な作業を行ったとしてもです。これは、私たちがプログラムを測定する方法における隠れた盲点を明らかにしています。つまり、2つのプログラムが「同じ」であるかどうかをチェックする標準的な方法は、一方がどれほど余計な仕事をしたとしても、その違いを見分けることができないのです。純粋で副作用のない厨房においては、標準的な同値性のルールは「効率に対して盲目」であることが判明しました。

これを証明するために、著者たちは単に推測したのではなく、数学的な機械、いわば「ロボット・シェフ」である「Silly MAM」を構築しました。これは愚かなルールに従ってステップごとに進むものです。また、彼らは「マルチタイプ（食材に何回触れたかを正確に追跡する、非常に詳細なレシピカードのようなもの）」を用いた特別な計数システムを作成しました。彼らはこのシステムを使って、愚かなロボットが行ったすべてのステップを数えました。その結果、愚かな戦略は、タスクを完了するために「最長」の経路を辿ることがわかりました。コール・バイ・ニードのロボットが最短の経路を辿る一方で、コール・バイ・シリーのロボットは、可能な限り最大数のステップを踏むのです。

この論文は、単なるシミュレーションではなく、厳密な数学的証明です。著者たちは新しい計算体系（記号を操作するためのルールの一群）を構築し、それが一貫して動作することを証明し、取られたステップの正確な数を測定するために形式的な型システムを用いました。彼らは、この「愚かな」システムが「必要（ニード）」システムの完全な鏡像であることを示しました。「ニード」システムが2つの世界のベストを組み合わせているのと同様に、「シリー」システムは最悪の2つを組み合わせています。

最も重要な発見は、この「愚かな」振る舞いが、標準的な「コール・バイ・バリュー」言語におけるプログラムの同値性の定義における限界を露呈させていることです。この論文は、プログラムが外部の世界（ファイルの変更や画面への出力など）と相互作用しない限り、一つのプログラムが膨大な無駄な作業を行っていたとしても、もう一つのプログラムが全く行っていなくても、両者は数学的に同等であることを示しています。これは、プログラムが「等しい」かどうかをチェックする現在のツールが、決定的な詳細を見落としている可能性があることを示唆しています。つまり、それらは「無駄に費やされた努力」をカウントしていないのです。

結局のところ、この論文は私たちに「愚かな」コードを書き始めるよう促しているわけではありません。むしろ、この不条理で非効率なシステムを、効率的なシステムをより良く理解するための「鏡」として利用しているのです。それは、コール・バイ・ニードが素晴らしい最適化である一方で、コール・バイ・バリューには、同値性を捉える方法における隠れた欠陥があることを示しています。つまり、コール・バイ・バリューは、あなたが賢かろうと愚かろうと、仕事さえやり遂げれば構わないと考えているのです。著者たちは、コンピュータサイエンスの地図の中に「愚かな」コーナーを設けることで、風景をより鮮明に見る手助けをすることに成功しました。何かを最善の方法で行う方法を理解するためには、時には最悪の方法を研究しなければならないということを証明したのです。