世界を動かす技術を、日本語で。

論理プログラミングの実装

概要

  • 多くのプログラマーが 手続き型・OOP・FP には精通
  • 論理プログラミング は知名度が低く、実務利用も少ない
  • PrologやDatalogなど 関係性・述語 で問題を記述
  • データベース的な思考 や関係性のモデル化に強み
  • Pythonによる Datalogインタプリタ の基礎実装例を紹介

論理プログラミング入門と他パラダイムとの違い

  • 多くのプログラマーは 手続き型・OOP・FP (関数型)に慣れ親しみ
  • 主要なプログラミング言語は 三つのパラダイムすべて をある程度サポート
  • HaskellのIO/StateモナドやCの関数ポインタ構造体、Javaのストリーム利用など、パラダイム横断的な実装例
  • 論理プログラミング は知名度・普及度が低く、大学で触れる程度
  • 論理プログラミング は特定の問題に非常に有効

論理プログラミングの基本概念

  • OOPやFPは 手続き型 の延長として説明しやすい
  • 論理プログラミングは 関係(relation)や述語(predicate) で記述
  • 関数 は入力と出力が明確だが、 関係 は入力・出力の区別がない
  • Prologでの例
    • male(dicky). female(anne). のような 事実(fact) の宣言
    • parent(don, randy). のような 二項関係 の記述
    • father(X, Y) :- male(X), parent(X, Y). のような ルール(rule) の定義
  • クエリ例
    • ?- father(X, randy). → X=don
    • ?- father(don, X). → X=randy, X=mike, X=anne

述語・関係の拡張と再帰

  • 新たなルールの追加で 複雑な関係性 も簡潔に表現
    • son(X, Y) :- male(X), parent(Y, X).
    • sister(X, Y) :- daughter(X, P), parent(P, Y), X = Y.
    • ancestor(X,Y) :- parent(X,Y). ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y).
  • 再帰的定義 で祖先関係なども自然に記述可能

Prologの課題とDatalogへの注目

  • Prologは 宣言的でない側面 があり、ルールの記述順が挙動に影響
  • SLD解決法 やバックトラッキングなど、実装依存の挙動
  • Turing完全であるがゆえの 無限ループや重複解答 のリスク
  • Datalog はPrologのサブセットでTuring完全でなく、 データベース的な利用 に最適
  • Datalogは SQLよりも関係性記述に長ける と評価

DatalogインタプリタのPython実装(概要)

  • 変数・値・述語使用(Atom) のデータ構造定義
    • class Variable, class Atom など
  • 述語(Predicate) は名前と引数数、事実集合、ルール集合を保持
  • ルール(Rule) はhead(結論)とbody(条件)から構成
  • Datalogクラス で全体の“データベース”を管理
  • Datalogでは
    • 否定や複雑な項の使用不可
    • すべての変数はbody内で登場必須
    • クエリ処理はナイーブなボトムアップ評価(fixpointアルゴリズム) で新事実を導出

Datalogの特徴と実用性

  • Turing完全でない ため、常に停止保証
  • データベース技術(B-tree, インデックス最適化等) の応用が可能
  • 部分評価や最適化 も容易
  • miniKanren のような関数型ロジック言語とは異なり、 状態管理型のデータベース的利用 が主眼

まとめ

  • 論理プログラミング は複雑な関係性のモデル化や推論に強み
  • Prologよりも Datalog の方が実用的なケースが多い
  • Python等の既存言語に組み込むことで、 既存のTuring完全な言語を補完
  • データベース・知識表現・推論エンジン の設計に有効

このように、論理プログラミングは「関係性のモデル化」や「推論処理」に特化したパラダイムとして、他のプログラミング手法とは一線を画す強みを持っています。特にDatalogは、既存のプログラミング言語やデータベース技術と組み合わせることで、実用性の高い知識処理基盤を構築可能です。

Hackerたちの意見

