クエリ言語における評価順序と非停止性

- Datalogは論理型プログラミング言語Prologのサブセットで、データベース問い合わせや宣言的プログラミングに使われる。Prologと違い、Datalogは本来「必ず停止する（terminate）」ことが保証されているが、実際の処理系では評価戦略（evaluation order）によって無限ループが発生することがある。 - 記事の著者Michael Arntzenius（"rntz"）は関数型/論理型プログラミング研究者で、Datalogの評価戦略や理論的性質を研究している。 - 問題の核心: Datalogが保証する停止性は「最小不動点意味論」という理想的な計算モデルに基づく。しかし実用的なコンパイラは効率のため「半ナイーブ評価（semi-naive evaluation）」という最適化を用いる。この最適化と特定の評価順序（特に制約が再帰ルールと相互に依存する場合）が組み合わさると、本来停止すべきプログラムが無限ループに陥る。 - この現象はDatalogの理論（必ず停止する）と実践（コンパイラが停止しない）のギャップを示しており、宣言的プログラミング言語の設計やデータベース問い合わせ最適化の分野で重要な問題として認識されている。 - DatomicやSouffléのような実用的Datalog処理系の実装者にとっては、評価戦略が停止性にどう影響するかを理解することが、堅牢なシステム構築に不可欠。