はしくれエンジニアもどきのメモ

情報系技術・哲学・デザインなどの勉強メモ・備忘録です。

2020年代でも環境構築できる論理型言語のメモ

2020年代でも環境構築できる論理型言語のメモ

2020年代でも使えそうな論理型言語のメモ. 論理型言語自体アカデミック向けだったり最近の人工知能はディープニューラル系が多いので情報が少ない.

このあたりhttp://minikanren.org/#papers を見ると,最近では"Program Synthesis"というコードの自動生成(Quin生成)の分野では活躍してるぽい.

結論から列挙すると以下が良さげ.

Prolog

prologのコードは次の3要素で構成される.

  • fact(事実)
  • rule(規則;条件(goal)付き事実で,手続き言語でいう"function"に近い)
  • query(質問): sqlの問い合わせみたいなもの

prologではfactとruleの集まりをknowledge base(database)という.これを読み込んで,queryで解を求める.

prologの基本操作としては

  • unify(単一化):論理変数同士の値が同じになるように処理が進む.
  • backtrack(バックトラック):解が見つからなかったら戻って別の解を見つける.
  • cut(カット): ! :バックトラックを止めて制御する. 1回は動作して2回目以降!の左側とそれ以降のheadは動作しない.continue+breakのような振る舞いをする.

Swi-prolog

アムステルダム大学が開発.

https://www.swi-prolog.org/

特徴:

特にDocker imageのおかげで,OSを気にせず環境構築できる. デメとして,Docker imageを利用するとGUIのライブラリがなく,組み込みのEmacsが使えない.

Clojure

Java上でLisp方言を使えるようにした言語

公式:https://clojure.org/

JavaはopenJDKでも動作する.

core.logicがminiKanrenになっておりprologのような処理もできる.

Docker公式のイメージもある.

https://hub.docker.com/_/clojure

miniKanren

minikanren.org

miniKanrenは,論理プログラミングのためのDomain Specific Language(DSL).

"Kanren"という名前は日本語の”関連”からきてるらしい.

Clogureのcore.logicもこれになる. membromemberなどがユーザレベルで定義されている.

各言語で実装されている. このDSL上の各機能の厳密な定義はなさそう. Schemeのcore-levelの機能を調べれば必要interfaceがわかりそう.

近いのはこの論文か?

Byrd, William, "Relational programming in miniKanren: Techniques, applications, and implementations", E.Indiana University, ProQuest Dissertations Publishing, 2009. 3380156.

教科書的な本は

Daniel P. Friedman, William E. Byrd, Oleg Kiselyov, and Jason Hemann, "The Reasoned Schemer, Second Edition", The MIT Press, Cambridge, MA, 2018

miniKanrenはprologと違ってバックトラックを持たない.

microKanren

2013年に登場.論文はこれ

http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf

miniKanrenファミリのミニマリスト言語. その実装は、40行未満のSchemeで構成される。 (おそらくcore部分のみ) この量でminiKanrenと同じ機能が実装できる.

上論文のSchemeでの実際の実装がgithubにある.

GitHub - jasonhemann/microKanren: The implementation of microKanren, a featherweight relational programming language

実装の参考になりそうな論文は

Prolog vs miniKanren

ここのstackoverflow https://stackoverflow.com/questions/28467011/what-are-the-main-technical-differences-between-prolog-and-minikanren-with-resp の解答にまとまっている.

miniKanren公式にも同じ解説がある.

minikanren.org

以下,テキトーに日本語訳したもの.

それでも、miniKanrenとPrologは異なる設計哲学を持っており、異なるトレードオフを行います。

  • Prolog: シンボリック人工知能プログラミング用の2つの古典言語の1つです(他の古典言語はLispです)。 Prologは、宣言的知識が一階述語論理でエンコードされるシンボリックルールベースのシステムの実装に優れています。この言語は、論理的な純粋さを犠牲にして、これらのタイプのアプリケーションの表現力と効率を高めるように最適化されています。たとえば、デフォルトでは、Prologは統合で「発生チェック」を使用しません。数学/論理の観点から、このバージョンの統合は正しくありません。ただし、発生チェックはコストがかかり、ほとんどの場合、発生チェックがなくても問題はありません。これは、Prolog深さ優先探索を使用し、カット(!)を使用してバックトラックを制御するのと同様に、非常に実用的な設計上の決定です。これらの決定は、1970年代のハードウェアで実行する場合に絶対に必要であり、今日では、大きな問題に取り組む場合や、巨大な(多くの場合無限の)検索スペースを扱う場合に非常に役立ちます。

