λProlog とは何か ── AI が数学を証明する時代、定理証明系 Rocq の内側で働く知られざる言語

はじめに

AI が数学の定理を証明する時代が始まっています。

Google DeepMind の AlphaProof や中国発の DeepSeek-Prover のように、大規模言語モデルが証明の候補を書き、それを機械が厳密に検査するという研究が急速に伸びています。

機械学習に馴染みのある方なら、ここに面白い対比があることに気づくはずです。

ニューラルネットワークの出力は「たぶん正しい」としか言えません。

ところが機械の検査を通った数学の証明は「間違いなく正しい」と言い切れます。
あいまいさを許さない検査を通り抜けているからです。

この「機械が証明を検査したり探したりする世界」の舞台裏で、日本ではほとんど知られていない一つのプログラミング言語が働いています。

証明の合否を最終判定する検査装置そのものとして、ではありません。

その手前で、押し寄せる証明の候補を検査し、整え、さばいていく層
── 検査装置が最終面接だとすれば、書類審査にあたる層
── を書くための言語として、世界的な定理証明系の内側で稼働しているのです。

その言語の名は λProlog（ラムダ・プロログと読みます）。本記事の主役です。

本記事は、論理プログラミングも関数型プログラミングも論理学も学んだことのない読者を想定しています。
専門用語は初めて登場するたびにその場で説明します。

前提知識は Python の経験だけで十分です。

この記事の全体像 ── 順路と結論を最初に

本記事はかなり長い記事です。

迷子にならないように、最初に結論と地図を示しておきます。

結論を先に言うと

λProlog は、Prolog を高階論理と単純型付きラムダ計算で拡張した論理型プログラミング言語です。

λProlog のプログラムを実際に動かすソフトウェア ── これを「実装」と呼びます ── が ELPI で、この ELPI は世界的な定理証明系 Rocq（旧 Coq）の公式な拡張言語 Coq-Elpi として実務で稼働しています。

そして AI が数学の証明を書く時代の中で、「AI の出力を受け止め、厳密に検証しながら定理証明系につなぐ」橋渡し役として、その価値をさらに高めていく ── これが本記事の結論です。

誤解の無いように、この「橋渡し」の意味を補足しておきます。

Rocq が AI の出力を受け取るために、ELPI の検証を必ず経由しなければならない、という意味ではありません。

証明の正しさを最終的に保証するのは、あくまで Rocq 本体の検査装置（カーネルと呼びます）です。

では ELPI の層は何を検証するのでしょうか。

会社の採用にたとえるなら、カーネルが最終面接、ELPI は書類審査にあたります。

最終面接だけでも合否は決められます。

しかし AI が大量の候補 ── その多くは形式の整っていない不合格品 ── を次々に送り込んでくる時代には、手前で候補を検査して弾き、整え、順に試していく受付の層が欠かせません。

この受付の仕事 ──「候補の型や形が要件に合っているかの事前検査」「不合格品への分かりやすいエラー返し」「候補の変換と再試行」── を書くための言語が ELPI なのです。
（この仕組みは、節5（AI との接点） で実際のコードとともに確かめます）

ここに出てきた用語はすべて本文で一つずつ説明するので、いまの時点で分からなくても大丈夫です。

順路 ── ３部構成で進みます

第１部（基礎編）── 前提知識ゼロから、次の４段階で土台を作ります。

1. まず「論理プログラミング」とは何か、その代表である Prolog とは何かを知る
    
2. 次に、Prolog を拡張した言語である λProlog を知る
    
3. そして「定理証明系」── 数学の証明を機械が支える仕組み ── を知る
    
4. 最後に、λProlog の実装である ELPI が定理証明系の内側でどう働いているかを知る

第２部（本編）── この４段階を土台にして、λProlog の歴史・技術の核心・実務での使われ方・AI との接点を掘り下げます。本編が答えるのは次の 5 つの問いです。

• λProlog とは何か？
   
• λProlog はコンピュータ・サイエンス全体の中でどこに位置する言語なのか？
   
• λProlog が設計・開発された動機と目的は何か？
   
• Prolog と何が違うのか？ 採用された高階抽象構文（HOAS）とは何か？
   
• Rocq の拡張 Coq-Elpi や Abella などでどう使われ、AI・定理証明とどう接点を持つのか？

第３部（応用編）── 締め括りとして、λProlog を支える８つの概念の整理、コード実例、実務で威力を発揮するユースケース、他の定理証明系との使い分け、日本と世界での認知度、学習リソース、対話篇、まとめ、と続きます。

本文の各見出しには「基礎編」「節 1〜5」「応用編」のラベルを付けてあるので、いまどの部を読んでいるのかは、見出しを見ればいつでも分かります。

なお本記事は λProlog の文法を細部まで解説する記事ではありません。文法の詳細は、記事の終盤の「学習リソース」の節で紹介する一次情報に譲ります。

先行記事と姉妹記事

本記事は単独で読めます。
前提として読んでおくべき記事はありません。

関連する記事は次のとおりです。

• 先行記事 ── 論理プログラミングは終わらなかった ── 第五世代コンピュータから LLM / AI Agent / MCP Solver へ。Prolog と現代のクラウド技術の関係を扱っており、本記事の背景理解が深まります
   
• 姉妹記事 ── F*（F Star） とは何か ── Firefox・Linux・WireGuard で動く「証明済みコード」を書けるプログラミング言語の早わかり。「証明済みコードを実務システムに直接組み込む」という、λProlog とは別の切り口の言語を紹介しています
   
• 続編（公開予定）── 実装である ELPI と Coq-Elpi のメタプログラミング実務を掘り下げる姉妹記事を、本記事の次に公開する予定です

想定読者

• これまでプログラミング言語は Python だけを使ってきたエンジニア
   
• 論理型プログラミング、高階論理、単純型付きラムダ計算を学ぶ機会がなかった方
   
• Prolog という名前は聞いたことがあるが、詳しく触れる機会がなかった方
   
• 定理証明系（Rocq、Lean 4、Isabelle、Agda など）を学んだことがない方
   
• AI と定理証明系の接点に関心のある方
   
• メタプログラミング（プログラムを操作するプログラム）の世界に関心のある方

前提知識は必要ありません。論理型プログラミング、高階論理、高階抽象構文（HOAS）、Constraint Handling Rules（CHR）、メタプログラミングといった概念は、登場するたびに本文の中で説明します。

この記事を読む価値

1. Prolog と λProlog は何が違うのかが分かるようになる
    
2. 高階抽象構文（HOAS）とは何か、この技法で何ができるようになるのかが分かるようになる
    
3. λProlog の実装である ELPI が、Rocq の Coq-Elpi、mathcomp の Hierarchy Builder、対話的定理証明系 Abella、プログラミング言語理論の Makam などでどう使われているかが分かるようになる
    
4. AI 時代における λProlog の位置付けと、AI × 定理証明のイメージを持てるようになる
    
5. なぜ λProlog が生まれたのか、その歴史的な経緯と学術的な動機が分かるようになる
    
6. 世界各国での λProlog の存在感（欧米、中国、ロシア、韓国、インド、イスラエル、日本）の全体像がつかめるようになる

TL;DR

（この節に登場する専門用語はいずれも本文の中で説明します。ここでは全体像だけつかんでください）

• λProlog は、1987 年に Dale Miller と Gopalan Nadathur が発表した、Prolog を高階論理と単純型付きラムダ計算で拡張した論理型プログラミング言語です。「高階抽象構文（HOAS、Higher-Order Abstract Syntax）による束縛変数の自然な扱い」と「型システムの導入」が Prolog との根本的な違いです。
   
• λProlog が生まれた動機は「プログラミング言語や論理体系の意味論（プログラムや論理式が何を意味するかの厳密な定義）を、機械的に扱えるプログラミング言語を作ろう」というものでした。プログラミング言語の型検査、コンパイラの中間表現、証明支援系の内部データ構造 ── これらはいずれも「変数の束縛を含む構文木（プログラムの構造を木の形で表したデータ）」を機械的に操作する必要があり、Prolog ではこの束縛の扱いが不自然でした。λProlog はこの難問を正しく自然に解く言語として設計されました。
   
• λProlog の主要な実装である ELPI は、2015 年に Cvetan Dunchev、Ferruccio Guidi、Claudio Sacerdoti Coen、Enrico Tassi が発表しました。OCaml で書かれ、他のアプリケーションに組み込むこと（embed）を目的に設計されており、λProlog 標準に Constraint Handling Rules（CHR、制約処理規則）を加えた方言です。
   
• λProlog/ELPI の主要な実務での用途は、Rocq（旧 Coq）の拡張言語 Coq-Elpi です。Rocq のタクティク、コマンド、そして代数構造の階層（mathcomp を支える Hierarchy Builder）といった Rocq 自身のメタプログラミングが ELPI で書かれています。この他、プログラミング言語の意味論の証明系 Abella（Miller、Nadathur、Gacek ら）、プログラミング言語理論の実装向け Makam（Antonis Stampoulis）などの利用があります。
   
• AI 時代における λProlog の学習価値は高いと考えられます。Coq-Elpi は Rocq と AI を橋渡しする「タクティクの記述言語」として機能します。AI が生成するコードやタクティクを λProlog の型システムと高階論理の力で厳密に検証する場面で、λProlog は独特の強さを発揮します。

λProlog の一次情報源

λProlog についての一次情報は以下の場所で公開されています。

• 公式サイト ── https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/ （Dale Miller 氏が管理）
   
• 主要な実装である ELPI の GitHub リポジトリ ── https://github.com/LPCIC/elpi （最新版 v3.7 は 2026 年 4 月 24 日にリリース）
   
• もう一つの主要な実装である Teyjus（テイジャス）の GitHub リポジトリ ── https://github.com/teyjus/teyjus （最新版 v2.1.1 は 2023 年 2 月 8 日にリリース。Gopalan Nadathur 氏が主導、ミネソタ大学、OCaml で実装）
   
• Rocq プラグイン Coq-Elpi の GitHub リポジトリ ── https://github.com/LPCIC/coq-elpi
   
• Abella（アベラ）公式サイト ── https://abella-prover.org/
   
• Makam（マカム）公式サイト ── https://astampoulis.github.io/makam/
   
• 公式書籍*"Programming with Higher-Order Logic"*（Dale Miller、Gopalan Nadathur 共著、2012 年、Cambridge University Press）── λProlog の理論と実装の決定版
   
• Dale Miller 氏のホームページ ── https://www.lix.polytechnique.fr/Labo/Dale.Miller/
   
• λProlog 英語版 Wikipedia ── https://en.wikipedia.org/wiki/%CE%9BProlog
   
• 主要学術論文 ── "A logic programming approach to manipulating formulas and programs"（Miller・Nadathur、1987 年）、"Uniform Proofs as a Foundation for Logic Programming"（Miller・Nadathur・Pfenning・Scedrov、ICLP 1988）、"ELPI: fast, Embeddable, λProlog Interpreter"（LPAR 2015）、"Elpi: an extension language for Coq"（Tassi、2018 年）、"Hierarchy Builder"（Cohen・Sakaguchi・Tassi、FSCD 2020）

---

基礎編 その 1 ── まず「論理プログラミング」と Prolog を知る

論理プログラミングとは何か

Python でプログラムを書くときは、コンピュータにやってほしい手順を一つずつ指示します。「この値を受け取る。計算する。結果を返す」という手順の連なりがプログラムです。

論理プログラミングは発想がまったく違います。手順を書きません。
書くのは次の２つだけです。

• 事実と規則 ──「何が成り立っているか」
• 質問 ──「何を知りたいか」

答えを探す仕事は、コンピュータに任せます。

具体例で見てみましょう。

次の２つの事実と１つの規則を考えます。

• 事実 1 ：次郎は太郎の父である
• 事実 2 ：三郎は次郎の父である
• 規則 ：$X$ が $Y$ の父で、$Y$ が $Z$ の父ならば、$X$ は $Z$ の祖父である

ここに「太郎の祖父は誰か？」と質問すると、コンピュータは事実と規則を自動的に組み合わせて「三郎です」と答えてくれます。

書き手は探し方の手順を一行も書いていません。これが論理プログラミングです。

Prolog ── 論理プログラミングの代表格

この発想を最初に形にした言語が Prolog（プロログ）です。

1972 年にフランスのマルセイユ大学で Alain Colmerauer と Philippe Roussel が開発しました。
名前は Programming in Logic（論理によるプログラミング）に由来します。

先ほどの家系図の例は、Prolog では次のように書きます。

father(jiro, taro).      % 次郎は太郎の父である（事実）
father(saburo, jiro).    % 三郎は次郎の父である（事実）

% X が Y の父で、Y が Z の父ならば、X は Z の祖父である（規則）
grandfather(X, Z) :- father(X, Y), father(Y, Z).

そして質問を投げます。

?- grandfather(G, taro).   % 太郎の祖父 G は誰か？
G = saburo.                % 答え：三郎

ここで father や grandfather のような部品を 「述語（じゅつご、predicate）」 と呼びます。
この言葉は本記事を貫く最重要語なので、しっかりと説明しておきます。

国語の授業で習った「主語と述語」を思い出してください。

「太郎は学生である」という文の「── は学生である」の部分が述語でした。

論理学の述語 もこれと同じ発想で、一言でいえば 「穴あきの文」 です。

• 「 __ は偶数である」── 穴が１つの述語。穴に $4$ を入れれば真、$7$ を入れれば偽になる
• 「 __ は __ の父である」── 穴が２つの述語。（次郎, 太郎）の順で入れれば真、（太郎, 次郎）なら偽になる

穴をぜんぶ埋めると、真か偽かが決まる文になる ── これが述語です。

Python でいえば def is_even(x): return x % 2 == 0 のような真偽を返す関数がちょうど述語にあたり、関数の引数が 「穴」に対応 します。

先ほどのコードの father(jiro, taro) は、「__ は __ の父である」という２つ穴の述語に次郎と太郎を入れた文だった、というわけです。

また grandfather(X, Z) :- father(X, Y), father(Y, Z). のような「$A$ かつ $B$ が成り立つならば $C$ が成り立つ」という形の式を**「Horn 節（ホーン節）」**と呼びます。

米国の論理学者 Alfred Horn（1918-2001、UCLA）が 1951 年に提案した形式です。

Prolog のプログラムとは、つまるところ Horn 節の集まりです。

同じことを Python で書くと ── 言語に何を任せているのかが見える

Prolog が何を肩代わりしてくれているのかを実感するために、同じ「祖父探し」を Python で書いてみます。

facts = {("jiro", "taro"), ("saburo", "jiro")}   # (父, 子) の集合

def grandfather(z):
    """z の祖父を探す"""
    for (x, y1) in facts:          # x は y1 の父
        for (y2, z2) in facts:     # y2 は z2 の父
            if y1 == y2 and z2 == z:
                yield x

print(list(grandfather("taro")))   # ['saburo']

Python では、「事実の集合を二重ループで総当たりし、つなぎ目（y1 == y2）を自分で照合する」という探索の手順を書き手が全部書いています。

Prolog版で書いたのは規則１行だけでした。
探索も照合も言語側の仕事だったわけです。

もう一つ大きな違いがあります。

Python の grandfather(z) は「孫を渡すと祖父が返る」一方向の関数です。
ところが Prolog の grandfather(X, Z) は関係なので、同じ１行のまま逆向きにも使えます。

?- grandfather(saburo, W).   % 三郎の孫 W は誰か？（さっきと逆向きの質問）
W = taro.

Python で逆向きが必要になったら関数をもう１つ書くところです。
関係を書けば質問の向きは自由 ── これが論理プログラミングの気持ちよさです。

Prolog は ISO 規格として標準化されており、SWI-Prolog、GNU Prolog、SICStus Prolog などの実装があります。

1980 年代には日本の国家プロジェクト「第五世代コンピュータ」の中核言語にも選ばれました。

Prolog と現代のクラウド技術（AWS Cedar、Neo4j Cypher、Datalog など）との関係は、「論理プログラミングは終わらなかった ── 第五世代コンピュータから LLM / AI Agent / MCP Solver へ」（2026 年 5 月 19 日公開）で論じで論じました。

よろしければ併せてご覧ください。

コンピュータはどうやって答えを見つけるのか

Prolog の推論エンジンは２つの基本操作を組み合わせて答えを探します。

１つ目は**「単一化（たんいつか、unification）」** です。

２つの式の形を突き合わせて、まだ決まっていない変数に入るべき値を見つける操作です。

たとえば grandfather(G, taro) という質問と規則の頭部 grandfather(X, Z) を突き合わせると、「G と X は同じもの、Z は taro」という対応が見つかります。

Python の辞書でいえば {"name": "太郎", "age": 30} と {"name": X, "age": 30} を見比べて X = "太郎" と決めるようなものです。

２つ目は**「バックトラック（backtracking）」**です。

ある選択で行き詰まったら、直前の分かれ道まで戻って別の選択を試す動き方です。

迷路を解くときに、行き止まりに突き当たったら分岐点まで引き返すのと同じ発想です（アルゴリズムでいう深さ優先探索にあたります）。

「単一化で式を照合し、失敗したらバックトラックで戻る」
── この繰り返しが、論理プログラミングの心臓部 です。

実際に、先ほどの「太郎の祖父は誰か？」に Prolog が答えるまでの動きを一歩ずつ追ってみます。

質問: grandfather(G, taro)

手順 1  規則の頭 grandfather(X, Z) と質問を単一化
        → X = G、Z = taro と決まる
手順 2  規則の本体が残りの課題になる
        → father(G, Y) かつ father(Y, taro) を満たせばよい
手順 3  father(G, Y) を事実と照合。最初の候補は father(jiro, taro)
        → G = jiro、Y = taro と仮に決める
手順 4  すると father(taro, taro) が必要になる
        → そんな事実は無い。失敗
手順 5  バックトラック。手順 3 に戻り、次の候補 father(saburo, jiro) を試す
        → G = saburo、Y = jiro
手順 6  すると father(jiro, taro) が必要になる
        → 事実にある。成功！

答え: G = saburo（三郎）

「仮に決めて進み、行き詰まったら戻って別の候補を試す」
── コンピュータがこの試行錯誤を自動でやってくれるので、書き手は事実と規則だけ書けばよい のです。

基礎編 その 2 ── λProlog は、Prolog をどう拡張した言語なのか

Prolog が分かったところで、本記事の主役に進みます。

λProlog は、1987 年に Dale Miller（当時 University of Pennsylvania、現在 INRIA & LIX/École polytechnique）と Gopalan Nadathur（当時 Duke University、現在 University of Minnesota）が発表した言語です。

読み方は 「ラムダ・プロログ」、英語では Lambda Prolog です。

一言でいえば、λProlog は 「Prolog を、高階論理と単純型付きラムダ計算という２つの数学的な道具で強化した言語」 です。

この２つの道具を順に説明します。

道具 1 ── 高階論理

まず、Prolog の節で説明した「述語 = 穴あきの文」を思い出してください。

「__ は偶数である」「__ は __ の父である」のように、穴をぜんぶ埋めると真偽が決まる文が述語でした。

