Loading article…
λProlog （ラムダ Prologとも表記）は、多相型付け、モジュール型プログラミング、高階プログラミングを特徴とする論理プログラミング言語です。これらのPrologへの拡張は、λProlog の基礎を正当化するために使用される 高階遺伝的Harrop 式から派生しています。高階量化、単純型付け λ 項、および高階単一化により、λProlog は、高階抽象構文への λ ツリー構文アプローチを捉えるために必要な基本的なサポートを提供します。これは、オブジェクトレベルのバインディングをプログラミング言語のバインディングにマッピングする構文表現アプローチです。λProlog のプログラマは、バインドされた変数名を扱う必要はありません。代わりに、バインダー スコープとそのインスタンス化を扱うためのさまざまな宣言的デバイスが利用可能です。
λPrologは1986年以来、数多くの実装が開発されてきた。2023年現在も、この言語とその実装は活発に開発が続けられている。
Abella定理証明器は、λPrologの宣言型コアに関する定理を証明するための対話型環境を提供するように設計されています。
λPrologの2つの特徴は、含意と全称量化です。含意は述語定義の局所スコープに使用され、全称量化は変数の局所スコープに使用されます。例えば、補助述語revに依存するreverseの以下の実装が挙げられます。
reverse L K :- pi rev \ ( rev nil K & ( pi H \ pi T \ pi S \ rev ( H :: T ) S :- rev T ( H :: S ))) => rev L nil 。?-逆[ 1 , 2 , 3 ] L 。成功: L = 3 :: 2 :: 1 :: nil これらのスコープ構造の一般的な用途は、論理の推論規則表現でよく見られるスコープをシミュレートすることです。例えば、自然演繹における証明探索（および証明チェック）は、次のように符号化できます。
pv Pf P :- hyp Pf P . pv ( andI P1 P2 ) ( and A B ) :- pv P1 A , pv P2 B . pv ( impI P ) ( imp A B ) :- pi p \ ( hyp p A ) => ( pv ( P p ) B ) . pv ( andE1 P ) A :- sigma B \ hyp P ( and A B ) . pv ( andE2 P ) B :- sigma A \ hyp P ( and A B ) . pv ( impE P1 P2 ) B :- sigma A \ hyp P1 ( imp A B ) , pv P2 A .?- pi p qr \ pv ( Pf p q r ) ( imp p ( imp ( and q r ) ( and ( and p q ) r ))) 。成功: Pf = W1 \ W2 \ W3 \ impI ( W4 \ impI ( W5 \ andI ( andI W4 ( andE1 W5 )) ( andE2 W5 )))