Prologは、カット、アサート、リトラクト、isを使用した算術演算用の変数の射影など、多くの「論理外」または「非論理」機能をサポートしています。これらの機能の多くは、複雑な制御フローを表現し、Prologの事実のグローバルデータベースを操作することを容易にします。 Prologの非常に興味深い機能の1つは、Prologコード自体がファクトのグローバルデータベースに格納されており、実行時にクエリを実行できることです。これにより、解釈中のPrologコードの動作を変更するメタインタープリタを作成するのは簡単になります。たとえば、検索順序を変更するメタインタープリターを使用して、Prolog幅優先探索エンコードすることができます。これは非常に強力な手法であり、Prologの世界以外ではあまり知られていません。 「The Art of Prolog」では、この手法について詳しく説明しています。

Prologの実装を改善するために多大な努力が払われており、そのほとんどはWarren Abstract Machine(WAM)に基づいています。 WAMは、値が論理変数に破壊的に割り当てられる副作用モデルを使用します。これらの副作用は、バックトラック時に元に戻されます。 WAMの命令を拡張することにより、多くの機能をPrologに追加することができます。このアプローチの欠点の1つは、WAMをしっかりと理解していなければ、Prologの実装ペーパーを読むのが難しい場合があることです。一方、Prolog実装者は、実装の問題を議論するための共通のモデルを持っています。 Prologと並行して多くの研究が行われ、1990年代にAndorraPrologで最高潮に達しました。これらのアイデアの少なくともいくつかは、CiaoPrologに残っています。 (Ciao Prologは興味深いアイデアでいっぱいで、その多くはProlog標準をはるかに超えています。)

Prologには、非常に簡潔なプログラムを実現する、美しい統合ベースの「パターンマッチング」スタイルの構文があります。 LispersがS式を愛するように、プロローガーは構文を愛します。 Prologには、標準述語の大規模なライブラリもあります。 WAMを高速化するために行われたすべてのエンジニアリングにより、非常に有能で成熟したProlog実装があります。その結果、多くの大規模な知識ベースのシステムは完全にPrologで書かれています。

miniKanrenは、小さく、理解しやすく、ハッキングしやすい実装を備えた、最小限の論理プログラミング言語として設計されました。 miniKanrenは元々Schemeに組み込まれており、過去10年間で他の数十のホスト言語に移植されてきました。最も人気のあるminiKanrenの実装は、Clojureの「core.logic」です。これには、多くのPrologのような拡張機能と多くの最適化が含まれています。最近、miniKanren実装のコアがさらに単純化され、「microKanren」と呼ばれる小さな「マイクロカーネル」が作成されました。その後、miniKanrenをこのmicroKanrenコア上に実装できます。 microKanrenまたはminiKanrenを新しいホスト言語に移植することは、miniKanrenを学ぶプログラマにとって標準的な演習になっています。 その結果、最も人気のある高級言語には、少なくとも1つのminiKanrenまたはmicroKanrenが実装されています。

miniKanrenとmicroKanrenの標準実装には、1つの例外を除いて、突然変異やその他の副作用は含まれていません。miniKanrenの一部のバージョンでは、論理変数の比較にポインターの等価性が使用されます。私はこれを「良性の効果」と考えていますが、多くの実装では、実装にカウンターを渡すことでこの効果すら回避しています。グローバルファクトデータベースもありません。 miniKanrenの実装哲学は、関数型プログラミングに触発されています。突然変異と影響は避け、すべての言語構造は字句スコープを尊重する必要があります。実装を注意深く見ると、いくつかのモナドを見つけることさえできるかもしれません。検索の実装は、ミューテーションを使用せずに、レイジーストリームを組み合わせて操作することに基づいています。これらの実装の選択は、Prologとは非常に異なるトレードオフにつながります。 Prologでは、変数ルックアップは一定時間ですが、バックトラックには副作用を元に戻す必要があります。 miniKanrenでは、変数ルックアップはより高価ですが、バックトラックは「無料」です。実際、ストリームの処理方法が原因で、miniKanrenにはバックトラックはありません。

miniKanren実装の興味深い側面の1つは、コードが本質的にスレッドセーフであり、---少なくとも理論的には---簡単に並列化できることです。もちろん、各スレッドまたはプロセスに並列化のオーバーヘッドを補うのに十分な作業を与える必要があることを考えると、コードを遅くせずに並列化することは簡単ではありません。それでも、これはminiKanrenの実装分野であり、もっと注目され、実験されることを願っています。

miniKanrenは、unifyのために発生チェックを使用し、深さ優先探索の代わりに完全なインターリーブ検索を使用します。インターリーブ検索は深さ優先検索よりも多くのメモリを使用しますが、深さ優先検索が永久に分岐/ループする場合には答えを見つけることができます。 miniKanrenは、いくつかの特別な論理演算子condaconduprojectなど)をサポートしています。 condaconduを使用してPrologのカットをシミュレートでき、projectを使用して論理変数に関連付けられた値を取得できます。