論理の世界には、穴を一つずつ値で埋める代わりに、「すべての〜について、…が成り立つ」「ある〜が存在して、…が成り立つ」とまとめて述べる言い回し があります。

これを 「量化（りょうか）」 と呼び、「すべての」「ある」を表す記号 を 「量化子」 と呼びます。

ここからが本題です。

一階と高階を分けるのは、たった一つの問いです
── 穴に入れてよいもの、「すべての」と言ってよいものは、何か？

一階論理（いっかいろんり）の答えは「モノだけ」です。

人、数値、文字列のような具体的な対象だけが、穴に入り、量化の対象になれます。

• 「すべての整数 x について、x + 0 = x が成り立つ」── x はモノ（数）。一階で書ける
• 「すべての人 p について、p には父がいる」── p はモノ（人）。一階で書ける
• 「ある整数 x が存在して、x × x = 4 が成り立つ」── これも一階で書ける

Prolog が扱えるのは、この一階論理です。

**高階論理（こうかいろんり）の答えは、「述語や関数そのものも入れてよい」**です。
すると、文についての文、性質についての文が書けるようになります。

具体例を２つ見てください。

例１ ──「対称的である」という述語

「friend（友だち）という関係は対称的だ。
$A$ が $B$ の友だちなら $B$ も $A$ の友だちだから。

でも father（父）という関係は対称的ではない」

── 私たちは日常でもこういう文を使います。

よく見ると、この文の主語は人ではなく、friend や father という関係そのものです。

きちんと書き下すとこうなります。

「関係 $R$ が対称的であるとは、すべての $x$ と $y$ について、$R(x, y)$ ならば $R(y, x)$ が成り立つこと」

穴 $R$ に入っているのは述語です。

つまり「対称的である」は、述語を穴に取る述語 ── 一段上の述語です。

一階論理には $R$ を量化する手段が無いので、この定義そのものが書けません。

例２ ── 数学的帰納法

「どんな性質 $P$ についても、$P$ が $0$ で成り立ち、『$n$ で成り立つなら $n + 1$ でも成り立つ』が言えるなら、$P$ はすべての自然数で成り立つ」

これは数学の証明の根幹をなす帰納法の原理です。

冒頭が「どんな性質 $P$ についても」── 性質（述語）についての量化 ── で始まっていることに注目してください。

帰納法の原理は生まれつき高階の文であり、一階論理では一つの文として書き下せません。

定理証明の世界で高階論理が必要とされる理由が、早くもここに顔を出しています。

λProlog が扱えるのは、この高階論理 です。

Python の高階関数との関係

「高階」という言葉には、見覚えがあるかもしれません。

Python では、関数を引数として受け取る関数や、関数を返り値として返す関数を「高階関数」と呼びます。

sorted(["banana", "apple", "fig"], key=len)   # 関数 len を引数として渡す
map(str.upper, ["a", "b"])                    # 関数 str.upper を引数として渡す

def make_adder(n):                            # 関数を返り値として返す関数
    return lambda x: x + n

高階関数とは「関数を数値やリストと同じ値として受け渡しできる関数」のことでした。

高階論理はその論理版で、「述語や関数を、モノと同じ扱いで穴に入れたり量化したりできる論理」です。

対応を表にします。

Python の世界	論理の世界
値（数値、リスト、文字列）	モノ（人、数）
関数	述語・関数
高階関数 ── 関数を引数や返り値にできる	高階論理 ── 述語や関数を穴に入れ、量化できる

どちらの「高階」も意味は同じで、「一段上のものまで対象にできる」ということです。
「階（order）」は語る対象の段数を表します。

モノについて語るのが一階、"モノについて語る述語"について語るのが二階
── 二階以上を、まとめて高階と呼びます。

書物によっては「一階述語論理」という表記も見かけますが、「一階論理」と同じものです（述語と量化を備えた論理を「述語論理」と呼び、その一階版・高階版という意味です）。

同様に「高階述語論理」と「高階論理」も同じ概念を指します。
本記事では短い「一階論理」「高階論理」で統一します。

道具 2 ── 単純型付きラムダ計算

もう１つの道具は「単純型付きラムダ計算（simply typed lambda calculus）」です。1940 年に Alonzo Church（米国 Princeton 大学。コンピュータ・サイエンスの理論的基礎を築いた数学者の一人）が提案した体系で、一言でいえば「型のついた関数を数学として厳密に扱うための体系」です。

言葉を分解しましょう。

「ラムダ」とは、名前をつけずにその場で関数を書く記法のことです。Python の lambda x: x + 1 の lambda は、まさにこの体系に由来しています。数学の記法では λx. x + 1 と書き、これを「ラムダ抽象」と呼びます。

「型」とは、値の種類の約束事です。Python の型ヒント def add(x: int, y: int) -> int: が表す「整数を 2 つ受け取り整数を返す」という約束が、型です。

つまり単純型付きラムダ計算とは、「lambda 式と型ヒントの世界を、数学として整えたもの」です。Haskell や OCaml といった「関数型プログラミング言語」── 計算を関数の組み合わせとして書き表す流儀の言語群 ── の型の理論は、すべてこの体系を源流としています。

この２つの道具で、何ができるようになるのか

Prolog には、実務で使い込むほど痛感される２つの弱点がありました。

弱点 １ ── 型がない。述語の引数にどんな種類の値が来るべきかを宣言できず、間違いが実行時まで見つからない。

この弱点をコードで見てみます。

Prolog では次のような明らかにおかしな事実も、文句を言わずに受け入れられてしまいます。

father(jiro, taro).
father(42, taro).      % 「42 は太郎の父」!? Prolog は素通しする

数値の $42$ が人の名前の場所に紛れ込んでも、Prolog は何も警告しません。

バグは実行時に変な答えが出るまで潜伏します。
Python で型ヒントも検査も無しに書いているときと同じ状況です。

同じ内容を λProlog（ELPI の構文）で書くと、型の宣言が加わります。

kind person type.                       % 「person という型がある」と宣言
type taro, jiro, saburo person.         % 太郎・次郎・三郎は person 型の値
type father person -> person -> prop.   % father は person を 2 つ受け取る述語

father jiro taro.
father saburo jiro.

% father 42 taro.
%   ↑ 42 は person 型ではないので、実行する前の段階で型エラーとして弾かれる

kind が型の宣言、type が値や述語の型づけです。

father person -> person -> prop は「father は person を 2 つ受け取ると、真偽が決まる文（prop）になる」という意味で、Python の型ヒント def father(x: Person, y: Person) -> bool: に相当します。

違いは、λProlog ではこの型が実行前に必ず検査されることです。

弱点 ２ ──「束縛変数」をうまく扱えない。

「束縛変数（そくばくへんすう）」は本記事の最重要語なので、ここで丁寧に説明します。

「すべての $x$ について、$x + 0 = x$ が成り立つ」という文の $x$ は、この文の中でだけ意味を持ちます。

文の外に出れば $x$ は何も指しません。

このように、ある式の中でだけ意味を持つように縛られた変数を束縛変数と呼びます。

Python の関数の引数 x が、その関数の中でだけ意味を持つのと同じ構図です。

なぜ束縛変数が問題になるのでしょうか。

プログラムや数学の論理式を、データとして機械に読み書きさせたい場面があるからです。

"プログラムを読み書きするプログラム" を 書くことを、「メタプログラミング」 と呼びます。

不思議な響きですが、種を明かせば単純な話です。

プログラムのソースコードは、ただのテキスト（文字の並び）です。

そして文字の並びなら、別のプログラムから読んだり書き換えたりできます。

「プログラムを、操作の対象となるデータとして扱う」
── これがメタプログラミングです。

実は、プログラミングを始めたばかりの人でも、毎日その恩恵を受けています。

エディタ（VS Code など）がコードに色を付けたり、間違いの箇所に赤い波線を引いたりできるのは、エディタというプログラムが、あなたの書いたコードをデータとして読み込んで解析しているからです。

ChatGPT のような AI がコードを読んで修正案を返してくれるのも、Python を実行するソフトウェアがあなたの書いた .py ファイルを読み込んで動かすのも、ぜんぶ 「プログラムを読み書きするプログラム」
── メタプログラミングの仲間です。

そして、メタプログラミングの対象になるプログラムや論理式には、束縛変数 が必ず含まれます。

理由は単純です。

関数を１つも含まないプログラムは実際ほとんど無く、関数には必ず引数
── その関数の中でだけ意味を持つ変数、つまり束縛変数 ──
があるからです。

数学の論理式も同じで、「すべての $x$ について」を含まない命題はまれです。

束縛変数が含まれると、それを読み書きする側には厄介な仕事が発生します。

身近な例を挙げましょう。

エディタの「変数名の一括変更」機能を使ったことはないでしょうか。

変数 $x$ の名前を $y$ に変えるとき、エディタは「この $x$ はどの関数の引数なのか」「たまたま同じ名前なだけの、別の関数の中の $x$ を巻き込んでいないか」を正しく見分けなければなりません。

ここを間違えれば、プログラムは壊れます。

この**「同じ名前でも別物かもしれない変数を、取り違えずに扱う」仕事こそが、束縛変数の管理** です。

つまり、プログラムや論理式をデータとして読み書きし始めた瞬間 ── メタプログラミングを始めた瞬間 ── 束縛変数の管理からは逃げられなくなる のです。

ところが Prolog の一階論理では、この「束縛変数を含むデータ」を正しく扱えませんでした。
なぜでしょうか。

思い出してください。

一階論理とは、穴に入れられるのも「すべての」と言えるのもモノだけの論理でした（「対称的である」のような、述語を主語にした文は書けません）。

この世界でデータとして持てるのは、father(jiro, taro) のような「モノの名前を組み合わせた式」だけです。

関数そのものをデータとして持つ道具立てが、そもそも存在しない のです。

それでも Prolog で「$x$ を受け取って $x + 1$ を返す関数」（ ラムダ記法 で $λx. x + 1$ ）をデータとして持ちたい としたら、どうするか。

苦肉の策は２つあります。そしてどちらも失敗します。

苦肉の策 1 ── 変数を、ただの記号（名前）として持つ

% λx. x + 1 を lambda(記号, 本体) というデータで表してみる
Term1 = lambda(x, plus(x, 1)).
Term2 = lambda(y, plus(y, 1)).

Term1 と Term2 は、変数の名前が違うだけで中身は同じ関数のはずです。

ところが Prolog にとって $x$ と $y$ はただの別々の記号なので、この２つは「違うデータ」と判定されます。

「名前が違っても同じ関数」という、束縛変数のいちばん大事な性質（後の節で $α$ 変換 として登場します）を、機械が知らない のです。

同じ扱いにしたければ、名前の付け替えの処理を書き手が延々と自作することになります。

苦肉の策 2 ── Prolog 自身の変数を流用する

「Prolog にも変数（大文字の $X$）があるじゃないか」と思うかもしれません。試してみます。

?- T = lambda(X, plus(X, 1)), X = 3.
T = lambda(3, plus(3, 1)).     % 束縛変数のはずの X が 3 で埋まり、関数が壊れた

Prolog の変数 $X$ は**「単一化でこれから値が埋まる未知数」** です。

一方、表したかったのは「関数の中でだけ意味を持つ束縛変数」です。

この２つは、見た目が似ているだけの別物です。

未知数はいつか値で埋まるのが仕事なので、単一化が走った瞬間に $X$ は $3$ で埋まり、「$x$ を受け取る関数」だったはずのデータは「$3$ の入った式」に壊れてしまいました。

まとめると、Prolog の一階論理には「束縛変数」という概念を表す正しい置き場所がそもそも無い
── 記号で代用すれば同一性が壊れ、未知数で代用すれば単一化に食われる。

これが「正しく扱えなかった」の中身 です。

λProlog はこの問題を、２つの道具を組み込むことで根本から解決しました。

どう解決したのかを順に見ます。

解決の鍵 １ ── 単純型付きラムダ計算が、「本物の関数」を言語の部品にする

単純型付きラムダ計算 とは、先ほど説明したとおり「lambda 式と型ヒントの世界を数学として整えた体系」でした。

λProlog はこの体系を言語の土台に採用したので、ラムダ抽象 ── 名前をつけずにその場で書く関数 ── が、言語の正式な部品になっています。

すると λx. x + 1 は、もはや記号の寄せ集めでも壊れやすい未知数入りの式でもなく、λProlog 自身の「本物の関数の値」として書けるようになります。

% λProlog では、言語自身のラムダ抽象(バックスラッシュ記法)でそのまま書ける
% （plus は「足し算」、one は「1」を表す記号です。本記事の説明用に用意しました）
F = (x \ plus x one)

ここが急所です。

λProlog は、**ラムダ抽象の名前の付け替え（x \ ... と y \ ... を同一視する）**や、値のあてはめ（代入）を言語の内部で正しく処理する仕組みを最初から備えています。

束縛変数を「本物の関数」として持てば、その面倒な管理はぜんぶ言語の既存の仕組みが引き受けてくれる
── 書き手が自作する必要が消えるのです。

解決の鍵 2 ── 高階論理が、その「関数の値」を推論の土俵に乗せる

ただし、関数を値として書けるだけでは足りません。

書いた関数を使って推論できなければ、メタプログラミングにならないからです。

具体的に述べます。

上のコードでは、変数 $F$ に関数 (x \ plus x one) がそのまま入りました。

Python でいえば f = lambda x: x + 1 と、関数を変数に代入した状態です。
メタプログラミング では、ここからさらに次のようなことをやりたくなります。

% 関数 F を受け取り、X に F を 2 回適用した結果が R である、という述語
% （father のときのような型宣言は、話を簡単にするため省略しています）
twice F X (F (F X)).

この１行では、述語 twice の引数に関数 $F$ が渡され、本体では $F$ が 2 回適用されています。

Python の def twice(f, x): return f(f(x)) にあたる高階関数です。

しかも λProlog なら「この規則は、どんな関数 $F$ についても成り立つ」と、関数を相手にした量化として読めます。

• 述語の引数に関数を渡す。
• 変数に関数を入れる。
• 関数について「すべての」と語る

── これらを許す論理が、道具１で見た高階論理そのものです。

逆に一階論理のままだと、せっかくラムダ抽象で関数を書けても、それを述語に渡すことも量化することもできません。

高階関数の無い Python を想像してみてください。

lambda 式は書けるのに、map にも sorted の key にも渡せず、変数にも代入できない
── 書けるだけで使えない、宝の持ち腐れです。

だから高階論理とラムダ計算は二つで一組なのです。

そして型にはもう一つの役割があります。

関数まで含めた照合（単一化）は、野放しにすると候補が爆発するのです。

たとえば、「$F$ に何かを渡した結果が $1$ になる。そんな関数 $F$ を探せ」と機械に頼んだとします。

候補は無限にあります。

• 何を受け取っても $1$ を返す関数。
• 受け取ったものをそのまま返す関数（引数として $1$ を渡した場合）。
• 受け取った数を２倍してから $1$ を引く関数（引数として $1$ を渡した場合）
• ……。

単純型付きラムダ計算の型が、「$F$ は数から数への関数」「この変数は person」と探索の範囲を区切ってくれるからこそ、機械はこの照合を現実的にこなすことができるのです。

型は弱点１（型が無い） への答えであると同時に、関数まで扱う世界の交通整理役でもあるわけです。

こうして λProlog では、型は言語に備わり、束縛変数はラムダ抽象の力で自然に扱えるようになりました。

この 「束縛変数の管理を、言語自身のラムダ抽象に委ねる」という仕掛け には名前がついています。

それが、後の節3（HOAS） で 主役として登場する高階抽象構文（HOAS） です。

基礎編 その３ ── 定理証明系：数学の証明を機械が支える仕組み

λProlog の姿が見えてきたところで、この言語が実際に働いている現場、「定理証明系」の世界 に進みます。

この記事の冒頭で触れた**「AI が数学の定理を証明する」話の本体** です。

予備知識ゼロの前提で、言葉の意味から説明します。

定理と証明

数学でいう「定理」とは、正しいことが証明された主張のことです。
「どんな整数 $x$ についても $x + 0 = x$ が成り立つ」は一つの定理です。

「証明」 とは、その主張が正しいことを、あらかじめ認められた推論の規則だけを使って一歩ずつ示した道筋のこと です。

「$A$ が成り立つ。$A$ ならば $B$ である。ゆえに $B$ が成り立つ」という具合に、飛躍のない小さな一歩を積み重ねて目標の主張までたどり着きます。

それを機械が担うと、どうなるか

「数学の定理の自動証明」とは、この営みをコンピュータに担わせることです。

この仕事は２種類に分かれます。

１つ目は、証明の検査です。

人間や AI が書いた証明を機械が読める形式のデータで表現し、「一歩一歩が本当に認められた規則どおりに進んでいるか」をコンピュータが確かめます。

検査に通った証明には、飛躍もごまかしも一切ないと言い切れます。

２つ目は、証明の探索 です。

すでに分かっている事実と推論の規則を組み合わせて、目標の主張にたどり着く道筋をコンピュータ自身に探させます。

── ここで、先ほどの Prolog の説明を思い出してください。

「事実と規則を書いておくと、コンピュータが答えへの道筋を探してくれる」のが論理プログラミングでした。

証明の探索とは、まさにこの仕事の形そのもの です。

**論理プログラミングの言語が定理証明の世界で重宝される理由が、ここにあります。}}

小さな体験 ── Prolog で「2 + 2 = 4」の証明を探索してみる

「証明の探索は論理プログラミングそのもの」という話を、実際に動くコードで体験してみましょう。足し算の規則だけを Prolog に教えて、「2 + 2 = 4」を機械に証明させてみます。

まず自然数を、0 を表す z と「1 つ次の数」を表す s(...) で表します。1 は s(z)、2 は s(s(z))、4 は s(s(s(s(z)))) です。原始的に見えますが、数学の証明の世界ではこの表し方（ペアノの自然数と呼ばれます）が標準です。

足し算の規則は 2 行で書けます。

plus(z, N, N).                          % 規則 1: 0 + N = N
plus(s(M), N, s(P)) :- plus(M, N, P).   % 規則 2: (M+1) + N = (M+N) + 1

plus(A, B, C) は「A + B = C が成り立つ」という述語です。規則 1 は「0 に何を足してもその数のまま」、規則 2 は「(M+1) + N を知りたければ、まず M + N を求めて 1 を足せばよい」と読めます。

ここで質問します。「2 + 2 は何か？」

?- plus(s(s(z)), s(s(z)), X).
X = s(s(s(s(z)))).            % 答え: 4

Prolog の推論エンジンは、規則２を２回適用して規則１にたどり着く道筋を探索し、答えを見つけました。

この $「規則 2 → 規則 2 → 規則 1」$という道筋こそが、まさに「$2 + 2 = 4$ の証明」です。

答えの計算と証明の探索が同じものだった
── これが、「計算とは証明の探索である」 という節 1（歴史）で登場する Uniform Proofs の考え方の入り口 です。

おまけに、質問を逆向きにもできます。
「足して $2$ になる組み合わせは？」