Sir Whinesalotの投稿のおすすめに賛成だよ(まだ全部読んでないけど)。miniKanrenとmicroKanrenを見てみるといいよ。数年前にmicroKanrenをOCamlに移植したとき、すごく勉強になったし、元のSchemeよりも少し理解しやすいと思う。ただ、理解するには論文を読む必要があるかもね。http://canonical.org/~kragen/sw/dev3/mukanren.ml miniKanrenの最も驚くべき成果は、前に進めたり後ろに進めたり、あるいは両方できるSchemeインタプリタだよ。http://webyrd.net/quines/quines.pdfでは、Schemeクワインを生成するのに使われているんだ。つまり、実行すると自分自身を出力するSchemeプログラムのことね(「miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl)」Byrd, Holk, Friedman)。SICPの§4.4にも、非常にアプローチしやすいSchemeでの論理プログラミングの実装があるよ。投稿とは違って、Datalogは論理プログラミングについて深い洞察を得る場所ではないと思う。むしろ、データベースについての深い洞察を得る場所だね。

SICP 4.4がとてもアプローチしやすいのに同意するよ。昔、簡単なPrologの課題があるクラスを受けたことがあって、建物の設計図をもらって、建物を通る道を解くプログラムを作ったんだ。ちょっと簡単すぎると思ったから、もっと深く掘り下げたくなった。単にタスクをこなすだけだと「これは魔法だ、これらの呪文を使えばいい」と感じるだけだったからね。Prologの実装方法を調べてみたけど、SICPのそのセクションを見つけるまで行き詰まってしまった。それで、JavaScriptに移植してProlog風の構文を与えて、課題を実行できるウェブページを作ったんだ。内部の仕組みも見せるようにして、それは今まで提出した中で一番面白いものだったよ。

インサイトなんてどうでもいい、データベース接続が肝だよ :P (記事を読んでくれてありがとう、前にmicroKanrenも実装したことがあるけど、完全な論理プログラミングエンジンを動かすのにこんなに少ないコードで済むなんて、すごいよね)

SICPの中にあるよ。https://t3x.org/amk/index.html 同じアプローチだね。古いバージョンの本が無料で手に入ると思うし、Scheme自体のものかもしれない。Schemeはホモアイコニックだから、クワインを作るのがかなり楽なんだよね。

最近、いろんなPrologの実装や制約処理ルールをいじってて、CLIPSにたどり着いたよ[0](パブリックドメインだけどNASAで開発されたんだ - かっこいいよね?)。ちょっと入りづらいけど、ルール解決がすごく速いし、純粋なCだから統合も簡単。論理言語を使ってスマートなコード解析を目指してるんだけど、これがなかなか期待できそう。Lispオタクだから、私には合ってるしね :)

https://ryjo.codes/ はこれに関してたくさんの作業をして、コースも作ったよ!

miniKanrenの実装について詳しく書いたのがここにあるよ: https://codeberg.org/ashton314/microKanren 最後には、小さな型チェッカーを実装して、逆に実行すると(型を与えることで)、その型に属するプログラムを列挙するんだ!

すごいね‽ LLMでその検索をガイドできるかな…

https://github.com/Seeker04/plwm 最近ここでPrologで実装されたウィンドウマネージャーが話題になってるよ。めっちゃクール!Prologを学ぶために新しい日常使いのツールとして使い始めたんだけど、実際に成功してる。開発者もすごくいい人で、基本的な質問や小さなPRに親切に答えてくれたよ。絶対おすすめ!興味がある人のためにGuixパッケージも持ってるよ。質の高い論理プログラミングのコードベースについてのおすすめの読み物ある?

Guixパッケージをどこかに公開した方がいいよ。

いいね!私は、構文や非線形変数の使用を妥協できるなら、結構好きな浅いバージョンのナイーブDatalogがあるよ。 edge = {(1,2), (2,3)} path = set() for i in range(10):

path(x,y) :- edge(x,y).

path |= edge

path(x,z) :- edge(x,y), path(y,z).

path |= {(x,z) for x,y in edge for (y1,z) in path if y == y1} 同じように、SQLを手書きで書くのも簡単で、見た目も似ていて、ストックデータベースエンジンから多くの機能とパフォーマンスを得られるよ。https://www.philipzucker.com/tiny-sqlite-datalog/ 最近、Z3 ASTからsqliteに小さなDatalogを書いたんだ。https://github.com/philzook58/knuckledragger/blob/main/kdrag...

わくわくするね!