condacondu、およびprojectの存在---および検索戦略を簡単に変更する機能---により、プログラマーは、埋め込まれたPrologのような言語としてminiKanrenを使用できます。これは、多くのPrologのような拡張機能を含むClojureの「core.logic」のユーザーに特に当てはまります。 miniKanrenのこの「実用的な」使用は、業界でのminiKanrenの使用の大部分を占めているようです。 ClojurePython、またはJavaScriptで記述された既存のアプリケーションに知識ベースの推論システムを追加したいプログラマーは、通常、Prologでアプリケーション全体を書き直すことに関心がありません。 ClojureまたはPythonに小さな論理プログラミング言語を組み込むことははるかに魅力的です。埋め込まれたPrologの実装は、おそらくこの目的のためにも同様に機能します。 miniKanrenは、「The Reasoned Schemer」の発行以降に発表された講演、ブログ投稿、チュートリアル、その他の教材に加えて、小さくて純粋なコア実装により、組み込みロジック言語として人気が高まっていると思います。

miniKanrenは、Prologと精神的に似た実用的な組み込み論理プログラミング言語として使用されているだけでなく、「リレーショナル」プログラミングの研究にも使用されています。つまり、数学関数ではなく数学関係として動作するプログラムを作成する場合です。たとえば、Schemeでは、append関数は2つのリストを追加して、新しいリストを返すことができます。関数呼び出し(append '(a b c)'(d e))はリスト(a b c d e)を返します。ただし、appendを2つの引数関数としてではなく、3つの場所の関係として扱うこともできます。次に、呼び出し(appendo '(a b c)'(d e)Z)は、論理変数Zをリスト(a b c d e)に関連付けます。もちろん、論理変数を他の位置に配置すると、状況はさらに興味深いものになります。呼び出し(appendo X '(de)'(abcde))はXを(abc)に関連付け、呼び出し(appendo XY '(abcde))はXとYを、追加されると(abcde)に等しいリストのペアに関連付けます。 )。たとえば、X =(a b)Y =(c d e)はそのような値のペアの1つです。 (appendo X Y Z)と書くこともできます。これは、リストX、Y、およびZのトリプルを無限に生成し、XをYに追加するとZが生成されます。

このリレーショナルバージョンのappendは、Prologで簡単に表現でき、実際、多くのPrologチュートリアルで示されています。実際には、より複雑なPrologプログラムは、カットなどの少なくともいくつかの特別な機能を使用する傾向があり、結果のプログラムを関係として扱う能力を阻害します。対照的に、miniKanrenは、このスタイルのリレーショナルプログラミングをサポートするように明示的に設計されています。 miniKanrenの最近のバージョンでは、シンボリック制約の解決(シンボロ、ナンバー、アブサン、不等式制約、名目論理プログラミング)がサポートされており、重要なプログラムをリレーションとして簡単に記述できます。実際には、miniKanrenの特別な機能を使用することはなく、すべてのminiKanrenプログラムをリレーションとして作成します。最も興味深いリレーショナルプログラムは、Schemeのサブセットのリレーショナルインタープリターです。これらのインタプリタには、リストに評価される100万のSchemeプログラム(I love you)を生成したり、クイン(自分自身に評価されるプログラム)を簡単に生成したりするなど、多くの興味深い機能があります。

miniKanrenは、このリレーショナルスタイルのプログラミングを可能にするためにいくつかのトレードオフを行います。これは、Prologが行うトレードオフとは大きく異なります。時が経つにつれて、miniKanrenはより多くの記号制約を追加し、実際には記号指向の制約論理プログラミング言語になりました。多くの場合、これらのシンボリック制約により、conduやprojectなどの論理外の演算子の使用を避けることが実用的になります。その他の場合、これらのシンボリック制約は十分ではありません。シンボリック制約のより良いサポートは、関係としてより大きくより複雑なプログラムをどのように書くかというより広い問題とともに、miniKanren研究の1つの活発な領域です。

要するに、miniKanrenとPrologはどちらも興味深い機能、実装、使用法を持っており、両方の言語からアイデアを学ぶ価値があると思います。 Mercury、Curry、Gödelなど、他にも非常に興味深い論理プログラミング言語があり、それぞれが独自の論理プログラミングを採用しています。

最後に、いくつかのminiKanrenリソースを紹介します。

Hy

pythonLisp方言を使えるようにしたもの. python上で動作してHyの式をpythonへの変換もできる.

The Hy Manual — hy 0.20.0+1.g0e4d576c documentation

docker imageがDocker公式から出ている.

https://hub.docker.com/_/hylang

※日本のバンドではない.

Hy上のminiKanrenの実装はいくつかあるが, adderallが使いすそう,

Racket

Schemeから派生した言語.研究向け.

Dockerイメージはracket公式が出してるものがある. https://hub.docker.com/r/racket/racket-ci

SchemeバイブルのSICP本用のパッケージも用意されてる.

docs.racket-lang.org