?- plus(X, Y, s(s(z))).
X = z,       Y = s(s(z)) ;    % 0 + 2 = 2
X = s(z),    Y = s(z) ;       % 1 + 1 = 2
X = s(s(z)), Y = z.           % 2 + 0 = 2

「答えから問いを探す」ことまで同じ２行の規則でできてしまう
── 定理証明の世界で論理プログラミングが愛される理由を、この小ささが物語っています。

この 「証明を検査したり探したりするソフトウェア」 を、定理証明系（または証明支援系） と呼びます。

代表的なものに Rocq（ロックと読みます。2023 年までは Coq ／コックという名前でした）、Lean 4、Isabelle、Agdaなど があります。

もう一つ、この先で繰り返し登場する言葉をここで押さえておきます。

定理証明系で、証明を一手ずつ前に進めるための指示のことを「タクティク（tactic）」と呼びます。

将棋の一手のように、タクティクを積み重ねて証明を組み上げていきます。
（実際の使い方は後の節でコードとともに見る機会を設けさせていただいております）

なぜ今、注目されているのか

冒頭で述べたとおり、大規模言語モデルに証明の候補を生成させ、定理証明系で厳密に検査するという組み合わせが、2024 年以降急速に伸びています。

LLMの発想力と、機械検査の確実さを組み合わせる わけです。

AlphaProof（Google DeepMind） や DeepSeek-Prover はその代表例です。

LLM の出力は、それ単体では「たぶん正しい」止まりです。

しかし定理証明系の検査を通れば「間違いなく正しい」に変わります。

この橋渡しの仕組みが、AI 時代の重要な研究領域になっている のです。

基礎編 その 4 ── ELPI：λProlog の実装であり、Rocq の中で働く現役の処理系

最後の登場人物が ELPI（エルピーと読みます。Embeddable Lambda Prolog Interpreter の略）です。

ELPI は 2015 年に、Cvetan Dunchev、Ferruccio Guidi、Claudio Sacerdoti Coen（ボローニャ大学）と Enrico Tassi（INRIA）が発表した、λProlog の高速な実装 です。

「実装」とは、言語の仕様どおりにプログラムを実際に動かすソフトウェアのことです。P
ython でいえば、Python という言語仕様に対する CPython のような関係です。

ELPI は OCaml（オキャムル。関数型プログラミング言語の一つ）で書かれており、名前のとおり 「他のアプリケーションに組み込む（embed する）」ことを目的に設計 されています。

なお ELPI にはブラウザ上で動く Elpi Playground が公開されているので、何もインストールせずに λProlog のコードを試せます（本記事のコード例を写して動かしてみるのに便利です）。

そして、ELPI の最大の活躍の場が、まさに定理証明系 Rocq の内側です。

ELPI は、 Coq-Elpi（コック・エルピー）という拡張機能として Rocq に組み込まれ、証明の自動化を担う正式な拡張言語として 日夜働いています。

「AI が生成した証明の断片を、Rocq に渡す前に厳密に検査する」という AI 時代の橋渡し役も、この位置から担っていくシナリオが考えられます。

基礎編のまとめ ── Prolog・λProlog・ELPI の関係

３者の名前はしばしば混同されるので、関係を整理しておきます。

• Prolog は、論理型プログラミングの大元の言語
   
• λProlog は、その Prolog を高階論理と単純型付きラムダ計算で拡張した言語
   
• ELPI は、その λProlog の現代的な実装の一つ（λProlog 標準に Constraint Handling Rules〈制約処理規則。後の節で説明します〉などの独自拡張を加えているため、厳密には「λProlog の方言」と呼ぶのが正確です）

本記事では、言語仕様の話題では λProlog を、実装や実務での使われ方の話題では ELPI を、それぞれ主題として扱います。

基礎編の補足 ── Python と λProlog

Python と λProlog の発想の違いを一枚の表で整理します。

観点	Python	λProlog
プログラミング・スタイル	命令型（処理の手順を一つずつ書く）	論理型（事実と規則を書き、コンピュータが答えを探索）
プログラムの単位	関数、クラス、モジュール	述語（真偽が決まる関係）と論理式
制御の流れ	書き手が明示的に指示	推論エンジンが自動的に決定
変数の扱い	値の入れ物として使う	論理変数（まだ値が決まっていない未知数）として使う
論理の階層	適用外	高階論理（関数や述語も変数にできる）
束縛変数の扱い	適用外	高階抽象構文（HOAS）で自然に扱える
典型的な用途	Web アプリ、業務システム、データ分析	定理証明系の内部、プログラミング言語の意味論の実装、メタプログラミング

表の中の「高階抽象構文（HOAS）」は節 3（HOAS） で、「意味論」は節 1（歴史） で説明します。

ここでは「Prolog が苦手だった変数の扱いを λProlog はうまく扱える」という対比だけ頭の片隅に置いてください。

Python は「何をどうやるかを指示する言語」です。

それに対して、λProlog は「何を知っていて何を求めたいかを教える言語」です。

この違いは実務のどこで効いてくるのでしょうか。

前の節で見たとおり、定理の証明とは「分かっている事実と推論の規則を組み合わせて、目標の主張への道筋を探す」営み です。

手順を指示する Python 流よりも、「事実と規則を書けば道筋は機械が探す」という λProlog 流 の方が、この仕事の形に要領よく重なるのです。

λProlog が Rocq の内側で証明自動化を担う言語に選ばれた背景には、この一致があります。
（詳しくは節 5（AI との接点） で扱います）

---

節１（歴史）── なぜ λProlog が生まれたのか

Prolog の誕生（1972 年、フランス・マルセイユ）

λProlog の物語は、その 15 年前のフランスから始まります。

1972 年、マルセイユ大学の Alain Colmerauer（アラン・コルメロエル）と Philippe Roussel が最初の Prolog を開発しました。理論的な土台になったのは、英国の Robert Kowalski（ロバート・コワルスキ、当時 Edinburgh 大学）による「論理を計算のモデルとして使う」というアイデアです。

Prolog という名前は、フランス語の「PROgrammation en LOGique（論理によるプログラミング）」の頭文字から取られています。

Prolog が世に問うた発想は、記事の前半で見たとおりです。「プログラマはコンピュータに『どう計算せよ』と命令しなくてよい。『何が真で、何が求めたい答えか』を教えれば、推論エンジンが答えを自動的に導き出す」── この発想は AI（人工知能）、自然言語処理、データベースの問い合わせ、専門家システム（エキスパート・システム）、法学における推論の形式化など広い領域で採用され、1980 年代の日本の「第五世代コンピュータ・プロジェクト」の中核言語にも選ばれました。

しかし、Prolog には限界があった

Prolog は強力な発想を持つ言語でした。しかし実務で使い込む研究者たちは、次第に 2 つの根本的な限界に突き当たります。型システムの欠如と、束縛変数の扱いの不自然さです（どちらも記事の前半で説明した言葉です）。

この限界がとりわけ強く感じられたのは、プログラミング言語や論理体系の「意味論」を機械的に扱う場面でした。

「意味論（semantics）」を説明します。意味論とは、プログラムや論理式が「何を意味するか」を厳密に定義したもののことです。「x + 1 というプログラムは、x の値に 1 を足した値を意味する」というルールの集まりが意味論です。新しいプログラミング言語を設計するとき、コンパイラ（ソースコードをコンピュータが実行できる形に翻訳するソフトウェア）を作るとき、型検査器（型の辻褄が合っているかを調べる部品）を作るとき、そして証明支援系の内部データを設計するとき ── こうした場面では、意味論を機械が扱える形で書き下ろす必要があります。

そしてこれらの場面では、プログラム自身や論理式自身を、機械が読み書きするデータとして扱わなければなりません。プログラムにも論理式にも、束縛変数は必ず含まれます。

Prolog の一階論理では、この「束縛変数を含むデータ」を正しく扱えなかったのです。

Miller と Nadathur の共同挑戦（1987 年）

この限界を突破するため、1987 年に Dale Miller（デイル・ミラー、当時 University of Pennsylvania）と Gopalan Nadathur（ゴパラン・ナダドゥル、当時 Duke University）が共同で λProlog の設計を発表しました。

• 論文 ── "A logic programming approach to manipulating formulas and programs"（Symposium on Logic Programming、1987 年）
   
• 論文 ── "Higher-order logic programming"（International Conference on Logic Programming、1988 年）

この２本の論文が、λProlog の学術的な基準点となりました。

さらに 1988 年には、Dale Miller、Gopalan Nadathur、Frank Pfenning、Andre Scedrov の 4 名による共著論文*"Uniform Proofs as a Foundation for Logic Programming"*が ICLP（International Conference on Logic Programming）で発表されました。この論文は「Uniform Proofs（一様な証明）」という概念を通じて、「論理型プログラミングにおける計算とは証明の探索のことである」と厳密に特徴づける枠組みを確立し、λProlog の理論的基盤の基準論文となりました。この基盤のおかげで λProlog は、「何を意味するか（宣言的な意味論）」と「どう動くか（操作的な意味論）」の両方を明晰に持つことができます。

Miller と Nadathur は、Prolog の設計思想 ──「論理を計算のモデルとして使う」── を受け継ぎつつ、次の 3 つの拡張を導入しました。

拡張 １ ── 高階論理への拡張

Prolog は一階論理しか扱えませんでしたが、λProlog は高階論理を扱えます。「関数を変数として扱う」「述語を他の述語の引数にする」ことができるようになりました。

拡張 ２ ── 単純型付きラムダ計算の統合

λProlog では、変数の束縛と、束縛変数を含むデータを、ラムダ抽象（λx. x + 1 のように名前をつけずに関数を書く記法。Python の lambda x: x + 1 にあたります）で表現します。この技法が、後に高階抽象構文（HOAS、Higher-Order Abstract Syntax）と呼ばれる考え方の土台になりました（節 3（HOAS） で解説します）。

拡張 ３ ── Hereditary Harrop Formulas（遺伝的ハロップ論理式）への論理式の拡張

Prolog の Horn 節より表現力の高い論理式の形式である Hereditary Harrop Formulas を、プログラミング言語の中で扱えるようになりました。これによりモジュール性（プログラムを部品に分けて管理すること）、局所的な仮定の導入、名前空間の管理が論理式の中で自然に表現できます（この形式は節 2（七つの違い） の違い 4 で改めて説明します）。

λProlog の最初の主要実装 ── Teyjus（テイジャス）

λProlog の最初の主要な実装は、Gopalan Nadathur とそのチームによる Teyjus（テイジャス）です。ミネソタ大学（University of Minnesota）が主な開発拠点で、OCaml で書かれたコンパイラとして実装されました。最新版 v2.1.1 は 2023 年 2 月 8 日にリリースされ、現在も保守が続いています。

Teyjus は λProlog の言語仕様に忠実な独立したコンパイラとして、学術研究や教育の場面で広く使われてきました。

そして、その 28 年後 ── ELPI の登場（2015 年）

λProlog の用途は、Teyjus の時代には長らく学術研究の領域にとどまっていました。

大きな転機は 2015 年に訪れます。

Cvetan Dunchev、Ferruccio Guidi、Claudio Sacerdoti Coen（いずれもボローニャ大学）と Enrico Tassi（INRIA）が、ELPI（Embeddable Lambda Prolog Interpreter、埋め込み可能なラムダ・プロログ・インタープリタ）を、フィジー（スバ）で開催された LPAR（Logic for Programming, Artificial Intelligence, and Reasoning）会議で発表しました。

• 論文 ── Cvetan Dunchev、Ferruccio Guidi、Claudio Sacerdoti Coen、Enrico Tassi. "ELPI: fast, Embeddable, λProlog Interpreter", Proceedings of LPAR, 2015 年 11 月, Suva, Fiji.

ELPI が革新的だったのは次の 2 点です。

革新 １ ── 高い実行速度

ELPI は、それまで最速の λProlog 実装とされていた Teyjus よりも一貫して高速に動きました。速さの源泉は「還元不要フラグメント（reduction-free fragment）」── λProlog のプログラムに頻出する部分集合 ── を特定し、そこに特化した高速なアルゴリズムを実装したことです。ここでの「還元」とはラムダ式の計算を進める操作を指します。単一化と併せて、この 2 つの操作を速くしたわけです。

革新 ２ ──「埋め込み可能」という設計思想

ELPI は、単独で使うことよりも「他のアプリケーションに組み込まれて使われる」ことを目的に設計されました。OCaml で書かれた API（外部のプログラムから機能を呼び出すための窓口）と FFI（Foreign Function Interface。異なるプログラミング言語の関数を呼び出す仕組み）を通じて、外部のアプリケーションが ELPI のインタープリタを呼び出し、独自の組み込み述語やデータ型を定義できます。

この「埋め込み可能」という設計思想が重要な扉を開きました。

その最大の扉が、後の節で扱う Coq-Elpi です。

ELPI は 2015 年の登場以来、活発に開発が続いています。

最新版 v3.7 は 2026 年 4 月 24 日にリリースされました。

Enrico Tassi 氏が CoqPL 2025（第 11 回 Coq for Programming Languages 国際ワークショップ）で発表した最新論文　"Elpi: rule-based meta-language for Rocq" をはじめ、理論と実装の両面で進化が続いています。

---

節 ２（七つの違い）── Prolog と λProlog は、何が違うのか

記事の前半では、λProlog を「Prolog を 2 つの数学的な道具で強化した言語」と大づかみに紹介しました。ここでは両者の違いを 7 つの観点から詳しく見ていきます。

違い １ ── 論理の階層（一階論理 vs 高階論理）

Prolog が扱えるのは一階論理です。穴に入れられるのも「すべての」と言えるのも、人や数値のような具体的なモノだけです。「すべての整数 x について x + 0 = x」は書けても、「friend という関係は対称的である」「どんな性質 P についても帰納法が使える」のように、述語そのものを主語にした文は書けません ── これが前半で見た一階論理の限界でした。

λProlog が扱えるのは高階論理です。関数や述語も変数として扱え、「すべての述語 P について〜が成り立つ」という文が自然に書けます。Python で map(func, データ) に関数そのものを渡すように、関数を値と同じ「モノ」として受け渡しできる論理です。

この違いは実務のどこに効くのでしょうか。プログラミング言語のコンパイラを書くときや、証明支援系のタクティク（証明を一手ずつ進めるための指示。後の節で詳しく説明します）を書くときには、「あるプログラムを別のプログラムに変換する」「ある証明を別の証明に変換する」という操作を扱います。この「プログラムや証明を扱うプログラム（メタプログラム）」を書くのに、高階論理は欠かせないのです。

違い ２ ── 束縛変数の扱い（名前ベース vs ラムダ抽象）

Prolog では、変数は名前で区別されます。「変数 X」と「変数 Y」は名前によって別のものとして扱われます。

λProlog では、束縛変数を単純型付きラムダ計算のラムダ抽象で表現します。この技法のおかげで、α 変換（変数の名前の付け替え）や、代入時の変数捕獲の回避といった「束縛変数を扱うときに必要な細かい配慮」を、λProlog が自動で処理してくれます（α 変換や変数捕獲が何かは、節 3（HOAS） で具体例とともに解説します）。

この違いは実務のどこに効くのでしょうか。プログラミング言語の意味論を機械的に扱うときには、「x = 3 のもとで body(x) の x が指すもの」といった束縛の扱いが必ず登場します。Prolog のように束縛変数を名前で扱うと、名前の付け替えや取り違えを書き手が自分で管理することになります。この管理は間違いやすく、コードを読みにくくします。λProlog では、この管理が言語そのものに組み込まれています。

違い ３ ── 型システム（型なし vs 単純型付き）

Prolog（伝統的な ISO Prolog）は型なしの言語です。述語や関数に引数の型を宣言できません。

λProlog は単純型付きラムダ計算に基づく型システムを持ち、述語や関数に引数の型を明示的に宣言します。

この違いは実務のどこに効くのでしょうか。大規模なプログラムでは、型システムは「実行する前の段階（コンパイル時）でバグを見つける」手段になります。Prolog では型のミスが実行時に初めて発覚しがちですが、λProlog ではコンパイル時に見つかります。

違い ４ ── 論理式の形式（Horn 節 vs Hereditary Harrop Formulas）

Prolog が扱うのは、「A かつ B ならば C」という形の比較的単純な論理式である Horn 節です。

λProlog が扱うのは「Hereditary Harrop Formulas（遺伝的ハロップ論理式）」という、Horn 節を含むより広い形式です。含意（「A ならば B」という形の論理式のこと）や量化子を、より自由な位置に入れ子にして書けます。

初めて目にする名前だと思いますが、一言でいえば「Horn 節を、豊かな入れ子構造を許す形へ拡張した論理式」です。Python でいえば、単純な型ヒント x: int しか書けなかったところに list[dict[str, int]] のような入れ子の型ヒントが書けるようになったときの、あの表現力の広がりに近いものがあります。「Harrop」は英国の論理学者 Ronald Harrop の名前に、「Hereditary（遺伝的）」は「含意や量化子で入れ子にしても形式が保たれる」性質に由来します。

この違いは実務のどこに効くのでしょうか。Hereditary Harrop Formulas を使うと、モジュール性、局所的な仮定の導入、名前空間の管理を論理式の中で自然に表現できます。大規模なプログラミング言語や証明系を実装するとき、この表現力の差が大きく効いてきます。

違い ５ ── メタプログラミング（困難 vs 自然）

Prolog では、メタプログラミング（プログラムを操作するプログラム）は call/1 や bagof/3 といった、その場しのぎの述語で対応するしかありませんでした。

λProlog では、高階論理と単純型付きラムダ計算の組み合わせにより、メタプログラミングが「言語の自然な使い方」として組み込まれています。「あるプログラムを受け取り、変換して、新しいプログラムを返す」という処理が素直に書けます。

違い ６ ── 構文（括弧で引数を渡す書き方 vs カリー化された書き方）

Prolog の関数適用は、C 言語や Python と同じく括弧の中に引数を並べる書き方です。p(x, f(y)) のように書きます。

λProlog の関数適用は、OCaml や Haskell と同じ「カリー化された書き方」です。p x (f y) のように、括弧を使わず引数を空白で並べます。カリー化とは、複数の引数を取る関数を「引数を 1 つずつ順に受け取る形」で扱う流儀のことです。

この違いが実務に与える影響は大きくありませんが、λProlog が OCaml や Haskell といった関数型プログラミング言語の伝統に近いことを物語っています。

違い ７ ── 実行モデル（逐次的な探索 vs より洗練された制約解決）

Prolog は、Horn 節を深さ優先で探索することで実行されます。中核にあるのは、記事の前半で説明したバックトラック ── 行き詰まったら直前の分かれ道に戻って別の選択を試す動き方 ── です。

λProlog の実装、特に ELPI では、この探索モデルに Constraint Handling Rules（CHR、制約処理規則）による制約解決の枠組みが加わっています。「まだ決まっていない部分は『制約』── 満たすべき条件 ── として持ち越しながら、決められるところから計算を進める」という、より洗練された実行モデルです。

一言で言えば

Prolog が「一階論理の中で Horn 節を機械的に推論する言語」であるのに対し、λProlog は「高階論理の中で、Hereditary Harrop Formulas を、単純型付きラムダ計算の力を借りて機械的に推論する言語」です。