ありがとう!こういうのを探してたんだけど、なぜかあなたの作品を見つけられなかったんだ。今、仕事でDatalogからPostgreSQLへのクエリエンジンを実装してるんだ。Datalogで権限ルールをモデル化して、データベース内で直接権限クエリを実行する実験をしたいからね。データベースへの往復を最小限に抑えたいから、あなたとは違うアプローチを使ってDatalogプログラムを再帰的CTEに変換してる。これには少し制限があるから、線形再帰のDatalogプログラムに制限しなきゃいけないけど、権限ルールをモデル化する目的には十分みたいだよ(例えば「権限はグループからグループメンバーに伝播する」みたいなことをモデル化できる)。

これって、離散数学の知識が必要なの?

もし自分でちょっと真面目なDatalogエンジンを書くことになったら、「SQLに変換する」機能を絶対追加したいな。あなたの作品は完璧なインスピレーションだよ、ありがとう!(Datalogでできることについての記事へのリンクも追加したよ、素晴らしい内容で、自分ではこんなにうまく書けなかったと思う)

PythonのASTとZ3を使うのもアリだよ :) ここにおもちゃみたいな実装があるよ: https://github.com/true-grue/python-dsls/blob/main/datalog/d...

Datalogについて気になっていることがあるんだけど、整数を言語に追加してもクエリ評価の終了保証を失わない方法ってあるのかな。successor()を使って整数を追加したり、concat()を使って文字列を追加すると、無限の関係を作る可能性があるみたい。整数や文字列(基本的なスカラー操作)を追加しつつ、終了保証を保つ方法ってあるのかな?記事の最後の部分では、いくつかのトリックを使えば可能かもしれないって示唆してるみたいだね。

「算術や複合原子(リストのような)をサポートすることもできるが、そうすると「チューリング不完全」であり続けるためのいくつかの課題が出てくる。」

終了チェックなしでは無理だね。Twelfを見てみて、これは依存型LF論理フレームワークに基づいた論理プログラミング言語であり、証明アシスタントなんだ。一般的な代数型を関係に使えるし、一般的なクエリは非終了になることもある。でも、システムにはモード付き関係を使って、再帰呼び出しがすべての引数で構造的に小さい項を持つかどうかをチェックする簡単な終了チェックの方法があるよ。Twelfはかなりエレガントだけど、Coqみたいな他の証明アシスタントほど強力ではないかな。Twelfの証明は、単に全体的で終了することが確認された論理プログラムなんだ。編集: 終了チェックの仕組みを示すマニュアルの短いページへのリンクはこちらだよ: https://twelf.org/wiki/percent-terminates/ Twelfの構文は他の論理言語とは少し違うけど、すべてのルールには名前が必要で、head :- subgoal1, subgoal2, ..., subgoaln の代わりに ruleName : head <- subgoal1 <- subgoal2 <- ... <- subgoaln と書く必要があることに注意してね。このアプローチはトップダウン評価にしか使えないから、無限の関係を定義することはできる(例えば自然数の後続関係は無限)。ボトムアップ評価は、あるグラウンドクエリに寄与する事実だけを導出するように制限しないと終了しないよ。誰かがその問題を調べたかは分からないけど、面白そうだね。おそらく、ボトムアップクエリを最適化するための「マジックセット」変換に関連していると思うけど、私の理解ではそれはパフォーマンスに対する確実な保証を与えないし、この問題にどう適用されるかは分からないな。

すべては項に関することだよ。ルールが単一の関係に対して無限の新しい項を生成できるようになると、例えば加算によって、非終了になっちゃうんだ。

うん、特定の種類のデータ構造に対する特定の種類の操作にはね。キーワード/特性は「単調性」だよ。単調関数は固定点セマンティクスの下で終了することが保証されてる。Datafunを調べてみて: Datalogを一般化した全体的な関数型言語だよ。それと、Datafunの著者マイケル・アーントゼニウスのStrangeloopのトークもぜひ見てみて。 https://www.rntz.net/datafun/ https://www.youtube.com/watch?v=gC295d3V9gE