この拡張の総体が、「プログラミング言語や論理体系の意味論を自然に正しく扱える」という、Prolog には持ち得なかった能力を λProlog に与えているのです。

---

節 ３（HOAS）── 高階抽象構文（Higher-Order Abstract Syntax）を使う理由

λProlog を語るうえで避けて通れない概念が、高階抽象構文（HOAS、Higher-Order Abstract Syntax）です。

この概念こそが、λProlog を Prolog をはじめとする他の論理型プログラミング言語からはっきりと区別する、核心の技法です。

そもそも「束縛変数を扱う」とは、どういう問題か

HOAS を理解する前に、「束縛変数を扱う」というプログラミング上の問題を整理します。

Python の関数定義を考えてください。

def add_one(x):
    return x + 1

この関数の中の x は束縛変数です。x という名前はこの関数の中でだけ意味を持ち、外に出れば消えてしまいます。

この関数を y という名前で書き直しても、同じ関数です。

def add_one(y):
    return y + 1

「x で書いた関数」と「y で書いた関数」は名前が違うだけで実質的に同じです。この「名前の違いを気にせず同じとみなす」ための名前の付け替えを、α 変換（アルファ変換、alpha conversion）と呼びます。

さて、ここで問題です。「関数をデータとして扱う」プログラムを書くとき、この束縛変数をプログラム上でどう表現するべきでしょうか。

この問題は次の場面で必ず登場します。

• プログラミング言語のコンパイラを書くとき ── コンパイラの内部では、パーサという部品がソースコードを解析して「構文木」を作り、その構文木の中の変数を扱います。構文木とは、プログラムの文法構造を木の形のデータにしたものです。たとえば 1 + 2 * 3 というコードは「足し算の左が 1、右が『2 かける 3』」という入れ子の木として表現されます
• プログラミング言語の意味論を機械的に扱うとき ── プログラムの動作を機械が理解できる形で定義する
• 証明支援系を書くとき ── 数学の論理式（「すべての x について P(x)」など）を機械が扱うデータとして表現する

従来の解法（一階抽象構文、First-Order Abstract Syntax）

Prolog を含む従来の言語では、束縛変数を「名前（文字列）」として扱うのが一般的でした。この技法を「一階抽象構文（First-Order Abstract Syntax）」と呼びます。

具体的にはこう表現します。

• 変数 x を、文字列「x」として表現
   
• 関数 λx. body（「x を受け取って body を返す関数」のラムダ記法）を、lambda("x", body) のようなデータ構造として表現

この方法には３つの問題が生じます。

問題 １ ── α 変換の管理を書き手が自分で行わなければならない

「lambda("x", body(x))」と「lambda("y", body(y))」を同じものと見なす処理を、書き手が自分で書く必要があります。

問題 ２ ── 代入時の「変数捕獲」を書き手が防がなければならない

変数捕獲とは、代入のときに、たまたま同じ名前だった別々の変数が誤って同一視されてしまう事故のことです。「lambda("x", body) に y = f(x) を代入する」とき、body の中の x と f(x) の x が同じ変数だと誤解されないよう、名前の付け替えを書き手が管理しなければなりません。

問題 ３ ── β 簡約（関数適用の実行）を書き手が実装しなければならない

β 簡約（ベータ簡約）とは、「(λx. body) を引数 arg に適用したもの」を「body の中の x を arg で置き換えたもの」へと計算し進めることです。関数を呼び出したときに実際に起きる計算にあたります。この処理も書き手が自分で実装することになります。

これらの管理は間違いやすく、コードを読みにくくします。プログラミング言語の意味論を機械的に扱うとき、書き手はこの「束縛変数の管理」に多くの労力を取られてしまうのです。

λProlog の解法（高階抽象構文、HOAS）

λProlog はこの問題に、根本から異なる解法を示しました。

「束縛変数の扱いを、宿主言語（この場合は λProlog 自身）のラムダ抽象に委ねる」という解法です。

一行で書くとあっさりしていますが、これだけでは何が起きているのか分からないと思います。「委ねる」とは具体的にどうすることなのか、なぜそれで問題が解決するのかを、順を追って種明かしします。

まず、表現の仕方がこう変わります。

• 変数 x を、λProlog 自身のラムダ変数として表現
   
• 関数 λx. body を、λProlog 自身のラムダ抽象 x \ body として表現（λProlog の構文ではバックスラッシュ \ がラムダ抽象を表します）

一階抽象構文の lambda("x", body) と、HOAS の x \ body は、見た目こそ似ていますが正体がまったく違います。lambda("x", body) は、lambda というラベルに文字列 "x" と本体をぶら下げただけの自作データです。その "x" が束縛変数のつもりだということを、言語は知りません。一方 x \ body は、λProlog にとって正真正銘の「関数の値」です。Python でたとえるなら、前者は ("lambda", "x", "x + 1") というただのタプル、後者は lambda x: x + 1 を実行してできる本物の関数オブジェクトに相当します。

「委ねる」とはつまり、束縛変数を含むデータを「名前入りの自作データ」としてではなく「言語にとっての本物の関数」として持つ、ということです。そうすれば束縛変数の面倒はすべて、言語が関数を動かすために最初から備えている仕組みが引き受けてくれます。

この持ち替えによって次の効果が得られます。なぜそうなるのかの理由も、一つずつ添えます。

効果 １ ── α 変換が言語に組み込まれる（名前の違いが消える理由）

Python で次の 2 つの関数を作ってみてください。

f = lambda x: x + 1
g = lambda y: y + 1

f と g は完全に同じ働きをします。パラメータ名の x や y は、関数オブジェクトができあがった瞬間に役目を終えるからです。関数の中身にとって大事なのは「受け取った値をどの場所で使うか」という位置の情報だけで、その場所を何と呼ぶかは書き手の趣味にすぎません。言語は関数を実行するとき、名前ではなくこの位置の対応で値を届けます。

λProlog のラムダ抽象も同じです。x \ body(x) と y \ body(y) は、λProlog の内部では「受け取ったものを body のこの位置に差し込む関数」という同一の存在であり、x や y という名前はデータとして保存されていません。名前が保存されていないのだから、名前を比較して別物と誤判定する事故は起こりようがない ── つまり α 変換の問題は、解決されたというより、最初から発生しない形にデータを持ち替えたのです。苦肉の策 1 が失敗したのは名前を文字列としてデータに残したからで、HOAS はその名前をデータから消した、と言い換えられます。

効果 ２ ── 代入時の変数捕獲が自動的に回避される（言語のスコープ管理に乗る理由）

Python を書いていて、「内側の関数の変数と外側の変数がたまたま同じ名前だったせいで、値が混線した」という経験はまず無いはずです。

x = 100

def make_adder(n):
    return lambda x: x + n   # この x は、外側の x = 100 とは別物

add3 = make_adder(3)
print(add3(5))    # 8 （外側の x = 100 は一切関係しない）

同じ名前の変数が混線しないのは、変数の有効範囲（スコープ）の管理が言語自身の仕事だからです。言語はプログラムを正しく動かすために、この管理を絶対に間違えないよう作り込まれています。ここを間違えたら、世界中のプログラムが壊れてしまうからです。

HOAS の代入は、λProlog 自身の関数適用として実行されます。つまり、この「言語が絶対に間違えないスコープ管理」の上で代入が走るのです。苦肉の策では、書き手が自作した代入処理が名前の衝突を自力で避ける必要がありました。HOAS では代入そのものを言語のエンジンに任せるので、変数捕獲は言語が防いでくれます。

効果 ３ ── β 簡約が言語に組み込まれる

そして関数適用の実行（β 簡約）は、λProlog が自分のプログラムを動かすために最初から持っている機能そのものです。書き手が実装する必要はありません。

まとめると、こうなります。一階抽象構文は「関数のデータ」を自作し、α 変換も代入も自作していました。HOAS は、言語が動くために正しく整備されている既存の道 ── 関数の値、スコープ管理、関数適用 ── にデータを乗せ替えることで、自作部分そのものを消したのです。これが「宿主言語のラムダ抽象に委ねる」の中身です。

この技法の名前 ── 高階抽象構文（HOAS）

この 「束縛変数の扱いを宿主言語のラムダ抽象に委ねる」技法 を、高階抽象構文（HOAS、Higher-Order Abstract Syntax ） と呼びます。

「高階（higher-order）」という名前は、「変数の束縛を扱うために、宿主言語の関数（高階の対象）を借りている」ことに由来 します。

HOASという技法 自体は、1988 年に Frank Pfenning（フランク・フェニング、当時 Carnegie Mellon University）と Conal Elliott が論文*"Higher-Order Abstract Syntax"*で正式に定式化しました。

しかしその発想の起源は、1987 年の Miller と Nadathur による λProlog の設計 にまで遡ります。

λProlog は、HOAS の発想をプログラミング言語の設計思想として最初に体現した言語 なのです。

一階抽象構文と HOAS の対比 ── 一枚の図で

「従来の一階抽象構文」と「HOAS」の違いを一枚の図で整理します。

題材は、Python の関数 def add_one(x): return x + 1 に対応するラムダ式 λx. x + 1 です。

同じ内容を表形式でも整理します。

ステップ	従来の一階抽象構文（First-Order Abstract Syntax）	HOAS（高階抽象構文）
束縛変数の表現	文字列（"x"）として名前で管理	宿主言語（λProlog）のラムダ変数として管理
ラムダ抽象の表現	lambda("x", body(x)) のようなデータ構造	宿主言語のラムダ抽象 x \ body(x)
α 変換の管理	書き手が明示的に書く	言語が自動で処理
変数捕獲の回避	書き手が明示的に書く	言語が自動で処理
β 簡約の実装	書き手が明示的に書く	言語が自動で処理
結果	間違いやすく、コードが不透明	正しく、コードが透明

この違いはコードの行数を見れば一目瞭然です。Prolog で HOAS 相当のことを実装しようとすると、束縛変数の管理と β 簡約の実装だけで多くのコードが必要になります。λProlog では、それが宿主言語の力でコードから消えるのです。

HOAS の実務上の意味

HOAS を使うと、次のような「束縛変数を扱うプログラミング」が自然に書けるようになります。

• プログラミング言語のコンパイラ、特に変数の有効範囲を厳密に扱うコンパイラ
• 型検査器の実装
• プログラミング言語の意味論の形式化（形式化とは、定義や証明を機械が検査できる厳密な形式に書き直すことです）
• 証明支援系の内部データ構造（証明のデータ、論理式の表現）
• 数学の論理式（「すべての」「ある」やラムダを含む論理式）の機械的な扱い

Rocq、Lean 4、Isabelle、Agda といった主要な定理証明系の内部でも、HOAS の発想はさまざまな形で活用されています。

そして、λProlog の実装である ELPI が Rocq の拡張言語 Coq-Elpi として選ばれた根本的な理由の一つが、この HOAS の力 なのです。

---

【中間の解説】Rocq（旧 Coq）とは何か？ そして、Rocq と Prolog / λProlog / ELPI は、どう接続するのか？

ここまで λProlog の設計思想を、5 つの問いのうちの 3 つ ── なぜ生まれたか、Prolog との違い、HOAS を使う理由 ── に沿って見てきました。

次の節 4（実務） では、λProlog の実装である ELPI が Rocq という定理証明系の拡張言語としてどう使われているか を紹介します。

記事の前半で Rocq には軽く触れましたが、その前にここで本格的に取り上げておきます。

答えるべき疑問は２つです。

• 「そもそも Rocq（旧 Coq）とは、どんな仕組みのソフトウェアなのか？」
• 「Rocq と λProlog/ELPI は仕組みが根本的に異なる言語のはずなのに、なぜ接続できるのか？」

Rocq（旧 Coq）とは何か

Coq（コック。2023 年に「Rocq（ロック）」へ改名されました）は、1984 年にフランスの国立研究所 INRIA（パリ近郊 Rocquencourt）で Thierry Coquand（ティエリ・コカン、当時ゴーテンブルク大学）と Gérard Huet（ジェラール・ユエ、INRIA）が開発を始めた 対話的定理証明系 です。

「対話的」 と呼ばれるのは、人間が証明を一手ずつ入力し、機械がその都度チェックと途中経過の表示を返す、というやり取りで証明を作っていくから です。

1991 年には Christine Paulin（クリスティーン・ポラン、当時 INRIA）が その 理論的基盤を、"Calculus of Inductive Constructions（CIC、帰納的構成の計算）" へと拡張 し、現代の Rocq の土台 を築きました。

Rocq の主な用途は次の３つです。

• 数学の定理を、機械が検査できる形に書き直す（例：「どんな地図も 4 色で塗り分けられる」という 1976 年の四色定理。Georges Gonthier〈現在 INRIA〉が 2005 年に Rocq による形式化を完成させました）
   
• プログラミング言語のコンパイラや OS カーネル（オペレーティング・システムの中核部品）の正しさを機械的に証明する（例：検証済み C コンパイラ CompCert。Xavier Leroy 主導、INRIA、2009 年）
   
• 暗号や通信の仕組みなど、安全性が命であるソフトウェアの正しさを検証する

Rocq を一言で表すなら、「型がきわだって強力なプログラミング言語であり、その強力な型で『定理』そのものを表現し、その定理の証明を機械が検査してくれるシステム」 です。

「型が強力」の意味を、Python の型ヒントと比べて説明します。

Python の型ヒントは次のようなものです。

def add(x: int, y: int) -> int:
    return x + y

Python では「型 int」は整数の集合を表し、関数 add の型は「int を 2 つ受け取り int を返す関数」です。

Rocq では、この「型」がはるかに強力になります。

「すべての整数 $x$ について $x + 0 = x$ が成り立つ」という数学の主張そのものを、型として書ける のです。

具体的な姿を見てください。
Rocq(の言語 Gallina)では、この主張は次のたった１行のコードで表現することができます。

(* この 1 行の「: 」の右側ぜんぶが、型であり、証明したい主張そのものです *)
Theorem add_0_r : forall x : nat, x + 0 = x.

forall x : nat は「自然数型 nat(0 以上の整数を表す型)のすべての x について」という意味です。

Python の型ヒント int が「整数のどれか 1 つ」しか語れなかったのに対し、この行の型は「すべての $x$ で $x + 0 = x$ が成り立つ」という数学の主張を、型の文法で丸ごと述べています。

あとは、この型を持つ「値」を作れば ── つまり Proof. から Qed. までを書き上げれば ── 主張は証明されたことになります。

（この定理は、この後の「実際の証明コードを見る」で、証明の中身つきでもう一度登場します）

そして、その型を「実現する値」を書くことが、そのままその主張の証明を書くことになります。

「主張を型として表し、証明をその型を実現する値として書く」
── この一見不思議な発想は、Curry-Howard 対応（カリー・ハワード対応）という論理学の発見 に基づいています。

1934 年から 1969 年頃にかけて見出された**「論理の世界の証明」と「プログラムの世界の型付き関数」が実は同じ構造をしている、という対応関係のこと** です。

Rocq の理論的基盤 CIC は、この Curry-Howard 対応を、依存型（ dependent types 。「長さがちょうど n のリスト」のように値に応じて決まる型）と帰納型（ inductive types 。「空リスト」と「要素を 1 つ足したリスト」のように、基本の形と組み立て方の規則からデータを定義する仕組み）の力で豊かに拡張した体系 です。

Rocq を構成する２つの言語 ── Gallina と Ltac

Rocq は実際には２つの言語でできています。

• Gallina（ガリーナ）── Rocq の仕様言語。定理、関数、データ型を記述する言語で、「関数の型と実装を書く言語」にあたります。
   
• Ltac（エルタック）── Rocq のタクティク言語。証明を機械への指示の連続として書く言語で、「証明の途中経過を段階的に変形していくスクリプト言語」にあたります。

たとえば、「すべての整数 $x$ について $x + 0 = x$ が成り立つ」という定理を Rocq で証明する場合、まず Gallinaで定理を書き、次に Ltac のタクティクを積み重ねて証明を組み上げます。

タクティクの一手一手が、Rocq の内部で「証明項（proof term）」── 証明そのものを表すデータ ── を少しずつ組み立てていきます。

実際の証明コードを見る ── Rocq と Lean 4

抽象的な説明だけではイメージが湧きにくいので、「すべての自然数 $x$ について $x + 0 = x$」を Rocq で実際に証明したコードの全文を見てみます。

Theorem add_0_r : forall x : nat, x + 0 = x.
Proof.
  intros x.
  induction x.
  - reflexivity.
  - simpl. rewrite IHx. reflexivity.
Qed.

1 行目の Theorem add_0_r : forall x : nat, x + 0 = x. が Gallinaで書いた定理の宣言 です。

forall x : nat は「自然数型 nat のすべての x について」という意味で、この行全体が「型」であること を思い出してください。

なお、Theorem の直後の add_0_r は定理の名前で、Python の関数名やクラス名と同じく、プログラマが自由に命名できる識別子です。英

字・数字・アンダースコアなどが使え、慣習として内容の分かる名前を付けます（この名前は add zero right、「右側に 0 を足す」の略です）。

証明した定理は、後から rewrite add_0_r のように名前で呼び出して再利用できる ので、良い名前を付ける価値も Python と同じです。

Proof. から Qed. までが Ltac のタクティクによる証明本体です。

一手ずつ何をしているのか表にします。

タクティク	何をする一手か
intros x	「すべての x について」の x を証明の場に取り出す。Python の関数が引数 x を受け取るのに似た一手
induction x	x について数学的帰納法を始める。ゴールが「x = 0 の場合」と「x = n + 1 の場合（n で成り立つと仮定してよい）」の 2 つに分かれる
reflexivity	左辺と右辺が同じ形になっていたら「等しい」で閉じる
simpl	式を計算できるところまで簡単にする
rewrite IHx	帰納法の仮定 IHx（n + 0 = n）を使って式を書き換える

- で始まる 2 つのブロックが、帰納法で分かれた２つの場合に対応 します。

$0$ の場合 は reflexivity の一言で閉じ、$n + 1$ の場合 は「$簡約 → 仮定で書き換え → 等しい$ 」の ３手で閉じています。

最後の Qed. の瞬間に、組み上がった証明項を Rocq のカーネルが検査し、通れば定理として登録されます。

比較のために、同じ定理を Lean 4 で書くとこうなります。

example (x : Nat) : x + 0 = x := rfl

たった１行 です。

Lean 4 の標準ライブラリでは足し算の定義の向きが Rocq と逆になっているため、この定理は「定義そのまま（rfl）」の一言で済んでしまうのです。

同じ定理でも土台の定義の設計しだいで証明の手間が変わる ── 定理証明の世界の興味深い一面です。

そして、この Ltac の弱点（型がない、デバッグが難しい、メタプログラミングが不自然） を λProlog/ELPI で置き換えたものが Coq-Elpi です（節 4（実務） で詳しく扱います）。

では、同じ証明を Coq-Elpi で書くとどうなるか

Ltac と Coq-Elpi の書き味の違い を、先ほどの定理 add_0_r で実際に見比べてみます。

証明の骨格は同じまま、「等しさで閉じる」最後の一手を、λProlog で自作したタクティク finish に置き換えたのが次のコードです（Coq-Elpi チュートリアルの流儀に沿った最小の例です）。

From elpi Require Import elpi.   (* Coq-Elpi プラグインの読み込み *)

Elpi Tactic finish.
Elpi Accumulate lp:{{

  % 規則 1: ゴールが「〜 = 〜」という等式の形なら、
  %         「左右は同じもの」という証明の断片 eq_refl をあてはめて閉じる
  solve (goal _ _ {{ _ = _ }} _ _ as G) GL :-
    refine {{ eq_refl }} G GL.

  % 規則 2: それ以外の形のゴールには、ゴールの型を添えたエラーを返す
  solve (goal _ _ Ty _ _) _ :-
    coq.error "finish は等式の形のゴール専用です。いまのゴール:" Ty.

}}.

Theorem add_0_r' : forall x : nat, x + 0 = x.
Proof.
  intros x. induction x.
  - elpi finish.
  - simpl. rewrite IHx. elpi finish.
Qed.

上記のコードを読み解いてみましょう。

Elpi Accumulate lp:{{ ... }} の中身が λProlog のプログラムです。

Rocq のファイルの中に、ここまで見てきた Horn 節がそのまま同居していることが分かります。

定理名 add_0_r' の末尾のアポストロフィは、Rocq では名前に使える文字の一つで、「別バージョン」を表す慣習的な印です。

solve はタクティクの本体を表す述語で、第１引数に「いまのゴール」が渡されてきます。

規則 １の頭にある {{ _ = _ }} に注目してください。

二重波括弧 {{ ... }} は、λProlog のプログラムの中に Rocq の式をそのまま書くための記法です（この後の「接続の仕組み」で詳しく説明します）。

単一化の力で「ゴールが等式の形をしているときだけ」規則 １ が発動し、eq_refl（左右は同じものだ、という証明の断片）をゴールにあてはめます。

等式でなければ規則 １ は単一化に失敗し、バックトラックで規則 ２ に落ちて、ゴールの型 Ty を添えた分かりやすいエラーを返します。

この短い例に、Ltacの３つの弱点への答えが揃っています。

• 型がない、への答え ── solve が受け取るゴールには決まった型があり、エラーにも型情報 Ty をそのまま添えられます
   
• デバッグが難しい、への答え ── 規則 ２ のように「想定外の入力に、中身の見えるエラーを返す」振る舞いを最初から自然に書けます
   
• メタプログラミングが不自然、への答え ──「ゴールの形で処理を分岐する」という仕事が、Horn 節と単一化とバックトラック ── 本記事の前半で学んだ道具そのもの ── で書けています

使う側から見ると、自作の elpi finish は reflexivity と同じ感覚で証明の中から呼び出せます。

タクティクという部品を、型と単一化のある言語で自作できる ── これが Coq-Elpi の書き味 です。

では、なぜ Rocq と Prolog / λProlog / ELPI が接続できるのか

ここで 根本的な疑問 が生じます。

• 「Rocq は、CIC という強力な依存型を持つ、関数型プログラミング言語の系譜」
   
• 「一方、Prolog / λProlog / ELPI は、Horn 節や Hereditary Harrop Formulas に基づく、論理型プログラミング言語の系譜」

「この 2 つは仕組みが根本的に異なるはず。なぜ手を結べるのか？」

この疑問に３つの側面から答えます。

３つの側面 ── 定理証明支援言語の仕組み、論理プログラム言語の仕組み、両者が接続する仕組み

側面 １ ── 定理証明支援言語（Rocq、Lean、Isabelle、Agda、F* など）の仕組み

定理証明支援言語は、「型を出発点として、証明項を段階的に組み立てる」システムです。
流れは次のとおりです。

• ステップ 1 ── 証明したい定理を型として書く（Rocq の場合、Gallina で forall x : nat, x + 0 = x のように書く。forall は「すべての〜について」、nat は自然数の型です）
   
• ステップ 2 ── その型を実現する証明項を、タクティクを積み重ねて組み立てる（Rocq の場合、Ltac で intros x. induction x. reflexivity. simpl. rewrite IHx. reflexivity. のように書く）
   
• ステップ 3 ── 完成した証明項を、Rocq のカーネル（証明の最終検査だけを担う小さな型検査器）が検査する。型検査に通れば、その定理は「機械が検査した証明を持つ」ことになる

要するに定理証明支援言語とは、「Python の型ヒントを、数学の主張そのものを表せるところまで強力にしたもの。そして、その型を実現する値を書くことが、その主張の証明を書くことになるもの」です。

中核にあるのは、先ほど説明した「型が主張を表し、値（証明項）が証明を表す」という Curry-Howard 対応です。

側面 ２ ── 論理プログラム言語（Prolog、λProlog、ELPI）の仕組み

論理プログラム言語は、「事実と規則を宣言的に書き、推論エンジンが答えを自動的に探索する」システムです。

「宣言的」とは、手順ではなく「何が成り立つか」を書き並べるスタイルのことです。流れは、記事の前半で見た家系図の例のとおりです。

• ステップ 1 ── 事実と規則を書く（father(jiro, taro). father(saburo, jiro). grandfather(X, Z) :- father(X, Y), father(Y, Z).）
   
• ステップ 2 ── 質問を投げる（grandfather(G, taro).「太郎の祖父 G は誰か」）
   
• ステップ 3 ── 推論エンジンが、単一化とバックトラックを組み合わせて答えを探索する
   
• ステップ 4 ── 答えが見つかれば返す（この例では G = saburo）

SQLに馴染みがあるなら、「SQL のクエリをもっと一般的な論理式で書けるようにし、それを単一化とバックトラックで解くもの」というイメージも持てます。

λProlog では、この土台に「HOAS による束縛変数の自然な扱い」「高階論理」「単純型付きラムダ計算に基づく型システム」が加わります。

ELPI では、さらに「Constraint Handling Rules（CHR）による制約解決」も加わります。

側面 ３ ── 両者が接続する仕組み（Coq-Elpi の HOAS 埋め込み）

ここで核心の問いです。

「型を出発点に証明項を組み立てる」Rocq と、「事実と規則を書いて推論エンジンが探索する」λProlog/ELPI は、どうやって手を結ぶのでしょうか。

答えは、「HOAS を使って、Rocq の項（term。Rocq の内部で式や証明を表すデータ）を λProlog の項として埋め込む」です。

仕組みを順に見ていきます。

接続の仕組み １ ── Rocq の項の、HOAS による埋め込み

Rocq の内部データ（証明項、ゴール、コンテキスト〈証明の途中で使える仮定の一覧〉、環境〈定理と定義のデータベース〉）は、すべて「束縛変数を含むラムダ計算の項」として表現されています。

Coq-Elpiプラグインは、この Rocq の項を HOAS の技法で λProlog の項として埋め込みます。

この HOAS の力により、Rocq の束縛変数の扱いを λProlog が自動で管理できます。

$α$ 変換、変数捕獲の回避、$β$ 簡約
── これらはすべて λProlog の言語機能に組み込まれているので、Coq-Elpi のプログラマはこの管理を意識せずに済みます。

接続の仕組み ２ ── Rocq の API の、ELPI への公開

Coq-Elpi は、Rocq の内部の API を ELPI から呼び出せるように公開しています。

ELPI のプログラムから、Rocq の環境（定理と定義のデータベース）を検索し、新しい定数を定義し、型検査器を呼び出し、証明項を組み立てる
── これらの操作がすべて可能です。

イメージとしては、3Dモデリング・ソフトウェア Blender の内部で Python スクリプトが 3D モデルを操作する関係に近いものがあります。

Blender の内部データを Python スクリプトが読み書きするように、Rocq の内部データを ELPI のプログラムが読み書きするのです。

接続の仕組み ３ ── λProlog の単一化変数と、Rocq の evar の対応

Rocq の内部には「evar（存在変数、existential variable ）」という、「まだ値が決まっていない項」を表す仕組みがあります。

証明を組み立てている途中では、この evar が「まだ埋まっていない穴」として存在します。

Coq-Elpi は、この Rocq の evar を λProlog の「単一化変数（まだ値の決まっていない変数）」に対応づけました。

これにより両者の「まだ決まっていない項」を同じ仕組みで扱えるようになり、「Rocq の証明の穴を ELPI の推論エンジンが自動で埋めていく」処理が自然に書けます。

接続の仕組み ４ ── クォーテーション（引用符）による Rocq 構文の直接記述

Coq-Elpi は {{ ... }} という記法を備えており、ELPI のプログラムの中に Rocq の構文を直接書くことができます。

たとえば {{nat}} と書けば「Rocq の自然数の型」を意味する項に、{{A -> B}} と書けば「A から B への関数の型」を意味する項に自動的に展開されます。

この恩恵に浴することで、ELPI のプログラマは、Rocq の内部データ構造を細かく意識せずに、Rocq の自然な構文でメタプログラミングを書くことができるのです。

全体を俯瞰すると

上記の４つの仕組み
── HOAS による項の埋め込み、Rocq API の公開、単一化変数の対応、クォーテーション
── の組み合わせにより、Rocq と λProlog/ELPI は、根本的に異なる仕組みを持ちながらも緊密に手を結んでいます。

Rocq自体は「型を出発点に証明項を組み立てる」定理証明支援系の側面を担い、λProlog/ELPI は「Rocq の内部データを宣言的にメタプログラミングする」拡張言語の側面を担う。

両者はそれぞれの得意分野を活かしつつ、HOAS の力で接続されているわけです。

この２つの言語の接続こそが、Coq-Elpi、Hierarchy Builder、mathcomp の代数階層構築
── これらすべての実務プロジェクトを支える基盤なのです。

【もう一つの疑問】なぜ Rocq は単独で仕事を完結できず、ELPI の助けが必要なのか

節 4（実務） に進む前に、素朴な疑問に答えておきます。

「Rocq は世界的な定理証明系なのに、なぜ単独で仕事ができず、わざわざ別の言語の力を借りるのか？」という疑問です。

正直に言えば、Rocq は単独でも定理証明ができます。

Gallina で定理を書き、Ltac で証明し、カーネルが検査する
── この一式は Rocq 本体に備わっています。

小さな定理を証明するだけなら、Rocq 単独で何の不自由もありません。

それでも実務の現場で拡張言語の助けが必要になるのには、３つの理由があります。

理由 １ ── 検査の中核は、意図的に「小さく」保たれている

Rocq の設計思想では、証明の最終検査を担うカーネルを、できるかぎり小さく単純に保ちます。

カーネルは「絶対に信頼できなければならない部分」だからです。
ここにバグがあれば、間違った証明が「正しい」と認定されてしまいます。

信頼の基盤は小さく ── セキュリティの世界と同じ原則です。

その代わり、便利な機能は本体の外側に拡張として足していきます。

この設計には大きな利点があります。
外側の拡張プログラムにバグがあっても、最後にカーネルが検査するので、間違った証明が通ることはありません。

だから拡張言語は、安心して強力にできるのです。

ELPI（Coq-Elpi）は、この「外側」を書くための言語です。

理由 ２ ── 実務の証明には、大量の「繰り返し仕事」がある

Excel を思い浮かべてください。

セルに数式を一つずつ書くのは Excel 単独でできます。
しかし数千行に同じ処理を繰り返すなら、マクロが欲しくなります。

Rocq も同じです。

mathcomp のような大規模ライブラリでは、似た形の定義や補題（大きな定理を支えるための小さな定理）を数百個単位で整備する仕事が日常です。

一つずつ手で書くのは現実的ではなく、「定義を量産するプログラム」
── つまりメタプログラミング
── が必須になります。

Rocq にとってのマクロ言語が、伝統的には Ltac であり、その現代的な強化が Coq-Elpi なのです。

理由 ３ ── 伝統のマクロ言語 Ltac には、限界があった

その Ltac には型が無く、デバッグが難しく、大規模なメタプログラミングの保守が困難でした（詳しくは次の節 4（実務） で扱います）。

Rocq のコミュニティは後継を模索し、その有力な答えの一つが、「束縛変数と高階論理の扱いに最初から強い言語 λProlog を、丸ごと拡張言語として迎え入れる」という Coq-Elpi の道 でした。

まとめると、こうなります。

• Rocq は単独でも証明を「書ける」。
• しかし実務規模の証明開発を「回す」には、小さなカーネルの外側で自動化と量産を担う拡張言語が要る。
• その役割を担っているのが ELPI ── これが答えです。

---

節 4（実務）── Coq-Elpi、Hierarchy Builder、Abella、Makam：λProlog は実務でどう使われているか

λProlog とその実装である ELPI は、学術研究の玩具ではありません。

世界の定理証明系とプログラミング言語理論の現場で、確固たる位置を築いています。

主要な実務での用途を４つの実例で見ていきます。

実務での用途 １ ── Coq-Elpi、Rocq の拡張言語

λProlog/ELPI の最も重要な用途は、Rocq（旧称 Coq）の拡張言語 Coq-Elpi です。

Rocq の内部では、証明を組み立てるために「タクティク（tactic）」という命令を書きます。前の節でも触れましたが、ここで改めて説明します。

タクティク とは「証明を機械に指示するための、関数のようなもの」です。

Python の関数が値を扱うのに対し、タクティクは「証明の途中経過（まだ証明されていない目標。ゴールと呼びます）」を扱います。

たとえば「すべての整数 $x$ について $x + 0 = x$ が成り立つ」という定理を証明したいとします。

Rocq には証明の途中経過がゴールとして表示されます。

タクティクはこのゴールを少しずつ変形し、最終的に「証明済み」の状態へ導く「一手」の役割を果たします。

将棋やチェスの一手のように、「intro を打つ」「apply を打つ」「rewrite を打つ」と積み重ねて証明を組み上げていくわけです。

Python でいえば、def transform_goal(goal): ... のような関数を証明の各段階で呼び出していくイメージです。

Rocq の伝統的なタクティク言語 Ltac は、長年 3 つの問題を抱えていました。

• 型がない ── タクティクの中で間違った型の引数を渡しても、実行時までエラーが分からない
• デバッグが難しい ── タクティクの動作を途中で観察しにくい
• メタプログラミングが不自然 ── タクティクを合成したり変換したりする処理が書きにくい

Enrico Tassi（INRIA）はこの問題を λProlog/ELPI で解決しようと考えました。

そして 2018 年頃から、Rocq の拡張言語 Coq-Elpi の開発が本格化します。

• 論文 ── Enrico Tassi. "Elpi: an extension language for Coq（Metaprogramming Coq in the Elpi λProlog dialect）", The Fourth International Workshop on Coq for Programming Languages, 2018 年.

Coq-Elpi を使うと、Rocq の .v ファイルの中に直接 λProlog/ELPI のプログラムを書けるようになります。

その ELPI のプログラムからは、Rocq の内部データ構造 ── ゴール、コンテキスト、証明項 ── にアクセスできます。

結果として、Rocq のタクティクを ELPI の型付き高階論理プログラミングとして書けるのです。

Coq-Elpi のコードを実際に見る

言葉だけでは伝わりにくいので、Coq-Elpi のコードがどんな見た目なのかを２つの小さな例で確かめます（いずれも Coq-Elpi 公式チュートリアルのコマンドを要点だけに切り詰めたものです）。

例 １ ── Rocq の中に λProlog で「あいさつコマンド」を作る

From elpi Require Import elpi.

Elpi Command hello.
Elpi Accumulate lp:{{

  main [str S] :- coq.say "Hello" S.

}}.

Elpi hello "world".   (* 出力: Hello world *)

Elpi Command hello. で hello という新しい Rocq コマンドを作ると宣言し、Elpi Accumulate lp:{{ ... }}. の中身が λProlog のプログラムです。main [str S] は「文字列の引数 S を 1 つ受け取ったら」という Horn 節の頭で、本体の coq.say は Rocq のメッセージ出力機能を ELPI から呼び出す組み込み述語です。Rocq の .v ファイルの中に、いま見てきた λProlog の規則がそのまま同居していることが分かると思います。

例 ２ ── λProlog のプログラムから、Rocq に新しい定義を追加する

Elpi Command define_one.
Elpi Accumulate lp:{{

  main [] :-
    coq.env.add-const "one" {{ 1 }} {{ nat }} @transparent! _.

}}.

Elpi define_one.
Print one.   (* one = 1 : nat *)

coq.env.add-const は「Rocq の環境に新しい定数を追加する」API です。

注目してほしいのは {{ 1 }} や {{ nat }} という書き方です。

これが本文で説明した「クォーテーション」で、二重波括弧の中には Rocq の構文をそのまま書けます。
ELPI 側は内部表現を意識せずに Rocq の項を組み立てられるわけです。

この例はわずか数行ですが、「λProlog の規則が Rocq の内部データベースを書き換える」というメタプログラミングの最小形になっています。

Hierarchy Builder は、この仕組みを数千行に積み上げて代数構造の階層を管理しているのです。

Coq-Elpi を核とする Rocq の生態系の主要な構成要素は次のとおりです。

• Coq-Elpi プラグイン ── Rocq の項を HOAS で λProlog に埋め込むための橋渡し
   
• Elpi の API ── Rocq の型検査器、環境、定理データベースへのアクセスの窓口
   
• Hierarchy Builder（HB、ハイアラーキ・ビルダ）── 代数構造（群、環、体、ベクトル空間など。数学で扱う「演算の規則を備えた集合」たち）の階層を Rocq の中で宣言的に組み立てるツール。ELPI ベース
   
• Coercion（コアーション）── 型変換の自動化を ELPI でプログラム可能に
   
• Record builder（レコード・ビルダ）── レコード型の柔軟な構築と更新の構文を ELPI で実現
   
• Locker（ロッカー）── 定義の計算内容を隠す仕組み
   
• Namespace Emulation System ── 名前空間の機能を Rocq のモジュール上に実装
   
• Trakt（トラクト）── 証明自動化のための汎用のゴール前処理ツール
   
• Algebra Tactics（代数タクティク）── ring や field のタクティクを Mathematical Components ライブラリに移植したもの

これらすべてが、λProlog/ELPI を核とする Rocq の一つの生態系を形づくっています。

実務での用途 ２ ── Hierarchy Builder、mathcomp の階層構造を支える

Coq-Elpi の力を最もはっきりと世界に示したプロジェクトが、Hierarchy Builder（ハイアラーキ・ビルダ、階層構築器）です。

Hierarchy Builder は、Cyril Cohen、Kazuhiko Sakaguchi（坂口 和彦）、Enrico Tassi の 3 氏が 2020 年開催の FSCD 会議で発表した、Rocq 上で代数構造の階層（モノイド、群、環、体、ベクトル空間など）を宣言的かつ機械的に管理するためのフレームワーク です。

• 論文 ── Cyril Cohen、Kazuhiko Sakaguchi、Enrico Tassi. "Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi", FSCD 2020.

Hierarchy Builder は、mathcomp（Mathematical Components。Rocq 上での代数と数学の主要なライブラリで、Georges Gonthier らが「Feit-Thompson の定理」── 有限群論の記念碑的な大定理 ── の形式化のために開発したもの）の階層構造を支える基盤として使われています。Hierarchy Builder のコードそのものが λProlog/ELPI で書かれています。