こんにちは、著者です。ハッカーニュースに投稿した後、すぐに寝るのは初めてなんだけど、その時にたくさんのコメントが来るなんて(笑)。整数のサポートを追加する方法はいくつかあって、終了が保証されるんだ。最も簡単なトリックは、述語(例えば pred(X, 42))と制約(例えば X > 7)を区別することだよ。述語には事実があって、制約にはないからね。ルールの頭にあるすべての変数が本体に現れることをチェックする時、本体の中に述語が現れる条件を追加するんだ。だから、もし age(X:symbol, Y:int) みたいな述語があれば、その事実を使って考慮する整数のセットを制限できる。次に、もし age(X, A), A + 1 >= 18 と書けば、来年成人になる人を得られるよ。もっと洗練された解決策も可能で、例えば有限ドメイン制約解決の技術を使うこともできる。

これに関する最近の面白い論文があるよ: https://dl.acm.org/doi/abs/10.1145/3643027

「この記事では、任意の半環上で解釈されるときのdatalogの収束について研究します。順序付き半環を考慮し、この半環におけるdatalogプログラムの意味を最小固定点として定義し、その固定点に到達するのに必要なステップ数を調べます。半環の代数的性質がdatalogプログラムの特定の収束特性に対応することを特定します。最後に、任意のdatalogプログラムに対して半自明評価アルゴリズムを使用できる順序付き半環のクラスを説明します。これは、通常のDatalogと非常に似たフレームワーク内で線形回帰、勾配降下、最短経路(APSP)を表現できるので、かなり面白いです。収束のための必要条件についてのセクションもあります(つまり、終了条件のことです)。」

偶然なんだけど、今日はDatalogの実装を見てたんだ。Datalog(関連の)Souffléのチュートリアルの最初の方にこんなことが書いてあるよ: > 「実用的な使用のために、SouffléはDatalogを拡張して算術ファンクタを使ってチューリング同等にします。これにより、プログラマーは終了しない可能性のあるプログラムを書くことができるようになります。」 https://souffle-lang.github.io/tutorial

最近、Bret VictorのDynamiclandのブラウザ版をminiKanren、Datalog、WebAssemblyを使って実装したんだ。すごく楽しかった!自分で小さな論理プログラミング言語をゼロから作るのって、時々スーパーパワーを持ってる気分になるよね。

Pythonでの論理プログラミング、このプロジェクトは結構面白そうだね。事実を型付きオブジェクトとしてエンコードして、ルールを関数として定義して、ソルバーを使ってモデルを実行できるんだって。実際に使う理由はまだ見つけてないけどね!

このスレッドが、Mochiに論理プログラミングを追加するための最後の一押しになったよ。https://github.com/mochilang/mochi — エージェントやリアルタイムデータのために作ってる小さな静的型付けスクリプト言語なんだ。OpenAI Codexにサンプルを使って一つのプロンプトを与えたら、Goで動くDatalogエンジンを生成してくれたんだ。 - 事実のストレージ + 再帰ルールのサポート - ボトムアップの固定点評価 - 統一と!=制約 - スクリプトにfactrulequeryを公開するためのFFIバインディング 完全な思考プロセスはこちら: https://chatgpt.com/s/cd_684d3e3c59c08191b20c49ad97b66e01 実装は約250行だったよ。本当にLLMがリアルな論理レイヤーを一発で立ち上げるのにどれだけ効果的だったかに驚いてる。PRはこちらだよ: https://github.com/mochilang/mochi/pull/616

この記事は素晴らしいけど、著者がSubstackを使ったせいで台無しになってる。なんでみんな同じようにSubstackで公開するのか理解できないよ。知らない人もいるかもしれないけど、SubstackはChatGPTが何かをクロールするのを禁止してるから、AIの助けを借りてコンテンツを作ることができないんだ。彼らはこのコンテンツを無料で手に入れたくせに、利益を得るためにそれを制限したいんだよね。それに、SubstackはきれいにフォーマットされたPDFや読みやすいバージョンのダウンロードを許可しないようにして、さらにコンテンツをロックアウトしてる。正気の人はSubstackを使うべきじゃないよ。みんな、本当に、静的サイトジェネレーターを使ったGitHubページがあれば十分だよ。君のコンテンツはみんなにきれいに、そして本当に自由にアクセスできるようになるから。