Hierarchy Builder が示したのは、単に便利なフレームワークの存在ではありません。「Rocq 自身の複雑なメタプログラミングを λProlog/ELPI で綺麗に書ける」という事実が、実地で証明されたのです。

実務での用途 ３ ── Abella、プログラミング言語理論の証明系

λProlog の設計者である Dale Miller と Gopalan Nadathur は、λProlog の学術的な発展として、対話的定理証明系 Abella（アベラ）の開発を主導してきました。

Abella は、David Baelde、Andrew Gacek、Gopalan Nadathur、Yuting Wang、Kaustuv Chaudhuri、Dale Miller、Alwen Tiu の 7 氏による共同開発の対話的定理証明系です。

• 論文 ── David Baelde 他. "Abella: A System for Reasoning about Relational Specifications", Journal of Formalized Reasoning, 2015 年.

Abella の中核にあるのは、λ-tree syntax（ラムダ木構文。HOAS の別名としてよく使われる呼び方です）による、束縛変数を含む構文の自然な扱いです。

Abella が得意とするのは、プログラミング言語の意味論、型システムの健全性、λ計算（ラムダ計算）の性質、π計算（パイ計算。並行して動くプログラムどうしのやり取りを扱う理論的枠組み）などです。特に λ計算とπ計算のメタ理論（その体系そのものの性質を論じる理論）の形式化で、Abella は優れた成果を挙げています。

Abella の背後には、Rockwell Collins（米国の航空宇宙・防衛企業）、INRIA、University of Minnesota、Nanyang Technological University（シンガポール）の研究者たちの共同研究があります。

実務での用途 ４ ── Makam、プログラミング言語理論の実装向け

Antonis Stampoulis（アントニス・スタンプーリス、当時 Yale 大学の博士課程学生）が開発した Makam（マカム）は、λProlog の設計思想をプログラミング言語理論の実装のために洗練させた言語です。

Makam は OCaml で書かれた λProlog の実装で、「新しいプログラミング言語を設計し、その意味論を形式化し、実装する」という試作（プロトタイピング）の作業に特化した機能を持っています。

Makam が提供するのは、「型システムを設計して機械的に検査する」「言語の動作の規則を、教科書に載る記法（構造的操作意味論と呼ばれます）に近い形でそのまま書く」といった、プログラミング言語理論の研究者が日々行う作業を λProlog の枠組みの中で素早くこなせる環境です。

この４つの他にも ── POPLMark reloaded、MLTS、Elpi の Web 実行

上記の４つに加えて、λProlog/ELPI は次の場面でも活躍しています。

• POPLMark reloaded ── プログラミング言語のメタ理論の形式化を評価するためのベンチマーク（性能や表現力を競う共通課題）です。λProlog/ELPI はこのベンチマークの主要な参加者の一つとして、プログラミング言語理論の学術研究に貢献しています。
   
• MLTS ── ML（Meta Language。OCaml や F# の源流にあたる言語の系譜）の型システムを λProlog で実装したものです。実用的な型システムの実装を体験できる、λProlog の貴重な教材です。
   
• Elpi の Web ブラウザ上での実行 ── ELPI は OCaml で書かれているため、js_of_ocaml というツールで JavaScript に変換すれば Web ブラウザの中で実行できます。オンラインの Elpi Playground と MLTS のデモは、λProlog の力をブラウザで直接体験できるリソースです。

４つの実務用途を俯瞰すると

Coq-Elpi、Hierarchy Builder、Abella、Makam の 4 つを俯瞰すると、λProlog/ELPI の実務での位置付けが明確に見えてきます。

λProlog/ELPI は「定理証明系の内部で、その系自身のメタプログラミングを担う言語」であり、「プログラミング言語の意味論や証明の形式化を支える基盤言語」なのです。

これらはいずれも、束縛変数、高階論理、メタプログラミング、型システムの厳密な扱い ── λProlog が最初から得意としてきた領域です。

Miller と Nadathur が 1987 年に λProlog を設計したときの動機 ──「プログラミング言語や論理体系の意味論を、機械的に扱えるプログラミング言語を作ろう」── は、38 年後の 2025 年に、Coq-Elpi、Hierarchy Builder、Abella、Makam という具体的な実務プロジェクトの中で、はっきりと実を結んでいるのです。

---

節 5（AI との接点）── λProlog は、AI Agent 時代にどんな役割を担うのか

2024 年から 2026 年にかけて、AI Agent（人間の指示を受けて自律的にタスクをこなす AI システム）と定理証明系の接点が急速に注目を集めるようになりました。

その代表格が、以下の中国発のプロジェクトです。

• DeepSeek-Prover（ディープシーク・プルーヴァ）── DeepSeek AI が開発した、Lean 4 を用いた自動定理証明の大規模言語モデル。数学の問題文を渡すと、Lean 4 の証明コードを丸ごと書き上げます。書いた証明は Lean 4 が検査し、合格した証明だけをお手本として学習し直す ── この自己改善の繰り返しによって、高校からオリンピック級までの問題集で高い正答率に到達しました
   
• Kimi-Prover（キミ・プルーヴァ）── Moonshot AI が開発した、Lean を用いた自動定理証明の高性能なモデル。人間の答案のようにまず「解く筋道」を長い思考として書き出し、その筋道に沿って Lean の証明を組み立てていくスタイルが特徴です
   
• REAL-Prover（リアル・プルーヴァ）── 中国国内の研究者による、検索補強型（retrieval augmented）の Lean 向け証明生成システム。証明の途中で「いま使えそうな既存の定理」をライブラリから検索して取り込みながら一手ずつ進める、人間が公式集を引きながら問題を解くやり方に近い方式を採ります

いずれも Lean 4 を主なターゲットとした「AI × 定理証明」のプロジェクトです。

３者に共通する骨格は「AI が証明の候補を書き、Lean 4 が厳密に検査し、不合格なら書き直す」というループであり、本記事の冒頭から見てきた「生成と検査の組み合わせ」が、そのまま実装されています。

率直な問い ── AlphaProof や DeepSeek-Prover で、Coq-Elpi は使われているのか？

冒頭からここまで読んでくださった方なら、当然この疑問が浮かぶはずです。答えを正直に言うと、使われていません。AlphaProof も DeepSeek-Prover も Kimi-Prover も、対象の定理証明系は Rocq ではなく Lean 4 です。

なぜ Lean 4 なのでしょうか。本記事執筆者は、主に３つの理由があると考えます。

理由 １ ── Mathlib という一枚岩の数学ライブラリ

Lean 4 には、現代数学の広い範囲を一つの巨大ライブラリに集めた Mathlib があります。

AI の学習には大量のお手本（証明のデータ）が必要で、統一された流儀で書かれた Mathlib は理想的な教材でした。

理由 ２ ── 競技数学ベンチマークとの相性

AI の証明能力は、数学オリンピック級の問題集（miniF2F など）で測るのが通例になっており、こうしたベンチマークは Lean を中心に整備されています。

AlphaProof が 2024 年の国際数学オリンピックの問題で銀メダル相当の成績を収めたのも、Lean 4 の上でのことでした。

理由 ３ ── 数学の形式化コミュニティの勢い

Terence Tao や Kevin Buzzard といった著名な数学者が Lean での数学の形式化を牽引しており、「AI × 数学」の話題は自然と Lean に集まる構図があります。

では、Rocq と Coq-Elpi はこの潮流の蚊帳の外なのでしょうか。
そうではない、というのが本記事の見立てです。

理由を３つ挙げます。

第１に、Rocq を対象にした証明自動化や機械学習の研究も続いているからです。
Rocq には CompCert（検証済み C コンパイラ）や mathcomp といった、Lean 側には無い種類の巨大な資産 ── 検証済みソフトウェアと、その証明群 ── があり、これを扱える AI への需要は確実に存在します。

第２に、勝負どころが違います。
Lean × AI の主戦場は「数学の問題を解く」ことです。

一方、Rocq の伝統的な強みは「ソフトウェアの正しさを証明する」ことにあります。

AI がソフトウェア検証の証明を書く時代が来るとき、その舞台の一つは Rocq であり、Rocq のタクティクと自動化の層 ── まさに Coq-Elpi の持ち場 ── が AI との接続面になります。

第３に、対比そのものに学びがあります。

Lean 4 は、自分自身のメタプログラミングを Lean 4 で書くという設計を選びました。

Rocq は、束縛変数と高階論理の扱いに最初から強い λProlog を、拡張言語として丸ごと迎え入れる設計を選びました。

同じ課題に対する２つの異なる設計解であり、λProlog を学ぶことは、この設計判断の意味を理解することでもあります。

では λProlog は、この潮流の中でどんな役割を担うのでしょうか。

役割 １── Rocq との接点

λProlog/ELPI の主要な用途は、Rocq の拡張言語 Coq-Elpi です。
Rocq は Lean 4 と並ぶ、世界の主要な定理証明系の一つです。

AI が Rocq の証明を自動生成する場面で、AI が生成するのは多くの場合 Rocq のタクティクです。
そのタクティクをより強力に、より安全に書くための拡張言語が Coq-Elpi です。

つまり、λProlog/ELPI は、AI が Rocq と対話するときの「共通の語彙」の一部になっていくと考えられます。

役割 ２ ── 型の厳密さと、高階論理の力

AI が生成するコードやタクティクの正しさを保証するには、型システムの厳密さが重要です。

λProlog は単純型付きラムダ計算に基づく型システムを持ち、生成された論理式が「型として辻褄が合っているか」をコンパイル時に検査できます。

さらに λProlog の高階論理の力を借りると、「AI が生成した証明が実は間違ったパターンを踏襲していないか」まで、より深い形で検査できます。

役割 ３ ── メタプログラミングによる、証明の変換と最適化

AI が生成する証明はしばしば「動くが無駄が多い」ものです。

この証明を機械的に変換し、より簡潔に、より汎用的にするには、「証明を操作する証明（メタ証明）」を書ける言語が必要です。

λProlog/ELPI の高階論理と HOAS の組み合わせは、この「証明の変換と最適化」を自然に正しく書くための道具になります。

役割 ４ ── 実務での実例 ── Coq-Elpi と AI の接点

現在、Rocq のコミュニティでは Coq-Elpi を用いた自動化の実験が活発に進んでいます。

• "Deriving proved equality tests in Coq-Elpi"（Enrico Tassi、ITP 2019）── データ型に対する等号判定関数の証明済み導出を Coq-Elpi で自動化
   
• Hierarchy Builder による代数階層の管理（前述）── 代数構造の階層を宣言的に管理
   
• "Determinacy Checking for Elpi"（Davide Fissore、Enrico Tassi 他）── ELPI の決定性（同じ入力に対して結果が一つに定まる性質）を静的解析で検査

これらの実例はいずれも、「AI が生成したコードやタクティクを λProlog/ELPI の型システムと高階論理の力で厳密に検証する」場面への入り口になっています。

AI × 定理証明 × λProlog の処理フロー ── 一枚の図で

AI が生成した証明が λProlog/ELPI を経て、Rocq の Kernel（カーネル、型検査器）で検証されるまでの流れを一枚の図で整理します。
（図中の LLM の枠に挙げた各プロジェクトは、前述のとおり現時点では Lean 4 を対象としています。この図は「Rocq を対象に証明を生成する場合」の役割分担を示した概念図として読んでください）

同じ流れを表形式でも整理します。

ステップ	担い手	処理内容
1	LLM（DeepSeek-Prover、Kimi-Prover、REAL-Prover 等）	証明したい定理を入力として受け取り、タクティク候補を生成
2	ELPI（λProlog インタープリタ）	生成されたタクティク候補を、単純型付きラムダ計算の型システムで検査。高階論理と HOAS の力で厳密に検証
3	Coq-Elpi（Rocq プラグイン）	検証済みのタクティクを、Rocq の内部データ構造（項、ゴール、環境、evar）に適用
4	Rocq 本体	タクティクを実行し、証明項を段階的に組み立てる
5	Kernel（カーネル、型検査器）	完成した証明項が定理の型を実現しているかを検査
6	検証済みの証明	型検査に通れば、機械が検証した証明として認められる

この流れの中で λProlog/ELPI が担うのは、「AI の生成した候補を型システムと高階論理の力で厳密に検証してから Rocq に渡す、フィルタと変換の層」 です。

AI が生成する候補は、しばしば「動くように見えて実は間違っている」ものです。

この間違いを Rocq 本体に持ち込まれる前に λProlog/ELPI の型システムで捕まえることが、AI × 定理証明の実務での品質を高めます。

「検証してから渡す」をコードで見る

「候補を検証してから Rocq に渡す」という役割分担を、Coq-Elpi でタクティクを書く最小の例で確かめます（Coq-Elpi チュートリアルの書き方に沿った例です）。

Elpi Tactic try_reflexivity.
Elpi Accumulate lp:{{

  solve (goal _ _ {{ _ = _ }} _ _ as G) GL :-
    refine {{ eq_refl }} G GL.

  solve _ _ :-
    coq.error "等式の形のゴールにだけ使えるタクティクです".

}}.

Goal 1 + 1 = 2.
Proof. elpi try_reflexivity. Qed.

solve はタクティクの本体を表す述語で、第１引数に「いまのゴール」が渡されてきます。

１つ目の規則の頭にある {{ _ = _ }} に注目してください。

単一化の力で「ゴールが等式の形をしているときだけ」この規則が発動し、refine {{ eq_refl }} ──「左右は同じものだ」という証明の断片 ── をゴールにあてはめます。

ゴールが等式の形でなければ１つ目の規則は単一化に失敗し、バックトラックで２つ目の規則に落ちて、分かりやすいエラーを出します。

つまり、「ゴールの形を検査してから証明の断片を適用する」という門番の仕事が、単一化とバックトラックというλProlog の基本動作だけで書けているわけです。

AI が生成したタクティク候補をふるいにかけてから Rocq に渡す、という本節の処理フローは、この門番を大規模にしたものだと考えてください。

AI 時代の学習価値

AI が生成したコードの正しさをどう保証するかは、今後の実務で重要な問いです。

F*（F Star）について、本記事執筆者が記した記事 「F*（F Star）とは何か ── Firefox・Linux・WireGuard で動く「証明済みコード」を書けるプログラミング言語早わかり」でも同じ論点を提示しましたが、λProlog/ELPI は Rocq の内側で、この問いに答える道具の一つとして既に立っています。

λProlog を学ぶことは、単に一つの言語を学ぶことではありません。

「AI 時代における、機械が検証できる正しさとは何か」という、実務と学問の両方で重要な問いに正面から向き合うことにつながるのです。

---

応用編 その 1 ── λProlog を支える 8 つの概念

ここまでは、冒頭で掲げた 5 つの問い ── なぜ生まれたか、Prolog との違い、HOAS を使う理由、Coq-Elpi や Abella などでどう使われているか、AI・定理証明との接点 ── を軸に λProlog の全体像をつかんでいただきました。

ここからは記事の締め括りに向けて、λProlog を支える 8 つの概念を整理します。本文の中で一つずつ説明してきた言葉たちの、まとめの一覧でもあります。

1. 論理型プログラミング（logic programming）

「解きたい問題を論理的な事実と規則の集まりとして書き、コンピュータに解を探させる」プログラミング・スタイルです。代表的な言語は Prolog です。Python の「値を受け取り値を返す関数の連なり」とは根本的に異なる発想です。

この後の各項でも「述語（predicate）」という言葉が繰り返し登場するので、改めて確認しておきます。

述語とは「引数を受け取って真か偽かを返す関数」のことです。

Python でいえば def is_even(x: int) -> bool: return x % 2 == 0 のような関数が、そのまま述語にあたります。

論理型プログラミングでは、この述語を宣言的に書き、推論エンジンがその述語を成り立たせる値を自動的に探してくれます。

2. Horn 節（Horn clause、ホーン節）

「$A$ かつ $B$ ならば $C$」の形をした論理式の一形式です。

Prolog のプログラムは Horn 節の集まりとして書かれます。
推論エンジンは Horn 節を機械的に組み合わせて答えを導き出します。

3. 一階論理（first-order logic）

「すべての〜について」の「〜」に、値（データ）しか入れられない論理です。

Prolog はこの一階論理の中で推論します。「すべての $x$ について $x + 0 = x$」は書けますが、「すべての関数 $f$ について〜」は書けません。

4. 高階論理（higher-order logic）

「すべての〜について」の「〜」に、関数や述語まで入れられる論理です。

λProlog はこの高階論理の中で推論します。

「すべての述語 $P$ について〜が成り立つ」という文が自然に書けます。

プログラミング言語や証明の意味論を機械的に扱う場面で、この表現力の違いが大きく効いてきます。

5. 単純型付きラムダ計算（simply typed lambda calculus）

1940 年に Alonzo Church（アロンゾ・チャーチ、Princeton 大学）が提案した関数の抽象化と適用を厳密に扱うための数学的な体系です。

「型を持つ関数」を数学として扱えるように整えたものです。

λProlog の型システムはこの体系に基づいています。

関数型プログラミング言語（Haskell、OCaml、F# など）の型理論の源流でもあります。

6. 高階抽象構文（HOAS、Higher-Order Abstract Syntax）

束縛変数の扱いを、宿主言語（λProlog 自身）のラムダ抽象に委ねる技法 です。

節 3（HOAS） で詳しく解説しました。

プログラミング言語の意味論や証明系の内部データ構造を機械的に扱う場面で強力です。

7. Hereditary Harrop Formulas（遺伝的ハロップ論理式）

Prolog の Horn 節を、含意と量化子でより自由に拡張した論理式の形式です。

λProlog はこの形式を扱うことができます。

モジュール性、局所的な仮定の導入、名前空間の管理を論理式の中で自然に表現できます。

Harropは、英国の論理学者 Ronald Harrop の名前に由来します。
Hereditaryは「遺伝的」の意味で、含意や量化子で入れ子にされても形式が保たれる性質を指します。

8. Constraint Handling Rules（CHR、制約処理規則）

Thom Frühwirth（トム・フリューヴィルト）が 1991 年頃に提案した、制約解決のためのプログラミング言語 です。

ELPI は λProlog の標準にこの CHR を独自拡張として加えているため、厳密には「λProlog の方言」と位置付けられます。

「まだ決まっていない部分は制約として持ち越しながら、決められるところから計算を進める」という洗練された実行モデルを実現します。

補足 ── 論理型プログラミングを支える「単一化」と「バックトラック」

上記の８つの概念を、論理型プログラミング全般を支える２つの実行モデル
──「単一化（unification）」と「バックトラック（backtracking）」
── が下支えしています。

記事の前半でも説明しましたが、大切な概念なのでここで改めて確認します。

単一化 とは、２つの論理式（あるいは項）を照合し、両者が一致するように、まだ値の決まっていない変数の値を決める仕組みです。

Python でいえば {"name": "太郎", "age": 30} と {"name": X, "age": 30} を見比べて X = "太郎" と決めるイメージです。

Python のパターン・マッチング（Python 3.10 以降の match 文）に、双方向性（左辺と右辺のどちらの変数が未定でもよい）を加えたものとも言えます。

バックトラック とは、「ある選択が失敗したら直前の分岐点に戻って別の選択を試す」実行モデルです。

迷路で行き止まりに突き当たったら分岐点まで引き返す、あの発想です（アルゴリズムでいう深さ優先探索〈DFS〉にあたります）。

Prolog と λProlog は、この単一化とバックトラックを基本の実行モデルとしています。

単一化とバックトラックを、コンパイラや証明系の内部データ構造の変換に応用する
── これが λProlog が実務で選ばれる大きな理由の一つです。

λProlog の立ち位置

以上の８つの概念に照らすと、λProlog はどこに位置するのでしょうか。

λProlog は、論理型プログラミング言語であり、高階論理プログラミング言語であり、単純型付きラムダ計算に基づく型システムを持ち、高階抽象構文（HOAS）による束縛変数の自然な扱いを言語の中核に据え、Hereditary Harrop Formulas を扱える ── という複数の性格を併せ持つ希少な言語です。

実装の ELPI はこれらすべてに加えて、Constraint Handling Rules（CHR）による制約解決の枠組みを持ち、他のアプリケーションに組み込むことを目的に OCaml で書かれています。

この組み合わせが、λProlog/ELPI を、Rocq の拡張言語、mathcomp の Hierarchy Builder、対話的定理証明系 Abella、プログラミング言語理論の Makam ── これらの実務用途で唯一無二の存在にしているのです。

---

応用編 その 2 ── λProlog/ELPI のコード実例

ここまでの解説を踏まえて、λProlog/ELPI のコードが実際にどう見えるかを確かめます。

Prolog は SWISH（SWI-Prolog のブラウザ版。https://swish.swi-prolog.org/ ）で、λProlog/ELPI は前述の Elpi Playground で、それぞれインストールなしに試せます。

読むだけより手を動かす方が何倍も身につくので、ぜひ写して実行してみてください。

コード例 1 ── リストの反転（Prolog と λProlog の対比）

まず、リストを反転する述語を Prolog と λProlog の両方で書き比べます。

Prolog のコード：

reverse([], []).
reverse([X|Rest], Reversed) :-
    reverse(Rest, RestReversed),
    append(RestReversed, [X], Reversed).

λProlog/ELPI のコード：

kind list type -> type.
type nil list A.
type cons A -> list A -> list A.

pred reverse i:list A, o:list A.
pred rev_helper i:list A, i:list A, o:list A.

reverse L R :- rev_helper L nil R.
rev_helper nil Acc Acc.
rev_helper (cons X Rest) Acc R :- rev_helper Rest (cons X Acc) R.

λProlog の方は kind と type でリストの型を明示的に宣言しています。pred では述語の引数の型と、入力（i:）/出力（o:）を宣言しています。この型宣言が、Prolog にはない λProlog の力です。

コード例 2 ── 高階述語の実例

λProlog の力が真価を発揮する場面の一つが、高階述語（higher-order predicate。他の述語を引数として受け取る述語）です。

例として「リストの中の、ある条件を満たす要素だけを取り出す」述語を λProlog で書きます。

pred filter i:(A -> prop), i:list A, o:list A.

filter _ nil nil.
filter P (cons X Rest) (cons X Filtered) :-
    P X, !, filter P Rest Filtered.
filter P (cons _ Rest) Filtered :-
    filter P Rest Filtered.

この filter 述語は、P という述語そのものを引数として受け取っています。Python の filter() 関数に判定用の関数を渡すのと発想は同じです。ただし Python では関数を渡すのに対し、λProlog では述語を渡します。これが高階論理の力です。

コード例 3 ── HOAS の実例（ラムダ計算の実装）

λProlog の HOAS の力が最もはっきり現れるのが、ラムダ計算そのものを λProlog で表現する場面です。

kind term type.
type app term -> term -> term.
type lam (term -> term) -> term.

pred beta i:term, o:term.

beta (app (lam F) X) R :- beta (F X) R.
beta X X.

この短いコードに、λProlog の HOAS の力が凝縮されています。

type lam (term -> term) -> term. は「ラムダ抽象とは、term から term への関数を受け取って term を返すもの」という型宣言です。この時点で、束縛変数の管理を λProlog 自身のラムダ抽象に委ねているわけです。

beta (app (lam F) X) R :- beta (F X) R. は「（λx. F(x)）を X に適用したものを F(X) へと計算し進める」という β 簡約の規則です。F X という書き方が λProlog 自身の関数適用であることに注目してください。この書き方のおかげで、変数捕獲の回避や α 変換の管理といった細かな配慮が、すべて λProlog の言語機能に組み込まれます。

同じことを Prolog で書こうとすると、変数の名前管理、α 変換の実装、代入の実装 ── これらすべてを書き手が自分で管理することになります。λProlog なら、この数行で済むのです。

この違いこそが、λProlog が Coq-Elpi をはじめとする定理証明系の内部で選ばれている根本的な理由です。

---

応用編 その 3 ── λProlog が、特に威力を発揮するユースケース

λProlog が特に強い力を発揮する実務のユースケースを 4 つに整理します。

ユースケース 1 ── Rocq のタクティクや拡張の開発

Coq-Elpi プラグインを通じて、新しいタクティクや証明自動化ツールを宣言的に簡潔に記述できます。

Hierarchy Builder のような大規模な数学ライブラリの拡張も λProlog/ELPI で記述されています。

このユースケースが実務でどれほどの規模の作業を扱えるかを実感していただくために、具体例を３つつ紹介します。

具体例 １ ── mathcomp の代数階層構築

mathcomp（ Mathematical Components ） は Rocq 上での代数と数学の主要なライブラリで、Georges Gonthier らが Feit-Thompson の定理の形式化のために開発しました。

この mathcomp には、モノイド、群、環、体、ベクトル空間、多元体、代数閉体など、数百の代数構造の宣言が含まれています。

この数百の代数構造の階層関係を綺麗に管理するのが Hierarchy Builder（HB） です。

その内部実装は数千行の λProlog/ELPI のコードで書かれています。
この規模のメタプログラミングを Ltac（Rocq の伝統的なタクティク言語）で書くことは、実務上困難です。

具体例 ２ ── データ型に対する等号判定関数の証明済み導出

Enrico Tassi 氏（INRIA）が ITP 2019 で発表した*"Deriving proved equality tests in Coq-Elpi"*では、Rocq 上のあらゆるデータ型（帰納型、レコード型、直積型など）に対して等号判定関数（eq_dec）を自動的に導き出す処理を Coq-Elpi で実装しました。

利用者が「このデータ型の等号判定を作って」と指示すると、Coq-Elpi がそのデータ型の構造を解析し、等号判定関数のコードとその正しさの証明を同時に自動生成します。

Python でいえば、クラス定義を読み取って、そのクラス用の等価比較メソッド（__eq__ にあたるもの）を、正しさの証明付きで自動生成するイメージです。

具体例 ３ ── 数百個の Rocq コマンドの自動生成

大規模な数学ライブラリの整備では「似たパターンの命題を数百個、機械的に生成する」作業が日常的に発生します。

Coq-Elpi を使えば、この「命題テンプレートから数百個の Rocq コマンドを自動生成する」処理が宣言的な指示で書けます。

AI が生成した命題群を Rocq に投入するパイプラインでも、Coq-Elpi は重要な役割を担うと考えられます。

AI が Rocq の証明を自動生成する場面では、AI が生成するタクティクを Coq-Elpi の型システムと高階論理の力で厳密に検証できます。AI × 定理証明の実務において、λProlog/ELPI は独特の希少な位置にあります。

産業界との接点 ── この生態系はどこでビジネスに使われているのか

「定理証明なんて研究の話では？」と思われるかもしれないので、この生態系が実際のビジネス課題とどうつながっているかを整理しておきます。

• 検証済み C コンパイラ CompCert（Rocq で検証）は、独 AbsInt 社から商用ライセンスで提供され、航空機など「コンパイラのバグが人命に関わる」産業分野で使われています。コンパイラが仕様どおりに翻訳することが数学的に証明されているため、生成コードの検査工数を大きく減らせることがビジネス上の価値です。
   
• 検証済み OS カーネル seL4（Isabelle で検証）は、防衛・車載などの分野で採用が進んでいます。
   
• 本記事で紹介した Abella の共同研究には、航空宇宙・防衛企業の Rockwell Collins が名を連ねています。安全性が最重要の産業ほど、「テストで確かめた」を超える「証明で保証した」への需要が強いのです。

λProlog/ELPI 自身が製品に直接組み込まれるわけではありません。

その役割は、こうした「証明で守られたソフトウェア」を生み出す証明基盤の側 ── たとえば Rocq の数学ライブラリ mathcomp の階層を Hierarchy Builder として支える ── にあります。

工場でいえば、製品そのものではなく、製品を作るための工作機械を担っている、という位置付けです。

AI が証明を書く時代にこの工作機械の需要が伸びていく、というのが本記事の見立てです。

ユースケース 2 ── プログラミング言語のプロトタイピング

新しいプログラミング言語を設計する場面で、その言語の型システム、意味論、変換規則を教科書の記法に近い形でそのまま実装できます。言語設計の実験や研究に向いています。

Makam はこの用途のために設計された λProlog の派生形です。Antonis Stampoulis 氏が Yale 大学の博士課程で開発した Makam は、プログラミング言語理論の実装のプロトタイピングに特化した機能を持っています。

ユースケース 3 ── 数学の形式化ライブラリの構築

代数構造（群、環、体、多元体、ベクトル空間、多様体など）の階層を λProlog の力で自動的に組み立てられます。

Peter Scholze、Kevin Buzzard、Terence Tao らに代表される、現代数学を機械が検査できる形に書き直していく「数学の形式化」の潮流の中で、Rocq の Hierarchy Builder は重要な役割を果たしています。

mathcomp は、Feit-Thompson の定理（有限単純群の分類の基礎となる定理）の形式化のために Georges Gonthier らが開発した大規模な数学ライブラリです。

この mathcomp の代数構造の階層を綺麗に管理するために、Hierarchy Builder が使われているわけです。

ユースケース 4 ── 学術研究（POPLMark reloaded、Abella）

プログラミング言語のメタ理論の形式化の分野 で、λProlog は主要な参加者の一つとして学術研究に貢献しています。

Abella 定理証明系は、λ計算、π計算（並行計算の理論的枠組み）、型システムの健全性といったプログラミング言語理論の中核的な定理を、λ-tree syntax（HOAS の別名）の力で綺麗に形式化できるようにしています。

---

応用編 その 4 ── λProlog/Coq-Elpi と、他の定理証明・形式検証言語との使い分け（得意分野と不得意分野の比較）

ここまで λProlog/Coq-Elpi の強みを紹介してきました。

公平を期すために、この言語の不得意な領域と、他の定理証明・形式検証言語との役割分担についても包み隠さずお伝えします。

万能の言語は存在しません。

λProlog/Coq-Elpi にも明確な「得意でない領域」があり、その領域では他の言語たちがそれぞれの持ち場で力を発揮しています。

λProlog/Coq-Elpi の得意分野

λProlog/Coq-Elpi が、他のどの言語にも代えがたい強さを発揮する領域は次のとおりです。

• Rocq の内側でのメタプログラミング ── タクティクの記述、拡張機能の実装、宣言的なコマンドの追加
   
• 束縛変数を含む構文の機械的な扱い ── プログラミング言語の意味論の形式化、型システムの実装、証明項の変換。いずれも HOAS の力を借りて自然に書けます
   
• 代数構造の階層の宣言的な構築 ── mathcomp の Hierarchy Builder に代表される「複雑な数学的階層を宣言的に管理する」用途
   
• プログラミング言語のプロトタイピング ── Makam に代表される「新しい言語の型システムや意味論を教科書の記法に近い形で試作する」用途

λProlog/Coq-Elpi の不得意分野

λProlog/Coq-Elpi には、次のような明確な不得意分野があります。

1. 証明そのものを書くこと ── これは Rocq 自身の役割

λProlog/Coq-Elpi は、Rocq の内側でタクティクを書くためのメタプログラミング言語です。定理を証明すること自体は Rocq 自身の言語で行います。λProlog/Coq-Elpi はその証明を支援する道具の側であって、証明そのものを書く言語ではありません。

1. 証明済みコードを実務システムに直接組み込むこと ── これは F*（F Star）の得意分野

λProlog/Coq-Elpi のプログラムを C 言語や WebAssembly に翻訳して、Firefox や Linux カーネルや WireGuard のような実務のシステムで動かすことは、この言語の想定用途ではありません。この用途には F*（F Star）が向いています。詳しくは本記事執筆者のF*（F Star） とは何か ── Firefox・Linux・WireGuard で動く「証明済みコード」を書けるプログラミング言語の早わかり（2026 年 8 月 1 日公開）をご覧ください。

1. 数学の広範な形式化 ── これは Lean 4 の独壇場

Lean 4 の Mathlib のような、現代数学の広い分野を覆う形式化ライブラリは、λProlog/Coq-Elpi の側には蓄積されていません。「フェルマーの最終定理を形式化しよう」「Peter Scholze の Perfectoid Spaces を形式化しよう」という話題で名前が挙がるのは Lean 4 であって λProlog ではありません。λProlog/Coq-Elpi の資産は、あくまで「Rocq の内側でのメタプログラミング」の方向に集中しています。

1. 大規模システムの形式検証 ── これは Isabelle の金字塔

OS カーネル全体の機能的正しさを証明した seL4 マイクロカーネルは、Isabelle/HOL という定理証明系で検証されました。λProlog/Coq-Elpi はこの規模のシステム検証を単独で担う言語ではありません。「大規模システムの機能的正しさを証明付きで保証したい」という用途には、Isabelle（seL4 の系譜）や Rocq 自身（CompCert 検証済みコンパイラの系譜）が向いています。

1. 型理論そのものの探究 ── これは Agda の得意分野

ホモトピー型理論（HoTT）や Cubical 型理論といった型理論の最先端の研究は、Agda（特に Cubical Agda）という定理証明系を舞台に進んでいます。λProlog の型システムは「単純型付きラムダ計算に基づく、実用のメタプログラミングのための型システム」であって、型理論そのものの新しい地平を探る道具としては設計されていません。

1. 一般のアプリケーション開発 ── Python、Java、Go、Rust などの領域

λProlog は汎用のプログラミング言語ではありません。Web アプリケーション、モバイルアプリ、業務システムといった一般のアプリケーション開発には、Python、Java、Go、Rust、TypeScript といった言語が向いています。

他の定理証明・形式検証言語との比較 ── 全体像

他の定理証明・形式検証言語との比較を表に整理します。

言語	最も力を発揮する領域	代表的な成果・資産	一言での位置付け
λProlog / Coq-Elpi	Rocq の内側でのメタプログラミング、タクティク開発、代数階層の宣言的構築	Coq-Elpi、Hierarchy Builder、Abella、Makam	Rocq の証明を「外側から支援する」拡張言語
Rocq（旧 Coq）	プログラミング言語理論、検証済みコンパイラ、対話的証明	CompCert（検証済み C コンパイラ）、Iris（並行分離論理）、mathcomp	証明そのものを書くための、主体の言語
Lean 4	数学の形式化、汎用プログラミング	Mathlib（現代数学の大規模ライブラリ）、AlphaProof（Google DeepMind）	数学の形式化と、AI × 定理証明の主要な舞台
Isabelle	大規模システム検証、古典的高階論理、強力な証明自動化	seL4（検証済み OS カーネル）、Sledgehammer、AFP（Archive of Formal Proofs）	OS や巨大システムの機能的正しさを証明する言語
Agda	型理論の研究、ホモトピー型理論	Cubical Agda	型理論そのものを探究する研究の道具
F*（F Star）	暗号・通信プロトコル・パーサの証明済み実装	Project Everest、HACL*（検証済み暗号）、EverParse、miTLS	証明済みコードを、実務のシステムに直接組み込む言語

使い分けの指針

将来これらの言語のどれかを選ぶ場面が来たときのために、指針を一言ずつでまとめます。

• 「Rocq の証明を書きたい、その内側でタクティクを拡張したい」 → λProlog/Coq-Elpi
   
• 「Rocq 自身で、定理の証明を対話的に組み立てたい」 → Rocq
   
• 「数学の定理を形式化したい、AI と定理証明系を組み合わせたい」 → Lean 4
   
• 「OS カーネルなどの大規模システムの機能的正しさを、証明付きで保証したい」 → Isabelle（seL4 の系譜）
   
• 「型理論そのものを探究したい、ホモトピー型理論に触れたい」 → Agda（Cubical Agda）
   
• 「動くシステム（Firefox、Linux、WireGuard など）に、数学的な証明を付けて出荷したい」 → F*（F Star）
   
• 「一般の Web アプリや業務システムを書きたい」 → Python、Java、Go、Rust、TypeScript など

一言で言えば

λProlog/Coq-Elpi は「何でもできる言語」ではありません。

しかし「Rocq の内側でメタプログラミングと証明自動化を担う」── この一点にかけては、他のどの言語にも代えがたい道具です。

この一点の希少性は、AI 時代における Rocq と AI の橋渡しという新しい役割によって、これからさらに高まっていくと考えられます。

限界を知ることは、その価値を正確に知ることでもあるのです。

---

応用編 その 5 ── 我が国での λProlog の認知度と、世界各国での存在感

λProlog/ELPI は世界のどこで、どのような形で存在感を示しているのでしょうか。

日本での λProlog の情報発信の状況

日本語圏における λProlog の情報発信として、本記事執筆者が web で確認できたのは次のとおりです。

• 須原 浩道（suharahiromichi）氏による Qiita 記事群（https://qiita.com/tags/λprolog）── λProlog、Coq-Elpi、ELPI のタグで 11 本の技術記事を継続的に発表なさっています。日本語圏での貴重な連続した情報発信です。
   
• 日本の大学の一部での研究 ── 早稲田大学の上田研究室では、LMNtal（同研究室で開発された計算モデル・言語）で実装された λProlog のサブセットの実装研究が発表されています。

しかし、予備知識のない読者向けの日本語の λProlog 入門記事は、これまでほとんど存在してこなかったというのが本記事執筆者の状況評価です。

日本での λProlog の認知度が低い理由 ── 本記事執筆者の見解

日本語圏で λProlog の情報が少ない理由を３つ考えます。

理由 １ ── λProlog の主要な用途が「定理証明系の内部」という深いインフラ層に集中している

λProlog の主要な用途は Rocq の生態系の内部です。Rocq を使わないエンジニアには、λProlog の名前を目にする機会がほとんどありません。

日本の IT エンジニアの主流は Web サービス、業務システム、モバイルアプリの開発であり、定理証明系の内部のメタプログラミングに直接関わる機会は少ないのが実情です。

理由 ２ ── 論理型プログラミング全般の日本での認知度の低下

1980 年代の第五世代コンピュータ・プロジェクト（1982 年開始、1992 年終了）の終了以降、日本の IT エンジニア教育の主流は手続き型・オブジェクト指向・関数型へと重心を移しました。論理型プログラミング全般の学習機会が減ったことも、λProlog の認知度が低い理由の一つと考えられます。

理由 ３ ── λProlog の系譜がフランスと米国に集中している

λProlog は、Dale Miller 氏（現在は INRIA & LIX/École Polytechnique 所属）と Gopalan Nadathur 氏（University of Minnesota 所属）、そして Enrico Tassi 氏（INRIA 所属）の系譜に強く根ざしています。

日本の大学で λProlog を主要な研究テーマとする研究室は限られているのが実情です。

では、日本で認知度が低いとしても、学ぶ価値はあるのか

本記事執筆者の答えは明確に「はい」です。
理由を３つ挙げます。

理由 １ ──「認知度が低い技術」を早期に学ぶことは、実務者としての希少価値を高める

日本語圏で λProlog の情報が少ないということは、裏を返せば、日本で λProlog を実務で扱える人材は希少だということです。

今後、日本の産業でも AI × 定理証明、数学の形式化、プログラミング言語の意味論といった分野で「λProlog/ELPI を扱える技術者への需要」が高まる可能性は決して低くありません。

理由 ２ ── AI 時代における証明自動化の価値の高まり

大規模言語モデルが証明の断片を生成する時代に、その断片を機械が自動的に組み立てて検証する橋渡しとして、λProlog/ELPI は独特の位置にあります。

この分野の実務者になれることは、AI 時代のエンジニアとしての希少な立場を意味します。

理由 ３ ── 日本語圏の空白を埋める、書き手・翻訳者・教育者としての機会

日本語で λProlog を扱える人が増えることは、日本の IT 業界全体の底上げに直結します。日本語での λProlog の書籍、翻訳、記事、講義動画を作れる人への需要は、これから生まれると考えられます。

世界での λProlog の存在感

世界の主要な研究拠点を、本記事執筆者が web で確認できた範囲で整理します。

フランス

• INRIA（フランス国立情報学自動制御研究所）、パリ近郊のオルセーおよびニース（Sophia Antipolis）── Enrico Tassi（ELPI と Coq-Elpi の主要開発者）の所属拠点。
  Dale Miller も INRIA & LIX/École polytechnique に所属し、λProlog と Abella の学術的な中心を担ってきました。INRIA は λProlog の世界的な研究拠点の一つです。

イタリア

• ボローニャ大学（Università di Bologna）── Cvetan Dunchev、Ferruccio Guidi、Claudio Sacerdoti Coen（ELPI の共同開発者）の所属拠点。イタリアの学術界で λProlog/ELPI の実装研究が続けられています。

アメリカ

• University of Minnesota（ミネソタ大学）── Gopalan Nadathur（λProlog の共同設計者）、Yuting Wang（Abella の共同開発者）の所属拠点。Teyjus（λProlog の伝統的な実装）もここが発祥です。
   
• University of Pennsylvania（ペンシルベニア大学）、Duke University、Yale University ── λProlog の学術的な発展に貢献してきた研究者たちの拠点。Makam を開発した Antonis Stampoulis は Yale の博士課程での成果として Makam を発表しました。

中国、ロシア、韓国、インド、イスラエル、ドイツ、オランダ、スイスなどでの、λProlog を主題とする独立した情報発信は、本記事執筆者がweb上で確認できた範囲では限定的でした。

全体を俯瞰すると

λProlog/ELPI は、フランス（INRIA）、イタリア（ボローニャ大学）、アメリカ（University of Minnesota）を中心とする学術研究の緊密なコミュニティに支えられています。その実務での利用は、Rocq、Abella、Makam、mathcomp といった定理証明系とプログラミング言語理論の主要プロジェクトの内部に深く組み込まれています。

そのため λProlog/ELPI は、「エンジニアの間で広く記事が書かれる主流言語」の地位にあるわけではありません。「学術研究と定理証明系の内部で、専門的なコミュニティに支えられて発展する基盤言語」の位置にとどまっている、というのが本記事執筆者の状況評価です。

日本語圏の技術者がこの分野で情報発信をすることは、単に「日本語圏の空白を埋める」以上の意味を持ちます。λProlog/ELPI を実務で扱える人材は、日本でも世界でも希少なのです。

---

応用編 その 6 ── Claude Code、Cursor、Kiro などの Agentic Coding 環境における λProlog サポート

Agentic Coding（AI Agent によるコーディング支援）環境における λProlog のサポート状況は次のとおりです（2026 年 8 月時点、本記事執筆者が web で確認できた範囲での情報）。

Claude Code、GitHub Copilot CLI、Cursor、Kiro などの主要な AI Agent 環境

これらの主要な AI Agent 環境において、λProlog（または ELPI）を明示的に推奨する公式の記述は、本記事執筆者が web で確認した範囲では明確な形では見つけられませんでした。

ただし、Coq-Elpi の重要性

Coq-Elpi の GitHub リポジトリは、Rocq の内側でのメタプログラミングを AI Agent の支援を受けながら進める場面で、重要なリソースです。

大規模言語モデルが Rocq の証明を支援する潮流の中で、Coq-Elpi の役割は今後さらに重要になる可能性があります。

AI が生成した証明の断片を λProlog/ELPI で機械的に検証・組み立てるという営みは、これから急速に成熟する分野と考えられます。

---

応用編 その 7 ── 学習リソース

λProlog を学ぶための主要なリソースを整理します。

1. 公式書籍*"Programming with Higher-Order Logic"*

Dale Miller と Gopalan Nadathur の共著、2012 年、Cambridge University Press。λProlog の理論と実装の決定版です。

2. λProlog 公式サイト

https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/ が公式サイトです。ドキュメント、チュートリアル、論文へのリンクがまとまっています。

3. ELPI GitHub リポジトリ

https://github.com/LPCIC/elpi が ELPI 実装の公式リポジトリです。Enrico Tassi 氏らが Coq-Elpi のチュートリアルを継続的に更新しています。

4. Coq-Elpi GitHub リポジトリ

https://github.com/LPCIC/coq-elpi が Rocq プラグインの公式リポジトリです。Rocq の内側で λProlog を使う実務的な入り口として価値のあるリソースです。

5. Amy Felty 氏のチュートリアル*"λProlog and its Applications to Theorem Proving"*（1997 年）

λProlog を用いた定理証明の実践的な入門として、今も読まれる古典的な資料です。

6. suharahiromichi 氏の Qiita 記事「λProlog （Lambda Prolog） の紹介」（2023 年）

日本語での λProlog の入門記事として貴重なリソースです。

Higher-Order Hereditary Harrop Formulas の解説を含み、須原氏の Qiita にはこの主題の記事が 11 本蓄積されています。

学ぶ方への一言

λProlog を学ぶことは、少なくとも短期的には学習コストが高いです。

論理型プログラミング、高階論理、HOAS、Hereditary Harrop Formulas といった概念を順に身につける必要があります。

しかし λProlog を学ぶと、「推論の規則をそのままプログラムとして書ける」という、他の言語では味わえない独特の体験が手に入ります。

プログラミング言語設計、型システムの実装、定理証明系の内部でのメタプログラミング、AI × 定理証明という、理論と実装が近い場面で λProlog は希少な選択肢です。

この経験は、実務のエンジニアとしての視座を一段階高めてくれるでしょう。

---

応用編 その 8【対話篇】── タロウくんと専任講師の対話：λProlog は、なぜ「Rocq の内側」で選ばれたのか

ここからは対話形式で「λProlog が、なぜ Rocq の内側で選ばれたのか」を考えてみます。

登場するのは、形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界 の登場人物、学部生のタロウくんと専任講師です。

タロウくん
先生、今日は λProlog について書かれた記事を一本読みました。

専任講師
感想を聞かせてくれるかな。

タロウくん
λProlog が Rocq の内側で ── Coq-Elpi として ── 動いている、というのがいちばん驚きでした。

専任講師
それは大きな発見だね。

タロウくん
はい。Rocq と言うと、僕は「証明を書くための専用の言語がある」と思っていました。でも、その Rocq 自身のタクティクやコマンドを書くための拡張言語として λProlog が採用されているとは思ってもいませんでした。

専任講師
そこが、この言語の面白いところだ。

順に整理しよう。

Rocq は証明そのものを書く言語だ。しかし Rocq で複雑な証明を書くときには、「タクティク」と呼ばれる、証明の指示を与える言語を使う。

タクティクを書く言語自体が、実は Rocq の言語とは別に存在する。伝統的には Ltac という言語だった。

タロウくん
Ltac は、Rocq の中で証明を組み立てるための指示言語なんですね。

専任講師
そうだ。

しかし Ltac には限界があった。型がなく、デバッグが難しく、メタプログラミングが不自然だった。

そこで Enrico Tassi（エンリコ・タッシ）が、λProlog の実装である ELPI を Rocq の拡張言語として組み込んだ。それが Coq-Elpi だ。

タロウくん
なぜ λProlog が選ばれたんですか？

専任講師
いい問いだ。

λProlog が選ばれた理由は 3 つある。

第 1 に、λProlog の高階抽象構文（HOAS）が、Rocq の内部データ構造 ── 証明項、論理式、コンテキスト ── を扱うのに自然に適合する。Rocq の内部データ構造は、束縛変数を含むラムダ計算そのもの。この束縛変数を扱うのに、λProlog の HOAS が大きな力を発揮する。

タロウくん
なるほど。Rocq の内部データが、そもそもラムダ計算に近い形をしているんですね。

専任講師
そのとおりだ。

第 2 に、λProlog の高階論理と単純型付きラムダ計算の型システムが、Rocq のタクティクを型のレベルで安全に書けるようにする。Ltac になかった「型による安全性」が、Coq-Elpi では実現される。

タロウくん
Ltac の弱点だった型の問題が、λProlog の型システムで補われるんですね。

専任講師
そうだ。

第 3 に、λProlog の Hereditary Harrop Formulas と、ELPI の Constraint Handling Rules（CHR）が、Rocq の複雑なメタプログラミング ── 例えば mathcomp の代数階層の管理 ── を宣言的に書けるようにする。これが Hierarchy Builder が実現していることだ。

タロウくん
なるほど。3 つの理由が揃って、Rocq の拡張言語として λProlog が選ばれたのですね。

専任講師
そうだ。

さらに言えば、この 3 つはいずれも、1987 年に Miller と Nadathur が λProlog を設計したときの動機 ──「プログラミング言語や論理体系の意味論を、機械的に扱えるプログラミング言語を作ろう」── にそのまま合致している。

λProlog が Coq-Elpi として実務で選ばれたことは、Miller と Nadathur の 38 年前の設計が時を越えて正しかったことの証明でもあるんだ。

タロウくん
あの、先生……正直に言うと、少し弱気になっています。この記事のコードも、web で見られる Rocq や ELPI のコードも、眺めてはみたのですが、何をやっているのか漠然としか読み取れません。目が慣れれば、コードリーディングできるようになるものでしょうか。

専任講師
なるよ。断言する。

思い出してほしい。初めて Python のコードを見た日、for 文や def がすらすら読めたかい？

タロウくん
……読めませんでした。記号の並びにしか見えませんでした。

専任講師
それと同じことが、いま起きているだけだ。文法の系統が Python と違うぶん、最初の壁が少し高く感じられる。それだけのことだ。

読み方には順序がある。私のおすすめはこうだ。

第 1 に、コードの行を 3 種類に仕分けることから始める。「事実」か、「規則」か、「型の宣言」か。kind や type や pred で始まる行は、物語でいえば登場人物の紹介ページだ。まずここを読んで、どんな型とどんな述語が出てくるのかだけを押さえる。

第 2 に、記号 :- を「右側が成り立つなら、左側が成り立つ」と日本語に訳しながら音読する。大文字で始まる名前は「まだ決まっていない未知数」と読む。この 2 つだけで、Prolog 系のコードの骨格は声に出して読めるようになる。

第 3 に、solve や {{ ... }} のような Coq-Elpi 特有の部品は、最初は「決まり文句」として素通りしてよい。全部を一度に理解しようとしないことだ。

タロウくん
決まり文句として素通りして、いいんですか。

専任講師
いいんだ。君は Python の if __name__ == "__main__": を、初日から完全に理解して使っていたかい？

タロウくん
……決まり文句として、写していました。

専任講師
それでいい。理解は後から追いついてくる。

そして何より、読むだけでなく手を動かすことだ。記事に出てきた Playground で、コードの 1 行を書き換えて動かしてみる。事実を 1 つ足して、質問を変えてみる。壊して、直す。この往復を数週間も続ければ、目は必ず慣れる。誰もが通ってきた道だ。

タロウくん
先生、僕、λProlog を学ぼうと思います。

専任講師
うん、いい判断だ。

── ただ、一つだけ覚えておいてほしいことがある。

λProlog が保証してくれるのは、「プログラムや論理式の、束縛変数を含む構造を正しく扱えること」だ。

「その論理式が本当に人間の望んでいた意味を反映しているか」は、依然として人間が担うべき役割であり続ける。

形式手法と要求工学 ── この 2 本の柱の存在を忘れてはいけない。

タロウくん
その 2 本柱は、先生が前にお話しくださった、形式証明の Correctness と Appropriateness の話ですね。

専任講師
そのとおりだ。

λProlog は Correctness ──「実装が仕様通りに動くこと」── の側で強力な道具だ。しかし Appropriateness ──「仕様が人間の意図を反映しているか」── は、いつだって人間が担う責任だ。

タロウくん
胸にとどめておきたいと思います。

---

まとめ

• λProlog は、1987 年に Dale Miller と Gopalan Nadathur が発表した、Prolog を高階論理と単純型付きラムダ計算で拡張した論理型プログラミング言語。「高階抽象構文（HOAS）による束縛変数の自然な扱い」と「単純型付きラムダ計算に基づく型システム」が Prolog との根本的な違いです。
   
• λProlog が生まれた動機は「プログラミング言語や論理体系の意味論を、機械的に扱えるプログラミング言語を作ろう」というものでした。Prolog では、束縛変数を扱う場面で書き手が α 変換、変数捕獲の回避、β 簡約の実装を自分で管理しなければなりませんでした。λProlog はこれらの管理を、宿主言語のラムダ抽象に委ねる HOAS の技法によって、言語が自動で担う仕事に変えました。
   
• λProlog の主要な実装である ELPI は、2015 年に Cvetan Dunchev、Ferruccio Guidi、Claudio Sacerdoti Coen、Enrico Tassi が発表。OCaml で書かれ、他のアプリケーションに組み込むことを目的に設計され、λProlog 標準に Constraint Handling Rules（CHR）を加えた方言です。
   
• λProlog/ELPI の主要な実務での用途は、Rocq（旧 Coq）の拡張言語 Coq-Elpi。Rocq のタクティク、コマンド、そして代数構造の階層（mathcomp を支える Hierarchy Builder）といった Rocq 自身のメタプログラミングが ELPI で書かれています。この他、プログラミング言語の意味論の証明系 Abella、プログラミング言語理論の実装向け Makam などの利用があります。
   
• AI 時代における λProlog の学習価値は高いと考えられます。Coq-Elpi は Rocq と AI を橋渡しする「タクティクの記述言語」として機能します。AI が生成するコードやタクティクを λProlog の型システムと高階論理の力で厳密に検証する場面で、λProlog は独特の強さを発揮します。

λProlog を学ぶことは、AI 時代のエンジニアにとって「機械が検証できる正しさとは何か」という、実務と学問の両方で重要な問いに正面から向き合うことです。この記事がその第一歩の後押しになれば幸いです。

姉妹記事の予告 ── ELPI を、より詳しく

本記事では λProlog という「言語仕様と歴史」を主題として、その全体像をお伝えしました。

しかし λProlog の実装である ELPI は、λProlog 標準に Constraint Handling Rules（CHR）、Rocq との統合、Web ブラウザでの実行、その他さまざまな独自拡張を加えた、豊かな生態系を持っています。

この ELPI の実装と、Coq-Elpi を通じたメタプログラミングの実務については、次の姉妹記事でより詳しく扱う予定です。AI 時代における Coq-Elpi の役割、Hierarchy Builder の実装の内側、mathcomp の代数階層構築の実務といった、より実装寄りの話題を次回お届けします。

---

関連記事

• 論理プログラミングは終わらなかった ── 第五世代コンピュータから LLM / AI Agent / MCP Solver へ（本記事執筆者、2026 年 5 月 19 日）
• 定理証明・形式検証はいまから学ぶ価値があるか（本記事執筆者、2026 年 7 月 23 日）
• Pythonの型ヒントの限界を超える「篩型」入門 ── x > 0 を型に書くと何が起きるのか（本記事執筆者、2026 年 7 月 26 日）
• AI Agent は社会規範に反していても、論理的に正しければ実行可能と判断してしまう ── 「何をしてよいか」を決める責任は、AIが賢くなるほど人間に集中する（本記事執筆者、2026 年 7 月 30 日）
• 形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界（本記事執筆者、2026 年 8 月 1 日）
• F*（F Star） とは何か ── Firefox・Linux・WireGuard で動く「証明済みコード」を書けるプログラミング言語の早わかり（本記事執筆者、2026 年 8 月 1 日）

---

出典

• λProlog 公式サイト https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/
• ELPI GitHub リポジトリ https://github.com/LPCIC/elpi （最新版 v3.7、2026 年 4 月 24 日リリース）
• Teyjus GitHub リポジトリ https://github.com/teyjus/teyjus （最新版 v2.1.1、2023 年 2 月 8 日リリース）
• Coq-Elpi GitHub リポジトリ https://github.com/LPCIC/coq-elpi
• Abella 公式サイト https://abella-prover.org/
• Makam 公式サイト https://astampoulis.github.io/makam/
• Dale Miller ホームページ https://www.lix.polytechnique.fr/Labo/Dale.Miller/
• λProlog 英語版 Wikipedia https://en.wikipedia.org/wiki/%CE%9BProlog
• Dale Miller and Gopalan Nadathur, "Programming with Higher-Order Logic", Cambridge University Press, 2012
• Dale Miller, Gopalan Nadathur, Frank Pfenning, Andre Scedrov. "Uniform Proofs as a Foundation for Logic Programming", ICLP 1988
• Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. "ELPI: fast, Embeddable, λProlog Interpreter", Proceedings of LPAR, 2015 年 11 月, Suva, Fiji
• Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi. "Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi", FSCD 2020
• David Baelde, Andrew Gacek, Gopalan Nadathur, Yuting Wang, Kaustuv Chaudhuri, Dale Miller, Alwen Tiu. "Abella: A System for Reasoning about Relational Specifications", Journal of Formalized Reasoning, 2015 年
• Enrico Tassi. "Elpi: an extension language for Coq", The Fourth International Workshop on Coq for Programming Languages, 2018 年
• Enrico Tassi. "Elpi: rule-based meta-language for Rocq", CoqPL 2025
• Amy Felty. "λProlog and its Applications to Theorem Proving", チュートリアル、1997 年
• 須原 浩道（suharahiromichi）氏、Qiita での λProlog、Coq-Elpi、ELPI 記事群 https://qiita.com/tags/λprolog