MetaPRL とは何か ── computational type theory を土台にした logical framework は何ができて、何ができなかったのか

Last updated at 2026-09-25Posted at 2026-09-14

Executive Summary

本稿の主題

本記事（本稿ということもあります）は、 ひとつの言語を土台にして複数の論理を載せるlogical frameworkというこの仕組み を主題に取り上げます。

本稿は、logical framework には、その土台部分に「型付き」言語を採用する方式 と、「型なし」言語を採用する方式 の ２つがあること に注目し、それぞれの方式の特徴と強み・弱みを比較した結果を論じるもの です。

両方式で、できることと、できないことがどう異なるのか？
両方式で、学術領域や産業領域における使われ方（用途）がどう異なるのか？

【比較対象】

Dedukti（別の記事で詳述済み。本稿でも必要な範囲で分かりやすく解説します）のように、土台部分を「型付き」言語に置いた logical framework（本稿で用語解説をします）
土台部分に「型なし」言語を採用したlogical framework

なお、「型なし」言語 とは、computational type theory という理論を採用した言語 であり、型を割り当てる仕組みが以下の手順を踏む言語 です。

① まずコードを実行させて、実行時のコードの振る舞い方（挙動）を眺める
② あらかじめ定められた「この振る舞い方をするコードは、この型に属すると判断する」という固定ルールを当てはめて、そのコードをどの型に所属させるかを判断する

後者の 「土台部分を型なし言語（computational type theory を採用した言語）に据えた logical framework」 としては、筆者が調べた限り、 MetaPRLのみ でしたが、日本語で読めるウェブ上の技術ブログ記事などは見当たらなかったため、 MetaPRL を主題に取り上げる記事を執筆致しました。

なお、土台部分に「型付き」言語を配置した logical framework としては、 Dedukti があり、本記事執筆者はすでに連載記事（全 6 回予定。現在、4 回目まで Qiita にて公開済み）を執筆中です。

土台部分の言語を「型付き」言語、「型なし」言語のどちらにしたかで、できあがる logical framework の性格や機能（できること、できないこと）や用途がどう変わるのかにご関心をお持ちの方は、本稿と併せて、 Dedukti 連載シリーズもお読みいただけますと幸いです。

なお、この Executive Summary ではこの後、簡潔に、本稿を読み解く上で 必須の専門用語や専門的な概念 について 解説文を掲載 します。

その直後に、土台部分の言語を「型付き」言語、「型なし」言語のどちらにしたかで、できあがる logical framework の性格や機能（できること、できないこと）や用途がどう変わるのか、本稿の結論部分を比較表を添えて掲載します。

なお、型なし言語（computational type theory を採用した言語）の強みのひとつ として、文脈に応じて帰属させる型を切り替える処理を実現させやすいこと に光を当てます。

この処理は、Haskell などの型付き言語でも実現できますが、型なし言語の方が実現させやすいこと を解説します。また、その実用的な意義についても言及します（対話篇3 で取り上げます）。

それでは、本稿を読み解く上で必須の専門用語や専門的な概念について解説に入ります。

MetaPRL とは何か

定理証明支援系 MetaPRL は、定理証明支援系 Nuprl の 型なし の 項言語（term language）を土台 に据え、その上に 一階論理（first-order logic）・集合論・型理論（type theory）など 10種類以上の論理体系を載せて動かす定理証明支援系 です。

なお、型なしの言語 とは、プログラムを実行したときの振る舞い（挙動）を見て、「この振る舞いをするコードは、この型に分類しよう」と判断する言語 です（新しい型の分類ルールを、定理証明エンジニア（人）が定義することもできます）。

computational type theory という型理論が背景 にあります。

computational type theory は別の記事で詳述しましたが、本稿でも後ほど解説します。

「型なし」とは何か

「型なし」という言い方について補足させてください。

「型なし」と書きましたが、プログラムを実行した際のコードの振る舞い方（挙動）を見て、「この振る舞い方をするコードにはこの型を割り当てる」というルールに従って型が割り当てられるので、正確には「型なし」ではなく、「計算した後に、事後的に型が定まる」言語です。

ただし、本記事では、 MetaPRL の設計者 Hickey の博士論文が Nuprl のプログラムを「型なし（untyped）」と呼んでいることに従い、computational type theory を「型なし」と表記します。

「型なしの項に、事後的に型を割り当てる」という考え方は、定理証明支援系のために発明されたものではありません。

ここでいう 項（term）とは、プログラムや命題を記号で書き表した式のこと です。
λx. x + 1 や 2 + 3 のような式が項です。

この考え方の起源 は、Dana Scott が 1976年に発表 した、型なしラムダ計算の数学的モデルに関する研究 に遡ります。

型なしの項の集まりの上 に、「どの項とどの項を同じ型の要素と見なすか」という関係（ 部分同値関係 、partial equivalence relation 、略して PER ）を置くことで、型を後から 定める。

この方法は、その後 PER モデル と呼ばれ、プログラミング言語理論の研究 では広く使われる技法になりました。

しかし、この考え方をそのまま定理証明支援系の型システムとして実装したもの は、筆者が調べた範囲では Nuprl の系統（Nuprl・MetaPRL・RedPRL）以外に見当たりません。

その意味で、computational type theory は定理証明支援系固有のものだと言えます。

出典：D. S. Scott, "Data Types as Lattices", SIAM Journal on Computing 5(3), pp. 522-587, 1976.

📌 中上級者向けコラム：「型なし」は「実行後に型が付く」と同じ意味ではない

本文では初学者向けに、「プログラムを実行した際の振る舞いを見て型を割り当てる」と説明しました。

この説明で伝えたい中心は、項に最初から型注釈が貼り付いているのではなく、項の計算的な振る舞いと型への所属判断が結び付いている、という点です。

ただし、Nuprl 流の computational type theory を、一般的な動的型付き言語の「実行時に型が決まる」仕組みと同一視してはいけません。

JavaScript や Python では、実行時に値のタグを調べて処理します。

Nuprl では、型は 「この項がどのように振る舞うか」を述べる数学的な条件 であり、その条件を満たすかどうかを判断・証明 します。

従って、「型なし」は、型という概念が存在しないという意味ではありません。

本稿では、Hickey が Nuprl の項を untyped と呼ぶ用法に従い、項に事前の型注釈がないという意味で「型なし」と呼んでいます。

computational type theory は定理証明支援系固有のもの

ところで、computational type theory をご存知のエンジニアやプログラマは少ない印象があります。

C/C++・Java・Scala・Rust・TypeScript・Go・Swift・Haskell は、コンパイル時 に型検査される 静的型付き の言語です。

Python・Ruby・JavaScript・Lisp・Clojure・Erlang は、実行時 に型が付く 動的型付き の言語です。

いずれも、型が先にあり、その型に従って値やプログラムが分類 されます。

型なし（厳密には、プログラムが実行されたときの計算の振る舞い方を見た後に、分類ルールに従って型が割り当てられる） の computational type theory は、筆者が調べた範囲では、定理証明支援系固有のもの です。

なぜ computational type theory が Web アプリケーション開発などのフロントエンドの言語や、SQL などのミドルウェアの言語、バックエンドの言語に採用されないのかは、中上級者向けのコラムで、研究者の間で一致した見方と本記事執筆者個人の私見を区別して記載します。

logical framework とは何か

ひとつの言語を土台にして複数の論理を載せる仕組み のことを、logical framework と呼びます。

1987 年に、イギリスのエディンバラ大学の Robert Harper・Furio Honsell・Gordon Plotkin が、複数の論理体系を 1 つの共通の仕組みで定義し実装するために考案した概念 です（先駆として 1967 年のオランダの de Bruijn による Automath があります）。

本記事執筆者が過去に扱った Dedukti と Isabelle も、同じ仕組みです。

しかし、 Dedukti と Isabelle の土台は 型付き の言語で、 MetaPRL の土台は 型なし の言語です。

MetaPRL と Nuprl の関係を層構造で見る

本稿の主題である定理証明支援系 MetaPRL は、別の独立した定理証明支援系 Nuprl（別の記事で解説済み）を構成する 項言語（term language） を、 MetaPRL の 土台部分に取り入れている ため、MetaPRL と Nuprl との関係が、最初は理解しづらいかもしれません

初学者向けに簡略化した概念図を示すならば、この関係 は以下のようになります。

各表は、下の行ほど土台に近く、上の行ほどその上に載る層 です。

なお、定理証明支援系によっては、型理論と言語（項言語）の上下関係（どちらが土台の側で、どちらが土台の上に載せられる側か）が逆に配置されているものがあります。

そのあたりを含めて簡潔に解説します（厳密にはより細かい議論が必要ですが、入門向けの記事を超えてしまいますので本稿では割愛します）。

Rocq や Lean 4 のような一般的な定理証明支援系では、型理論が土台にあり、その上に言語が載ります。

型が先に決まっていて、その型に従って項を書く、という順序 です。

Nuprl は逆です。

Nuprl が採用する computational type theory は、先に項とその計算があり、型はあとから項の振る舞いによって定まる、という順序 です。

したがって Nuprl では、項言語が土台にあり、その上に型理論が載ります。

この違い が、一般的な定理証明支援系の表と Nuprlの表とで、最下段が異なる理由です。

すべての表は、土台を最下段に置く形式で揃えています。

表をご覧になると、（処理系によっては異なりますが）一番下の土台に配置される「型理論」は、言語（項言語など）よりも下の基層に位置付けられるものです。

それでは、最下層（土台）にある型理論は、具体的にはどのプログラミング言語で、コード例としてはどのように実装されるのか、不思議に思われる方もおられるかもしれません。

MetaPRL の型理論を定義するコードは、この後に掲載し、解説を添えます。

各定理証明支援系の層構造と実装言語

【一般的な定理証明支援系の構成要素（層構造）】

以下は、 Rocq・Agda・Idris 2・Lean 4 など一般的な定理証明支援系についての、おおざっぱな言葉の定義です。

層	内容	実装言語
対話環境	定理証明エンジニア（人）がタクティクを与え、型検査器と対話しながら証明を組み立てる環境	型検査器と同じ言語
型検査器	書かれた証明が型理論に照らして正しいかを判定するプログラム	Rocq は OCaml、 Agda は Haskell、 Idris 2 は Idris 2 自身、 Lean 4 は Lean 4 自身と C++
言語	型理論に従って、定義や定理や証明を書き表す言語。項言語とも呼ぶ	各処理系の言語そのもの
型理論	型と項の意味を定める理論。何が正しい証明かを決める	型検査器のプログラムとして実装される

定理証明支援系とは、これらの層を合わせた全体を指します。

型理論は、数学的には紙（概念）の上の推論規則ですが、プログラムとしては型検査器の中に実装されます。

【定理証明支援系 Nuprl の構成要素（3 層構造）】

層	内容	実装言語
システム	項言語と型理論の上で、対話的に証明を組み立てる環境	Common Lisp。制御は ML の変種
型理論	Nuprl 型理論（computational type theory）。型の意味を、項の計算の振る舞いによって定める	Common Lisp の中の推論規則として実装
項言語	項を書き表す言語。型なし	Common Lisp の中のデータ構造として実装

Nuprlだけ、型理論が項言語の上に載っています。

Nuprl が採用する computational type theory は、「先に項とその計算があり、型はあとから項の振る舞いによって定まる」という順序なので、項言語が土台で、その上に型理論が載るのです。

computational type theory（日本語訳としては定まった訳語がありません） を採用する定理証明支援系は、基本的には、「項と計算がまず先にあり、型は、その振る舞い方を分類ルールにあてはめることで事後的に、対応づけられる」順序をとるので、項言語の上に型理論が載る構造です。

なお、Nuprl のソースコードは公開されていません。

ただし、実装言語と規模は公開文献に記されています。
1986 年に Constable らが出版した Nuprl の本によれば、1984 年の初版は約 6 万行の Lisp と数千行の ML で書かれています。

先ほど、それぞれの処理系の型理論を定義しているコードの一部を示す、と述べました。

Nuprl のソースコードは非公開であるため、本稿では Nuprl 自体のコードは引用できません。

そこで本稿は、Nuprl型理論の規則をMetaPRLの上で定義し直したコード を、 MetaPRLのリポジトリから引用します。

MetaPRLのソースコードは GitHub で公開されており、その中の theories/itt/ に Nuprl 型理論の規則がMetaPRLの項言語で書かれています。

Nuprl 型理論をコードとして読める公開資料は、筆者が調べた範囲では、これが唯一です。

2000 年の Allen らの論文によれば、現在の Nuprl 5 も主にCommon Lisp で書かれています。

出典：

R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, S. F. Smith, Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986, Chapter 1 "Overview". https://nuprl-web.cs.cornell.edu/book/Overview.html

S. F. Allen, R. L. Constable, R. Eaton, C. Kreitz, L. Lorigo, "The Nuprl Open Logical Environment", CADE-17, LNAI 1831, pp. 170-176, Springer, 2000.

【定理証明支援系 MetaPRL の構成要素（3 層構造）】

層	内容	実装言語
システム	型検査器と、タクティクによる対話環境	OCaml
対象論理	土台の上に載せる論理体系。 Nuprl型理論・一階論理・CZF・LF・CIC など 10 種類以上。 Nuprl 型理論は、そのひとつとして載る	MetaPRL の項言語で記述。OCaml のソースファイルに埋め込む
土台（メタ言語）	Nuprlの項言語をそのまま使う。型なし。ここに Nuprlとの接点がある	OCaml

MetaPRLの土台 は Nuprlの項言語 であり、 Nuprlの型理論 は MetaPRLの上に載る複数の対象論理の中のひとつ です。

つまり、Nuprl の言語を借り、 Nuprl の型理論を載せ直した、という関係です。

【（比較対象 1）定理証明支援系 Dedukti の構成要素（3 層構造）】

層	内容	実装言語
システム	型検査器 dkcheck。証明項を受け取って自動で再検査する	OCaml
対象論理	土台の上に符号化する論理体系。CIC・HOL・一階論理など。 Lean 4 や Rocq の証明を翻訳して載せる	Dedukti の言語（.dk ファイル）で記述
土台（メタ言語）	λΠ計算 modulo rewriting。型付き	OCaml

対象論理を符号化したコードの一部を示します。

記事「【Dedukti入門 ②】Lean 4 の型理論も HOL Light の高階論理も、なぜ同じ言語で書けるのか ── Dedukti の言語 λΠ計算 modulo rewriting を、実物のコードで読む」で扱った nat.dk からの引用です。

Nat : Type.
z : Nat.
s : Nat -> Nat.

def plus : Nat -> Nat -> Nat.
[n]    plus z n     --> n.
[m, n] plus (s m) n --> s (plus m n).

1 行目で Nat という型を宣言しています。
: Type という型が付いています。土台が型付きであることが、コードに現れています。

【（比較対象 2）定理証明支援系 Isabelle の構成要素（3 層構造）】

層	内容	実装言語
システム	型検査器と、タクティクおよび Isar による対話環境	Standard ML（Poly/ML）
対象論理	土台の上に定義する論理体系。HOL・ZF・FOL など	Isabelle の理論ファイル（.thy）で記述
土台（メタ論理）	Isabelle/Pure。直観主義高階論理の断片。型付き	Standard ML

Isabelle のコードは、記事「依存型を使わないIsabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか」で扱いました。

上記の３つの表は、いずれも、土台・対象論理・システムの3層構造です。
違いは土台部分の「型の有無」にあります。

（この Executive Summary を含めて、本記事は専門的な厳格な議論は避けて、入門者向けに簡略化した説明をさせていただきます）

3つの定理証明支援系の層構造を見比べたところで、 MetaPRLの型理論を定義しているコード を見ましょう。

Nuprl の 型理論の規則は、2種類に分かれます。

種類	内容	例
構造的規則	証明の組み立て方を定める規則。仮定の使用、等しさの対称律・推移律など。型の意味（どんな項がどの型に属するか）には触れない	`equalityAxiom`・`equalityRef`・`equalitySym`・`equalityTrans`
型ごとの規則	各型について「どんな項がその型に属するか」を定める規則。自然数型・関数型・対の型などに、それぞれある。「この振る舞いをする項は、この型に属する」という固定ルールはこちら	`lambdaFormation`・`lambdaEquality`（関数型）など

computational type theory の「振る舞いで型を定める」という考え方を示すのは、後者です。

以下では、後者を取り上げます。

Nuprl 型理論の規則のうち、「この振る舞いをするコードは、この型に帰属する」という固定ルールを定義している部分を示します（ Nuprl 自体のコードではなく、 MetaPRL のリポジトリにあるコードです。

関数型言語の OCaml で書かれています。

厳密には、prim や sequent は OCaml の標準構文ではなく MetaPRL が拡張した構文ですが、ファイルは OCaml のソースファイル（.ml）であり、OCaml のコンパイラで処理されます）。

GitHub の theories/itt/core/itt_dfun.ml から、関数型への帰属を定める 2 つの規則 を引用して紹介します。

prim lambdaFormation {| intro [] |} :
   [wf] sequent { <H> >- "type"{'A} } -->
   [main] ('b['a] : sequent { <H>; a: 'A >- 'B['a] }) -->
   sequent { <H> >- a:'A -> 'B['a] }
   = lambda{a.'b['a]}

prim lambdaEquality {| intro [] |} :
   [wf] sequent { <H> >- "type"{'A} } -->
   [wf] sequent { <H>; a1: 'A >- 'b1['a1] = 'b2['a1] in 'B['a1] } -->
   sequent { <H> >- lambda{a1. 'b1['a1]} = lambda{a2. 'b2['a2]} in a:'A -> 'B['a] }
   = it

【コード解説】

lambdaFormation は、「$A$ の要素 $a$ を受け取ったとき、$B[a]$ の要素を返す、という振る舞いをするプログラムは、関数型 $a:A \to B[a]$ に帰属する」という規則 です。

前提は以下の2つです。

$A$ が型であること
$a$ を $A$ の要素として仮定したときに $B[a]$ の要素 $b[a]$ が作れること

結論は、関数型 $a:A \to B[a]$ に要素が存在することです。
末尾の = lambda{a.'b['a]} が、その要素の中身、つまり「$A$ の要素を受け取って $b[a]$ を返す」というプログラム $\lambda a., b[a]$ です。

lambdaEquality は、「$A$ のどの要素 $a_1$ を入れても、計算結果 $b_1[a_1]$ と $b_2[a_1]$ が $B[a_1]$ の要素として等しい、という振る舞いをする 2 つのプログラム $\lambda a_1., b_1$ と $\lambda a_2., b_2$ は、関数型 $a:A \to B[a]$ の等しい要素である」という規則 です。

プログラムの形（$\lambda$ の中身が同じ文字で書かれているか）ではなく、どの入力に対しても同じ結果を返すか、という振る舞いで、等しさと帰属を定めています。

この 2 つの規則 が、「先に項とその計算があり、型はあとから項の振る舞いによって定まる」という computational type theory の順序を、コードとして書き表したもの です。

詳しくは 対話篇 2 で解説します。

本稿の問い

本稿が向き合う問い は、次の問い です。

Logical frameworkの土台部分に、「型なしの言語」を採用する場合と、「型ありの言語」を採用する場合とで、何が変わるのか？

用途は変わるのでしょうか？

得るものと失うものは変わるのでしょうか？

それぞれの用途や目的から見て、メリットとデメリットは何か？

本稿は、この問いを、比較表や mermaid 図、視覚的なイラスト図を用いながらわかりやすく解説します。

なお、本記事は、computational type theory を主題にとりあげた本記事執筆者の過去の記事と、logical framework を扱った Dedukti の記事と Isabelle の解説記事とが 交差する領域 に切り込む記事です。

比較表

	型なしの土台	型付きの土台
代表	MetaPRL	Dedukti・Isabelle・Edinburgh LF
型検査	決定不能	決定可能
証明の検査	定理証明エンジニア（人）がタクティクで導出を組み立てる	証明項を受け取れば、型検査器が自動で再検査する
型なしの体系（Nuprl の型理論）を載せる	できる。型なしのまま計算しながら扱える	記述はできるが、型なしのまま計算することはできない
型付きの枠組み（LF・CIC）を載せる	できる	できる
他の定理証明支援系の証明を持ち込む	できない	できる
主な用途	大規模システムの検証、複数の論理の関係づけ	証明の相互運用

📌 中上級者向けコラム：型付き／型なしだけで、型検査の決定可能性は決まらない

比較表では、MetaPRL 側を「型検査は決定不能」、Dedukti 側を「型検査は決定可能」と対比しました。これは、この記事で比較する２つの土台の設計を要約したものです。

一般論としては、「型付きなら決定可能」「型なしなら決定不能」とは言えません。

型検査が必ず終わるかどうかは、型注釈の有無だけでなく、等式をどう扱うか、どの計算規則を認めるか、型推論をどこまで行うかなど、型理論全体の設計によって決まります。

MetaPRL の背景にある Nuprl の computational type theory では、型への所属や等しさを扱う判断が一般には決定不能です。

Dedukti は、証明項を自動再検査できるように、決定可能な型検査をもつ λΠ計算 modulo rewriting を土台に選びます。

本文の表は、この設計上の対比を示しています。

本記事の結論

土台に 型付きの言語 を置いた logical framework にしかできないことは、他の定理証明支援系が出力した証明項を持ち込み、型検査器が自動で再検査すること（証明の相互運用、proof interoperability）である。「型なし」の土台では、型検査が決定不能なので、この自動再検査が成り立たない。

土台に 型なしの言語 を置いた logical framework にしかできないことは、 Nuprl の型理論のように、項に型が貼り付いていない体系を、その項の計算をそのまま行いながら扱うこと である。型付きの土台 では、その体系を「データ」として記述することはできるが、項の計算の仕組みを土台の側で作り直さなければならない。

どちらの土台でもできること は、型付きの枠組み（Edinburgh LF・CIC）を対象論理として載せること と、複数の論理体系のあいだの関係を記述すること である。

MetaPRL は、コーネル大学が開発した 分散通信システム Ensemble の検証のために 1996 年に構想 され、1997 年に Nuprl-Light として発表された。1998 年に MetaPRL と改名され、10 以上の論理の実装・自動証明器（automated theorem prover）JProver・コンパイラの形式化（formalization）に使われ、2017 年に凍結 された。Ensemble は、研究に留まらず、BBN・Nortel Networks・NASA が軍事と商用の両目的で使用した。 ただし、 MetaPRL 自体が製品や運用システムに組み込まれたかどうかは、筆者が確認した範囲では分からない。

MetaPRL の開発者 Hickey は、大規模なソフトウェアシステムの検証を念頭に置いて、2 つの機能を MetaPRL に求めた。
1 つは、問題の部分領域ごとに適した論理を使えるように、複数の論理を定義できること。
もう 1 つは、システムを部品に分解して検証した結果を組み合わせられるように、論理どうしの形式的な関係を表現できること。この 2 つを満たす形式システムが、定義上 logical framework であった。

MetaPRL は、数学の形式化 にも使われた。Xin Yu が CZF の上で群の公理から出発して部分群・準同型を形式化し、Klein の四元群を具体例として構成した。また、Bryukhov・Kopylov・Krupski・Nogin が基本的な数論を実装し、その証明を自動化した。

MetaRPL には直接の後継は存在しないが、 Nuprl 5・EventML・OMake・Cedille の基礎理論に、派生物が生き残っている。
MetaPRL は、型なしの言語を土台にした logical framework の、筆者が調べた範囲では唯一の例である。

1 つのプログラムを、文脈に応じて異なる型に帰属させる処理が多く発生する用途では、型なしの土台の方が向いている。
型付きの土台でも、多相型・交差型・部分型といった仕組みを型システムに組み込めば実現できるが、それらを組み合わせると型検査が複雑になり、新しい種類の帰属が必要になるたびに型システムを拡張しなければならない。
型なしの土台では、型システムを拡張せずに、新しい型への帰属を判断として後から与えることができる。

土台に型付きの言語を置くべきか、型なしの言語を置くべきかには、一般的な答えはない。
用途で決まる。
他の定理証明支援系の証明を持ち込んで再検査することが目的なら、型付き の土台を選ぶ。
Nuprlの型理論のような型なしの体系をそのまま扱うことが目的なら、あるいは、文脈に応じて型への帰属を切り替える処理が多い用途なら、型なし の土台を選ぶ。
どちらの用途もないなら、型検査が決定可能で自動化しやすい型付きの土台が、実務では扱いやすい。これは筆者の見解 である。

📌 中上級者向けコラム：「できる／できない」は、実装の絶対的な不可能性を意味しない

本文では、型付きの土台と型なしの土台で「できること」「できないこと」を対比しました。
これは、MetaPRL と Dedukti の設計上の得意分野を初学者向けに見通しよく示すための表現です。

厳密には、型付きの logical framework でも型なしの項をデータとして表し、計算規則を実装することはできます。

反対に、型なしの環境でも型付きの論理体系を記述できます。したがって、ここでの違いは「論理的に絶対不可能か」ではありません。

違うのは、どの処理が土台の機構として 自然に 使えるかです。

Dedukti では、翻訳済みの証明項を型検査器で自動再検査する流れが中心になります。

MetaPRL では、型なしの項を共通の表現として使い、タクティクと推論規則で対象論理を組み立てる流れが中心になります。

結論の比較表

結論を2つの表にまとめます。

【型付きの土台の方が優れている点】

項目	型付きの土台（Dedukti・Isabelle）	型なしの土台（MetaPRL）との比較
型検査	決定可能。必ず有限時間で終わる	型なしの土台では決定不能
証明の再検査	証明項を受け取れば、型検査器が自動で再検査する	型なしの土台では、定理証明エンジニア（人）がタクティクで導出を組み立てる必要がある
他の定理証明支援系との連携	Lean 4・Rocq・HOL Light の証明を翻訳して持ち込める（証明の相互運用）	型なしの土台では、この仕組みが成り立たない
自動化	証明項があれば、人手を介さずに検査が終わる	型なしの土台では、自動化はタクティクによる部分的なものに留まる

【型なしの土台の方が優れている点】

項目	型なしの土台（MetaPRL）	型付きの土台（Dedukti・Isabelle）との比較
型なしの体系を扱う	Nuprl の型理論のような、項に型が貼り付いていない体系を、項の計算をそのまま行いながら扱える	型付きの土台では、データとして記述はできるが、項の計算の仕組みを作り直す必要がある
文脈に応じた型への帰属	1 つのプログラムを、型システムを拡張せずに、文脈に応じて異なる型に帰属させられる	型付きの土台では、多相型・交差型・部分型を型システムに組み込む必要があり、組み合わせると型検査が複雑になる
新しい型の追加	新しい型を定義し、既存の項がその型に属するかを判断として後から与えられる	型付きの土台では、新しい種類の型が必要になると、型システムそのものを拡張しなければならない
プログラムコードの検証	実際のプログラムコードを型なしのまま扱えるので、大規模システムの検証に向く。 MetaPRL は Ensemble の検証のために作られた	型付きの土台では、プログラムに型を付けて符号化する必要がある

結論の各項目と記載箇所

結論の各項目が、本記事のどこで論じられているかを示します。

結論の項目	論じている箇所
型付きの土台にしかできないこと（証明項の自動再検査）	対話篇 1、対話篇 4
型なしの土台にしかできないこと（型なしの体系を計算しながら扱う）	対話篇 3、対話篇 4
どちらの土台でもできること（LF・CIC を載せる、論理の関係を記述する）	対話篇 4、対話篇 7
MetaPRL の歴史（Ensemble、JProver、コンパイラ、2017 年の凍結）	対話篇 6、対話篇 7、対話篇 8
Ensemble の産業利用と、 MetaPRL 自体の産業利用	対話篇 6、対話篇 7
後継（Nuprl 5・EventML・OMake・Cedille）	対話篇 9
MetaPRL が唯一の例であること	対話篇 1、ここまでのまとめ
文脈に応じた型への帰属は型なしが向いていること	対話篇 3
総合判断（一般解なし、用途で決まる）	対話篇 4、ここまでのまとめ
型付きの土台の方が優れている点（表）	対話篇 4、ここまでのまとめ
型なしの土台の方が優れている点（表）	対話篇 3、対話篇 4、ここまでのまとめ
computational type theory が実用言語に採用されない理由	Executive Summary 末尾のコラム
実装言語（Lisp と OCaml）	対話篇 6
pointwise と pairwise	対話篇 5

読者の皆様に伝えたいこと

「計算が先、型が後」という computational type theory の考え方は、型理論の中だけでなく、その型理論を扱う土台の設計にまで貫かれます。 MetaPRL のソースコードは、その一貫性が何を可能にし、何を不可能にしたかを、20 年の開発の記録として残しています。

中上級者向けコラム

📌 中上級者向けコラム：なぜ computational type theory は、実用のプログラミング言語に採用されないのか

（研究者の間で一致した見方）

computational type theory が実用のプログラミング言語に採用されない理由は、型検査の決定不能性 にあります。

computational type theory では、「この項はこの型に属する」という判断が、項を計算した結果の振る舞いによって決まります。等式反映（equality reflection）を認めるため、その判断が有限時間で終わる保証がありません。

実用のプログラミング言語では、コンパイラが必ず有限時間で型検査を終えることが前提です。

型検査が終わらないかもしれない言語では、コンパイルが終わらないかもしれず、ビルドの工程に組み込めません。

型理論の標準的な教科書である Pierce の "Types and Programming Languages"（2002 年）は、実用の型システムの要件として、型検査が決定可能であることを挙げています。

したがって、computational type theory の型検査を、定理証明エンジニア（人）がタクティクで導出を組み立てる形に頼ることは、定理証明支援系では許容されても、ビルドを自動化したい実用言語では許容されません。

この点は、型理論の研究者のあいだで異論のない見方です。

出典：
B. C. Pierce, Types and Programming Languages, MIT Press, 2002, Chapter 1.

（本記事執筆者の私見）

もうひとつ、目的の違い があると筆者は考えます。

実用言語の型システムの目的 は、プログラムのバグを、実行する前に見つけること です。

Int と String を足そうとしたら、コンパイル時に弾く。
そのために型があります。

型は、プログラムを書く人が守るべき制約として、先に置かれます。

computational type theory の型の目的 は、プログラムの性質を証明すること です。

「この関数は、どの自然数を受け取っても自然数を返す」という 主張を、型として書き、その証明を組み立てる。

型は、プログラムについての主張であり、証明の対象 です。

前者では、型が先にあって、それに合うプログラムを書きます。
後者では、プログラムが先にあって、その性質を型として述べます。

この順序の違いが、それぞれの目的に合っています。

実用言語が「型が先」を選ぶのは、バグを早く見つけるという目的に、その順序が合うから です。

なお、動的型付き言語 は、実行時に値の型が決まる点で computational type theory に似て見えます。

しかし、動的型付き言語の型は、値に貼り付いた実行時のタグであり、「プログラムがこう振る舞うからこの型に属する」という判断ではありません。

JavaScript の typeof は値のタグを返すのであって、プログラムの振る舞いを判断しているのではありません。

この違いは、筆者の私見ではなく事実です。

本記事の議論の流れ

本記事の位置づけ

本記事は、筆者が過去に公開した computational type theory の前編・後編（全 2 回）の連載に 関連する独立した記事 です。

記事	タイトル
前編	Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す https://qiita.com/etale_cohomology/items/a830a5ac5013a298fb97
後編	なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜 https://qiita.com/etale_cohomology/items/4035a0b3f4d40766437c
本記事	MetaPRL とは何か ── computational type theory を土台にした logical framework は、何ができて、何ができなかったのか

本記事は、本記事執筆者が過去に書いた記事の内容を前提知識としています。

特に、以下の 3 つの記事で扱った概念は簡単に振り返るのみに留め、詳細部分は公開済みの元記事を参照いただく形をとっております。

それらの記事を読まずに本記事だけを単独で理解することは困難です。

computational type theory の「計算が先、型が後」という順序
先にプログラムがあり、そのプログラムを計算したときの振る舞いによって、あとから型が決まる、という考え方です。
プログラムに型が貼り付いているのではなく、型は「こういう振る舞いをするプログラムの集まり」という条件として与えられます。
定理証明支援系のひとつである Nuprl が採用しています。
equality reflection と型検査の決定不能性
equality reflection（等式反映） とは、「$a$ と $b$ が 等しいという命題の証明があれば、$a$ と $b$ を 計算上も等しいものとして 扱ってよい」という規則です。
この規則を認めると、型検査（type checking）を行う型検査器（type checker）は「等しいという証明がどこかにあるか」を自分で探さなければならなくなり、探索が終わる保証がなくなります。
これが、型検査の決定不能性（undecidability） です。
逆に、必ず有限時間で終わることを決定可能（decidable） と呼びます。
Nuprl とその系統は、この規則を採用しています。

logical framework の仕組み
ひとつの型理論またはメタ論理を土台に固定し、その土台を用いて複数の論理体系を記述できるようにした仕組みです。 Edinburgh LF・Isabelle・Dedukti・MetaPRL がこの仕組みを採用しています。

前提となる記事

本記事では、これらの概念に触れるたびに、どの記事のどの箇所で扱ったかを示します。

本記事について

前提記事に掲げた記事「なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜」では、computational type theory を実際に動かせる定理証明支援系 として、以下の5つ を挙げました。

Nuprl：コーネル大学で 1984 年に公開された定理証明支援系。computational type theory の原型で、以後の 4 つはすべてこの系統に属する
MetaPRL：本記事の主題。 Nuprl の項言語を土台にした logical framework。1996 年に開発が始まり、2017 年に凍結された
RedPRL：カーネギーメロン大学で 2016 年頃に開発された定理証明支援系。Cartesian cubical type theory（ホモトピー型理論の区間 I を扱える型理論のひとつ）を、computational type theory の流儀で実装した
redtt： RedPRL の後継。同じく Cartesian cubical type theory を扱うが、computational type theory の流儀を離れ、型付きの項を直接書く方式に移った
cooltt： redtt の後継。同じく流儀を離れており、正規化を evaluation で行う方式を採る

このうち MetaPRL については、名前と一行の説明を載せただけでした。

本記事は、その MetaPRL を 独立した主題として 扱います。

先に、PRL という略語 を説明します。

PRL は Proof Refinement Logic の略語です。

定訳がないため、本記事では 「証明の精密化の論理」 と訳します（refinement は精密化、詳細化の意）。

証明を、大まかな目標（goal）から出発して、段階的に細かい部分目標（subgoal）へ精密化していく、という 証明の組み立て方 を指します。

コーネル大学の Constable らが 1969 年（アポロ 11 号が人類初の月面着陸を成し遂げた年です）に始めた方法論の名前であり、その方法論を実装したシステムの一族の名前でもあります。

Nuprl は「ν（ギリシャ文字のニュー、new の意）＋ PRL」で、新しい PRL という意味 です。
MetaPRL は「Meta ＋ PRL」です。
「Meta」の由来を明記した資料は、筆者が確認した範囲では見つかりませんでした。

MetaPRL は、PRL という名前のとおり、証明を精密化しながら組み立てる方法論に従っています。

この方法論では、定理証明エンジニア（人）が行う工程と、 MetaPRL が自動で行う工程が、交互に繰り返されます。

工程	担当	内容
1	定理証明エンジニア（人）	証明したい定理を、大まかな目標として立てる
2	定理証明エンジニア（人）	その目標に対して、タクティク（tactic）と呼ばれる命令を選んで与える
3	MetaPRL	その命令に対応する推論規則（inference rule）を目標に適用し、目標をより細かい部分目標に分解する
4	定理証明エンジニア（人）	分解された部分目標のそれぞれに、さらにタクティクを選んで与える
5	MetaPRL	同じく、推論規則を適用して、さらに細かい部分目標に分解する
…		部分目標がすべて自明になるまで、工程 4 と 5 を繰り返す
最終	MetaPRL	すべての部分目標が自明になったことを確かめ、証明を完成させる

たとえば、定理証明エンジニア（人） が「$A$ かつ $B$」という 目標を立て 、dT 0 という タクティクを与えます 。

dT は decompose（分解）のタクティクで、0 は「結論に対して」という指定です。

MetaPRL は、結論「$A$ かつ $B$」の形を見て、intro リソースと呼ばれる規則の登録簿の中から「かつ」の 導入規則（introduction rule） を探し、それを適用して、「$A$」と「$B$」という 2 つの部分目標に分解 します。

次に、定理証明エンジニア（人） が「$A$」に対して タクティクを選び、「$B$」に対して タクティクを選びます。

MetaPRL の 主なタクティク を挙げます。

タクティク	働き
`dT 0`	結論の形（かつ・または・ならば …）を見て、intro リソースに登録された規則から合うものを選び、適用する
`dT n`（n は 1 以上）	n 番目の仮説の形を見て、elim リソースに登録された規則から合うものを選び、適用する
`trivialT`	自明な目標を閉じる。結論が true、仮説に false がある、仮説がそのまま結論に一致する、のいずれかの場合
`nthHypT n`	n 番目の仮説が結論と一致していれば閉じる
`autoT`	`trivialT` に加えて、`dT` などを再帰的に適用して、自動で証明を探す
`rwT`	書き換え規則（rewrite rule。計算規則、computation rule とも）を適用する
`thenT`	2 つのタクティクを順に適用する。タクティクを組み合わせるための関数で、タクティカル（tactical）と呼ばれる
`orelseT`	1 つ目のタクティクが失敗したら 2 つ目を試す。タクティカルのひとつ

「Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す」で見た RedPRL の refine bool/eq/tt は、規則の名前を直接指定するタクティク でした。

MetaPRL の dT は、規則の名前を指定せず、目標の形から規則を自動で選びます。

定理証明エンジニア（人）は、どの規則を使うかを覚えていなくても、dT 0 と書けば MetaPRL が探してくれます。

定理証明エンジニア（人）が担うのは、どのタクティクをどの目標に与えるかを選ぶことです。

MetaPRL が担うのは、選ばれたタクティクに対応する推論規則を探して適用し、部分目標を生成し、最終的にすべてが自明になったことを確かめる作業 です。

どの規則を使うかを定理証明エンジニア（人）が判断し、規則の適用が正しいかを MetaPRL が確かめる、という分担 です。

この分担は、タクティクという命令の列を定理証明エンジニア（人）が書く、という形で行われます。

「依存型を使わないIsabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか」で扱った Isabelle には、タクティク の列を書く方式のほかに、Isar と呼ばれる宣言型の証明記述方式 があります。

Isarでは、証明の各段階で何が成り立つかを、人が読める文の形で書き、その根拠を Isabelle が自動で埋めます。

MetaPRL を含む PRL 系の定理証明支援系は、筆者が確認した範囲では、この宣言型の方式を備えていません。

Nuprl・MetaPRL・RedPRL は、いずれも タクティクの列を書く方式 です。

MetaPRL のユーザーガイドは、タクティクが対話的証明の一般的な推論の仕組みであると述べており、Isar に相当する記述方式には触れていません。

証明は、proof editor と呼ばれる対話的な画面で、タクティクを 1 つずつ与えて組み立てます。

RedPRL の後継である redtt と cooltt は、タクティクではなく、型の付いた証明項（proof term）を直接書く方式 です。

これは Agda や Lean 4 の 項モードと同じで、Isar のような宣言型の記述方式とは異なります。

証明の記述方式の 3 分類（Isar・タクティク・項スタイル） は、「【Arend 連載（最終回）】AIによる数学定理証明プロジェクトは Lean 4 を採用した ── Arend 言語仕様の設計判断は、それでも学ぶ意義はあるか」の第5部で表にまとめています。

大まかな目標から出発し、段階的に細かい部分目標へ精密化していく。
これが PRLの方法論 であり、 MetaPRL は この方法論に従って証明を組み立てます。

対話篇2 で、この分解を定めている推論規則のコードを読みます。

なお、Executive Summary で示した層構造の表について補足します。

一般的な定理証明支援系は、型理論・言語・型検査器・対話環境の 4 層からなります。

型理論は紙の上の推論規則ですが、プログラムとしては型検査器の中に実装されます。

Nuprl・MetaPRL・Dedukti・Isabelle は、いずれも土台・対象論理・システムの 3 層に整理できます。

違いは土台の型の有無と、 Nuprl だけ型理論が項言語の上に載る点にあります。

そのうえで、 MetaPRL は、logical framework でもあります。

logical framework とは、ひとつの型理論またはメタ論理を土台に固定し、その土台を用いて複数の論理体系を記述できるようにした仕組みです。

MetaPRL の場合、土台にあるのは、 Nuprl の式を書き表すための言語です。

式とは、プログラムや命題を記号で書いたものです。この言語で書かれる式は、型を持ちません。

Nuprl が採用した computational type theory では、先に式があり、型はあとから判断で決まるからです。

MetaPRL は、この型なしの式の言語を土台にして、その上に一階論理・集合論・型理論といった複数の論理体系を載せます。

なお、型理論の専門用語では、式のことを「項（term）」と呼びます。
本記事でも、対話篇2 以降では「項」という語を使います。

型なしの型理論（先に式があり、型はあとから判断で決まる型理論） については、本記事執筆者が既に公開した 次の2つの記事 をご参照ください。

筆者の別の連載で扱った Dedukti も logical framework です。

Dedukti の土台は λΠ計算 modulo rewriting という型付きの型理論で、その上に複数の論理を載せます。

構造は同じです。
しかし、土台が異なります。

Dedukti の土台は型付きの型理論で、 MetaPRL の土台は型なしの式の言語です。

「依存型を使わないIsabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか」で扱った Isabelle も、同じ構造 を持っています。

Isabelle/Pure という土台の上に、 HOL・ZF・FOL といった論理を載せます。

Isabelle/Pure は、直観主義高階論理（intuitionistic higher-order logic）のうち含意・全称量化（universal quantification）・等号だけを持つ、型付きのメタ論理（meta-logic）です。

MetaPRL と Isabelle には、深いつながりがあります。

MetaPRL の設計者である Jason Hickey の博士論文（コーネル大学、2001 年）によれば、 MetaPRL のメタ論理は、 Isabelle のメタ論理の考え方を借りて作られました。

ただし、そのまま借りたのではありません。 Nuprl の項が型なしであることに合わせて、型なしの二階 Horn 節（second-order Horn clause）に修正しています。

Horn 節 とは、「$A$ が成り立ち、かつ $B$ が成り立ち、かつ $C$ が成り立つならば、$D$ が成り立つ」という形の論理式です。記号で書けば $A ∧ B ∧ C → D$ です。前提 $A・B・C$ は「かつ」で結ばれ、その全体が「ならば」で結論 $D$ につながります。

前提の数は 0 個以上で、前提が 0 個なら「D が成り立つ」という事実そのものになります。

プログラミング言語 Prolog の基礎になっている形 です。

二階とは、この $A・B・C・D$ の位置に、命題だけでなく「命題を受け取って命題を返すもの」も置ける、という拡張です。

推論規則の「前提が成り立てば結論が成り立つ」という構造を、この形で書き表します。

つまり、 MetaPRL は「型なしにした Isabelle」と言えます。

この修正がなぜ必要だったか は、対話篇3 で扱います。

3つを並べます。

名称	土台（メタ理論）	土台の型	載せる論理
Dedukti	λΠ計算 modulo rewriting	型付き	CIC・HOL・一階論理 …
Isabelle	Pure（直観主義高階論理の断片）	型付き	HOL・ZF・FOL …
MetaPRL	Nuprl の項の上の型なし二階 Horn 節	型なし	Nuprl 型理論・CZF・LF・CIC・HOL・一階論理 …

この違いが、何をもたらしたのか。本記事は、 MetaPRL の一次資料である Jason Hickey の博士論文（2001 年）と、15 名の共著による TPHOLs 2003 の論文を読み、GitHub に残されたソースコードを読んで、その答えを探します。

J. J. Hickey, "The MetaPRL Logical Programming Environment", PhD thesis, Cornell University, Ithaca, NY, January 2001.
https://nuprl-web.cs.cornell.edu/documents/Hickey/Hickeythesis.pdf
J. Hickey, A. Nogin, R. L. Constable, B. E. Aydemir, E. Barzilay, Y. Bryukhov, R. Eaton, A. Granicz, A. Kopylov, C. Kreitz, V. N. Krupski, L. Lorigo, S. Schmitt, C. Witty, X. Yu, "MetaPRL – A Modular Logical Environment", TPHOLs 2003, LNCS 2758, pp. 287-303. DOI: 10.1007/10930755_19.
https://www.cs.uni-potsdam.de/ti/kreitz/PDF/03tphols-metaprl.pdf
jyh/metaprl（GitHub）
https://github.com/jyh/metaprl

はじめに

本記事の細かい論点に入る前に、本記事全体を通して読者の皆様に何を示したいのか、何をお伝えしたいのかを、先に述べます。

本記事は9つの対話篇からなり、それぞれが MetaPRL の一面を扱いますが、9つの対話はすべて、ひとつの問いに向かっています。

その問いとは、以下の問いです。

computational type theory を土台にして logical framework を作ると、何ができて、何ができなくなるのか。

（本記事の主題に入る前に：logical framework とは何か）

logical framework とは、ひとつの型理論またはメタ論理を土台に固定し、その土台を用いて複数の論理体系を記述できるようにした仕組みです。

本記事執筆者が過去に書いた記事「【Dedukti入門 ③】Logical Framework とは何か ── 1967 年の Automath から Isabelle、1987 年の Edinburgh LF、そして Dedukti へ」で詳しく扱いました。

本記事では、その仕組みをご存じであることを前提に話を進めます。

（本記事におけるメインの主張）

この logical framework を、computational type theory を土台にして作ると、何ができて、何ができなくなるのか。 MetaPRL は、その問いに動くプログラムで答えた、筆者が調べた範囲では唯一の例です。

なぜ MetaPRL が唯一なのか。 Dedukti 連載で扱った logical framework は、すべて λΠ計算や Isabelle/Pure といった型付きのメタ言語（meta-language）を土台にしていました。

MetaPRL だけが、型なしのメタ言語を土台にしています。
この違いが、 MetaPRL の強みと限界の両方を決めています。

（この主張を支える 3 つの柱）

（1 本目の柱）

まず、 MetaPRL は、 Nuprl の computational type theory を土台にした logical framework です。

Dedukti と構造は同じです。

土台の上に複数の論理を載せ、論理どうしを関係づけます。

（2 本目の柱）

しかし、土台が型なしなので、 Dedukti とは 用途が違います。

Dedukti は、他の定理証明支援系が出力した証明項を翻訳して、独立に再検査します。

それに対して、MetaPRL が行うのは、 MetaPRLの内部で定義された論理どうしの関係づけ です。型なしの土台を選ぶと、型検査の決定可能性を犠牲にするのと引き換えに、型なしプログラムをそのまま扱えるようになります。

（3 本目の柱）

Nuprl の型なしの項言語を土台にした logical framework という MetaPRL の設計は、コーネル大学が開発した分散通信システム Ensemble を検証する、という具体的な課題から生まれました。

1996 年に構想され、1997 年に Nuprl-Light として発表され、1998 年に MetaPRL と改名されました。2001 年に Hickey の博士論文が、2003 年に 15 名の共著論文が出たあと、20 年の開発を経て 2017 年に凍結されました。

2026 年 7 月には、凍結の事実を明記した historical status banner が GitHub に追加されました。

（読者の皆様に持ち帰っていただくもの）

以上の 3 つの柱から、次のことが言えます。logical framework の用途は、土台の型理論の選び方で決まります。型付きの土台を選べば、証明項を型検査器が自動で再検査できます。型なしの土台を選べば、型なしプログラムをそのまま扱えますが、再検査は定理証明エンジニア（人）のタクティクに頼ることになります。

【対話篇 1】MetaPRL は Dedukti の computational type theory 版か

タロウくん：
Qiita に「なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜」という記事がありますよね？
僕と先生の対話が掲載されている記事です。

その中で名前だけ言及されている MetaPRL ですが、これは、 Dedukti の computational type theory 版 と理解していいですか？

専任講師：
その理解は、半分合っています。

（タロウくんの認識が合っている点）

MetaPRL は、 Nuprl の computational type theory をメタ理論として、その上に複数の論理体系を記述できる logical framework です。

logical framework という概念は、1987 年にエディンバラ大学の Robert Harper・Furio Honsell・Gordon Plotkin が、論文 "A Framework for Defining Logics" で提案しました。

複数の論理体系を1 つの共通の型理論（λΠ計算）の上で定義し、その型理論の型検査器で証明を検査するという仕組みです。

先駆として1967 年にオランダの N. G. de Bruijn が始めた Automath があります。

出典：
R. Harper, F. Honsell, G. Plotkin, "A Framework for Defining Logics", LICS 1987, pp. 194-204. 拡張版：Journal of the ACM 40(1), pp. 143-184, 1993.

Dedukti が λΠ計算 modulo rewriting をメタ理論（meta-theory）として複数の論理を符号化（encoding）するのと構造は同じです。

「【Dedukti入門 ③】Logical Framework とは何か ── 1967 年の Automath から Isabelle、1987 年の Edinburgh LF、そして Dedukti へ」で、logical frameworkの5つの事を比較する表を掲げました。その表に MetaPRL の行を加えると、次のようになります。

名称	ルールブック（メタ理論）	検査するプログラム	ルールブックの型
Edinburgh LF	λΠ計算	Twelf	型付き
Isabelle	Pure（直観主義高階論理）	Isabelle	型付き
Dedukti	λΠ計算 modulo rewriting	dkcheck	型付き
MetaPRL	Nuprl の項の上の型なし二階 Horn 節	MetaPRL	型なし

2003年 に、TPHOLs（Theorem Proving in Higher Order Logics、高階論理における定理証明）という定理証明支援系の国際会議 に MetaPRL の 開発者 15 名による共著論文 が発表されました。

本記事では、以後この論文を「TPHOLs 2003 の論文」と呼びます。

J. Hickey, A. Nogin, R. L. Constable, B. E. Aydemir, E. Barzilay, Y. Bryukhov, R. Eaton, A. Granicz, A. Kopylov, C. Kreitz, V. N. Krupski, L. Lorigo, S. Schmitt, C. Witty, X. Yu, "MetaPRL – A Modular Logical Environment", TPHOLs 2003, LNCS 2758, pp. 287-303. DOI: 10.1007/10930755_19. https://www.cs.uni-potsdam.de/ti/kreitz/PDF/03tphols-metaprl.pdf

TPHOLs 2003 の論文 は、 MetaPRL のことを、以下に示す4種類のシステムを1つに兼ねたもの として説明しています。

LCF 流のタクティクにもとづく対話的証明支援系（interactive proof assistant）
logical framework
論理プログラミング環境
形式手法（formal methods）のプログラミングツールキット

このうち 2 つ目の logical framework という点が、 Dedukti と共通します。

なお、この 4 種類は、いずれも本記事執筆者が別の記事で扱った概念です。

MetaPRL が、それぞれの概念にどう当てはまるのかを、順に示します。

LCF 流のタクティクにもとづく対話的証明支援系
「Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す」で、 RedPRL の refine bool/eq/tt というタクティクを見ました。タクティクとは、定理証明エンジニア（人）が証明の手順を命令として書く方式で、1979 年のエディンバラ大学の LCF に由来します。 MetaPRL のタクティク（dT 0 など）は、 RedPRL のタクティクと同じ LCF 流の方式です。
logical framework
「【Dedukti入門 ③】Logical Framework とは何か ── 1967 年の Automath から Isabelle、1987 年の Edinburgh LF、そして Dedukti へ」で、logical framework を**「ひとつの型理論を土台に固定し、その上に複数の論理を載せる仕組み」と定義** しました。
MetaPRL は、その定義に当てはまる定理証明支援系のひとつ です。
論理プログラミング環境
「λProlog とは何か ── AI が数学を証明する時代、定理証明系 Rocq の内側で働く知られざる言語」で、論理プログラミング を扱いました。
論理プログラミングの基礎は Horn 節で、Prolog も λProlog も Horn 節を拡張した言語です。
MetaPRL のメタ論理も Horn 節（型なしの二階 Horn 節） なので、 MetaPRLは論理プログラミングの系統に属します。

記事「Haskell から始める型理論の家系図 — 単純型付きラムダから HoTT まで」では、Twelf を 「論理プログラミングの様式と依存型が合流した定理証明支援系」 として紹介しました。 Twelf は 依存型と論理プログラミングを合流 させ、 MetaPRL は 型なしの項言語と論理プログラミングを合流させた、という違いがあります。

形式手法のプログラミングツールキット
MetaPRL の 項操作や書き換えの機能を、外部のプログラムから部品として使える、という意味です。
MetaPRL は OCaml で書かれており、項の構文・α 等価性の判定・単一化・書き換えエンジンといった機能が、それぞれ OCaml のモジュールとして分かれています。
TPHOLs 2003 の論文によれば、これらのモジュールは汎用的なインタフェースで公開されており、
MetaPRLの対話環境を起動しなくても、別のOCaml プログラムからライブラリとして呼び出せます。
この対話篇の後半で扱う JProver が、その部品を使って作られた実例 です。
JProver は、 MetaPRL の項操作モジュールを使って書かれた OCaml プログラムであり、
MetaPRL の上に載る個々の論理（一階論理や CZF）は参照していません。

（タロウくんの認識が誤っている点が2つあります）

（１つ目）
Dedukti の中心目的は、他の定理証明支援系、たとえば Lean 4・Rocq・HOL Light が出力した証明を翻訳して、独立に再検査することですが、MetaPRL には、こうした機能を実現するための仕組みは備わっていません。

しかし、MetaPRL*が、他の定理証明支援系と無関係だというわけではありません。

TPHOLs 2003 の論文によると、 MetaPRL は Formal Digital Library（FDL、形式的デジタル図書館）という計画 の一部として使われました。

FDL とは、コーネル大学が進めた計画 で、複数の定理証明支援系で作られた定義・定理・証明を、1 つの共有データベースに登録して保存し、検索や再利用ができるようにするもの です。

この計画は、遅くとも 2000 年には動き始めていました。
（西暦何年からスタートしたのかは、筆者が調べた限り、資料が見当たりませんでした。2000年に Allen らが国際会議 CADE-17 で発表した Nuprl 5 の論文が、筆者が確認できた最も古い史実です）

TPHOLs 2003 の時点で、 MetaPRL・Nuprl・PVS で作られた定義や定理が登録されており、将来は Coq・HOL・Isabelle なども加える計画でした。

MetaPRL は、この共有データベースに定義や定理を登録する定理証明支援系のひとつとして採用された実績があります。

なお、コーネル大学の Nuprl System ページによれば、FDL は Nuprl 5 の別名であり、 Nuprl 5 は 現在もクラウドで稼働しています。

出典：
Cornell University, PRL Project, "Nuprl System". https://nuprl-web.cs.cornell.edu/html/NuprlSystem.html

FDL は Nuprl 5 という形で 2000 年に実装されはじめ、その後も開発が続き、現在も上記のウェブサイトからアクセスすることができます。

ただ、TPHOLs 2003 の論文で謳われていた「 Coq・HOL・Isabelle なども加える」という構想が実現したかどうかは、筆者が調べた範囲では確認できませんでした。

また、Nuprl・MetaPRL・PVS 以外の定理証明支援系の定義や定理が FDL に登録されたかどうかを確認できる資料も見当たりませんでした。

出典：
S. F. Allen, R. L. Constable, R. Eaton, C. Kreitz, L. Lorigo, "The Nuprl Open Logical Environment", CADE-17, LNAI 1831, pp. 170-176, Springer, 2000.

また、 MetaPRL の上に作られた JProver という一階直観主義論理の自動証明器 は、 Coq にも統合されました。

JProver は、MLで書かれたプログラム です。

出典：
Rocq Prover packages, coq-jprover. https://rocq-prover.org/p/coq-jprover

JProver は、項を扱う処理（項の読み取り・単一化・書き換えなど）を自分では持たず、 MetaPRL のモジュールを呼び出して済ませています。

そのため、JProver を MetaPRL の外に持ち出すには、JProver 自身のコードだけでは足りず、JProver が呼び出している MetaPRL のモジュールのコードも一緒に持ち出す必要があります。

Huang Guan-Shieng という研究者は、JProver 自身の ML コードと、JProver が呼び出している MetaPRL のモジュールの ML コードを、 MetaPRL から取り出し、 Coq のプラグインとして組み込みました。

これによって、Coq の中で JProver をタクティクとして呼び出せるようになりました。

つまり、 MetaPRL の上で動いていた自動証明器が、 Coq の上でも動くようになった、ということです（詳しくはこの対話篇の後半で扱います）。

このように、Formal Digital Library と JProver という実例は存在するものの、これらは、証明の保管と、自動証明器の移植 を目指したものです。

いずれも、Deduktiのように、別の定理証明支援系の証明を翻訳して再検査する仕組みではありません。

JProver を Coq に移植したことは、証明を作るプログラム（つまり、自動証明器）を移したことであって、証明そのものを移したことではありません。

（２つ目）
Dedukti のメタ理論は 型検査が決定可能 です。
だから、翻訳された証明項をそのまま検査することが可能です。

それに対して、MetaPRL のメタ理論は computational type theory なので、型検査が決定不能 です。
証明の検査には、タクティクによる対話的な構築が必要になります。

Deduktiの「小さな証明検査器が自動で再検査する」という用途は、MetaPRLでは実現困難です。

（したがって、こう表現するのが妥当と思われます）

MetaPRL は「computational type theory を土台にした logical framework」ですが、「Dedukti と同じ目的を持つもの」ではありません。

📌 中上級者向けコラム：タクティク方式でも、規則の適用はシステムが確認する

本文では、MetaPRL では定理証明エンジニア（人）がタクティクで導出を組み立てると説明しました。これは、人が証明の正しさを目視だけで保証するという意味ではありません。

人が担うのは、どのタクティクを使うか、どの方針で部分目標を分解するかを選ぶことです。MetaPRL は、そのタクティクに対応する推論規則を適用し、生成された部分目標を管理します。

Dedukti の典型的な利用像は、完成した証明項を受け取り、型検査器が自動再検査することです。MetaPRL の典型的な利用像は、推論規則を使って証明を段階的に精密化することです。両者の違いは、自動化があるかないかではなく、自動化を証明作成のどの段階に置くかにあります。

タロウくん：
先ほど 「自動証明器の移植」 という言葉が出てきました。
自動証明器の移植 とは、何ですか？

専任講師：
JProver という自動証明器 を、 Coq の中で使えるように 移し替えた ことです。

JProver は、connection method という手法で証明を探索する、一階直観主義論理の自動証明器 です。

自動証明器とは、証明したい命題を入力として受け取り、その命題の証明を人手を介さずに探索し、見つかれば証明を出力するプログラムです。

JProver の場合、入力となる命題は、定理証明エンジニア（人）が定理証明支援系の中で証明を組み立てている途中で現れます。

証明の途中で、一階直観主義論理の範囲に収まる部分目標が出てきたとき、定理証明エンジニア（人）はその部分目標を JProver に渡します。

JProver は、渡された部分目標の証明を自動で探索し、見つかれば証明を返します。

JProver は、MetaPRLの項操作モジュール（項の読み取り・単一化・書き換えなど）を部品として使って、ML で書かれています。

ただし、 MetaPRL の上に載る個々の論理（一階論理や CZF）には依存していないので、特定の論理体系に縛られない汎用的なプログラムになっています。

この汎用性は、出力の形にも現れています。

JProver は、見つけた証明を、一階論理の推論規則をどの順に適用したか、という規則の適用列の形で出力します。

この適用列 は、 MetaPRL の項でも Coq の項でもなく、どの定理証明支援系にも属さない中立な形式 です。各定理証明支援系では、この適用列の 1 つ 1 つの規則を、自分のタクティクに置き換えれば、JProver の見つけた証明をそのまま自分の証明として使うことが可能です。

実際に、コーネル大学の PRL グループ（Constable が率いる研究グループで、 Nuprl と MetaPRL を開発した）は、2つの置き換えを行いました。

1つは、 MetaPRL の上に載っている論理のひとつであるNuprl型理論（theories/itt/）のタクティクへの置き換え です。

もう 1 つは、 MetaPRLとは別 の 独立したシステムである Nuprl そのもののタクティクへの置き換え です。

さらに、Guan-Shieng Huang という研究者が、 Coq のタクティクへの置き換え を、TPHOLs 2003 の論文によれば PRL コミュニティの助けなしに単独で行いました。

こうして、 MetaPRL の部品で作られた自動証明器が、 MetaPRL の外の定理証明支援系でも使われるようになりました。

タロウくん：
それは、 Dedukti がやっていることとは違うのですか？

専任講師：
違います。移されたものが違います。

Dedukti が移すのは、証明項 です。

Lean 4 や Rocq が出力した証明項を Dedukti の形式に翻訳し、 Dedukti の証明検査器で再検査します。証明そのものが、定理証明支援系のあいだを移動します。

JProver の移植で移されたのは、証明を探索するプログラム です。
JProver というプログラムが Coq の中で動き、 Coq の証明を新しく作ります。

証明が移動するのではなく、証明を作るプログラムが移動するのです。

したがって、JProver の Coq 統合は、 MetaPRL と Coq のあいだで 証明を相互運用する仕組みではありません。

出典：
J. Hickey, A. Nogin, R. L. Constable ほか 12 名, "MetaPRL – A Modular Logical Environment", TPHOLs 2003, LNCS 2758, pp. 287-303. DOI: 10.1007/10930755_19. https://www.cs.uni-potsdam.de/ti/kreitz/PDF/03tphols-metaprl.pdf

【対話篇 2】型なしの土台とは、具体的にどんな言語か

タロウくん：
MetaPRL の 「型なしの土台」 とは、具体的にはどんな言語なのですか？

専任講師：
項言語（term language） と呼ばれるごく単純な言語です。
Nuprl の項の構文を、そのまま使っています。

項は、演算子の名前と、部分項の並びからなります。部分項には、束縛変数を付けられます。それだけです。
項は型を持ちません。

実際のコードを見てみましょう。

MetaPRL のソースコードは、GitHub の jyh/metaprl というリポジトリに残されています。

jyh は MetaPRL の設計者 Jason Hickey 自身のアカウントで、このリポジトリが MetaPRL の公式のソースコードです。

MetaPRL は OCaml 4.02.3 または 4.05.0 を要求し、現在も保守されている OCaml ではビルドできません。
本記事ではソースコードを読むことで、動かす代わりとします。

そのリポジトリの theories/fol/fol_and.ml から、一階論理の「かつ」を定義した部分を抜き出してみます。

このファイルを選んだのは、theories/ の中で最も短いファイルの 1 つ（62 行）で、「かつ」という誰でも知っている概念を定義しているからです。

extends Fol_type

open Basic_tactics

declare "and"{'A; 'B}
declare "pair"{'a; 'b}
declare spread{'x; a, b. 'body['a; 'b]}

（読み方）

1 行目の extends Fol_type は、この理論が Fol_type という別の理論を継承する、という宣言です。 MetaPRL の理論は、モジュール（module）として継承（inheritance）できます。

declare "and"{'A; 'B} が、項の宣言です。"and" が演算子の名前、{'A; 'B} が 2 つの部分項です。'A の先頭のアポストロフィは、これがメタ変数（何か任意の項が入る場所）であることを示します。この宣言は「and という演算子は、2 つの項を受け取る」と述べているだけで、'A や 'B は型を持ちません。

declare spread{'x; a, b. 'body['a; 'b]} は、束縛付きの部分項の例です。a, b. が束縛変数の宣言で、その後ろの 'body['a; 'b] は「a と b に依存しうる項」です。「対 'x を分解して、その 2 つの成分を a と b と名付け、'body の中で使う」という形を宣言しています。

タロウくん：
これは OCaml のファイルですよね。declare という構文は OCaml にはないと思うのですが。

専任講師：
そのとおりです。.ml という拡張子で、OCaml のファイルです。しかし、declare・prim・prim_rw・dform・sequent { … } は OCaml の構文ではありません。

これらは、camlp5 という OCaml の構文拡張の仕組みを使って、 MetaPRL が OCaml に足した構文です。README.md が「MetaPRL 独自の camlp5 quotation 構文」と呼んでいるものです。camlp5 quotation は言語ではなく、項言語を OCaml のソースの中に書くための記法です。

つまり、 MetaPRL の理論ファイルは、OCaml のコードと、 MetaPRL の項言語で書かれた定義とが、1 つのファイルに織り込まれたものです。README.md はこれを「形式的な文と OCaml コードの密な織り込み」と表現しています。

続きを見ます。計算規則と推論規則です。

prim_rw reduce_spread : spread{pair{'x; 'y}; a, b. 'body['a; 'b]} <--> 'body['x; 'y]

prim and_intro {| intro [] |} :
   [main] ('a : sequent { <H> >- 'A }) -->
   [main] ('b : sequent { <H> >- 'B }) -->
   sequent { <H> >- 'A & 'B } = pair{'a; 'b}

（読み方）

prim_rw reduce_spread : … <--> … が、計算規則（書き換え規則）です。

左辺 spread{pair{'x; 'y}; a, b. 'body['a; 'b]} は「対 pair{'x; 'y} を spread で分解する」という項で、右辺 'body['x; 'y] は「分解した成分をそのまま 'body に代入した」項です。

<--> は、左辺を右辺に書き換えてよい、という意味です。
これは、対を作ってすぐ分解するなら分解結果に直接置き換えてよい、という $β$ 規則の一種 です。

注目すべきは、この書き換え規則には、型が一切出てこないことです。

'x・'y・'body が どんな型かを問わずに、形だけを見て書き換えます。

「なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜」で述べた 「型なしの書き換え」 が、これです。

📌 中上級者向けコラム：型を見ない書き換えは、無制限の書き換えではない

prim_rw の規則に型が現れないことは、MetaPRL の書き換え規則が、型注釈ではなく項の形を直接見て書かれていることを示します。

ただし、これは任意の書き換え規則を自由に追加してよい、という意味ではありません。

ある対象論理を正しく表すには、採用する計算規則が、その論理の推論規則や意味づけと整合していなければなりません。

本文で押さえればよい点は、「spread{pair{...}; ...} のような項の形が現れたら、型注釈を参照せずに書き換える」ということです。

中上級者向けには、型なしの項書換えを土台にして、その上で論理ごとの判断を構成する設計だと捉えられます。

prim and_intro … : が、推論規則です。--> で区切られた前提が 2 つあり、最後の行が結論です。

前提 1  sequent { <H> >- 'A }        文脈 H のもとで A が成り立つ
前提 2  sequent { <H> >- 'B }        文脈 H のもとで B が成り立つ
結論    sequent { <H> >- 'A & 'B }   文脈 H のもとで A かつ B が成り立つ

sequent { <H> >- 'A } がシーケント（sequent）の記法です。<H> は文脈変数（context variable）で、任意の仮説の列が入ります。>- がターンスタイル（turnstile）です。

[main] は、この前提が主要なサブゴールであることを示すラベルです。('a : …) は、前提 1 の証明を 'a と名付ける、という意味です。

最後の = pair{'a; 'b} が、この規則の計算的内容 です。

MetaPRL の user guide は、これを proof extract（証明の計算的内容を定義する項） と呼んでいます。

「$A$ の証明 'a と B の証明 'b から、$A$ かつ $B$ の証明 pair{'a; 'b} を作る」と述べています。前提の証明から結論の証明を組み立てる、というプログラムが、規則に付いています。

{| intro [] |} は、この規則を intro リソースに登録するアノテーションです。

intro リソースとは、結論を分解するための規則の登録簿です。

定理証明エンジニア（人）が dT 0 と書くと、 MetaPRL は結論の形を見て、この登録簿から合う規則を探して適用します。

結論が「$A$ かつ $B$」の形なら、この and_intro が選ばれます。

タロウくん：
つまり、型なしの項言語 で、一階論理の「かつ」の意味（導入規則と計算規則）を書いている、ということですね。

専任講師：
そのとおりです。
同じ項言語で、theories/ の他のディレクトリは別の論理を書いています。

ディレクトリ	載せている論理
theories/itt	Nuprl 型理論
theories/fol	一階論理
theories/czf	Aczel の構成的集合論 CZF（Constructive Zermelo-Fraenkel set theory）
theories/lf	Edinburgh LF
theories/cic	Calculus of Inductive Constructions
theories/hol	高階論理
theories/kat	テスト付き Kleene 代数（Kleene algebra with tests）
theories/s4lp	正当化論理（justification logic）
theories/fir	コンパイラ中間表現（intermediate representation）
theories/poplmark	POPLmark challenge

項言語は 1 つで、載せる論理が 10 以上ある。
これが 「型なしの土台の上に複数の論理を載せる」ということを、コードで見た姿 です。

タロウくん：
Executive Summary で、itt_dfun.ml というファイルからの引用がありました。
あれは何を定義しているのですか？

専任講師：
Nuprl 型理論の関数型です。

theories/itt/ は、 Nuprl の型理論（ITT、intuitionistic type theory）を MetaPRL の項言語で定義したディレクトリです。

その中の itt_dfun.ml が関数型のファイルで、「$A$ の要素を受け取って $B$ の要素を返す振る舞いをするプログラムは、関数型 $A \to B$ に帰属する」という規則を定めています。

Executive Summary で引用した lambdaFormation と lambdaEquality は、関数型への帰属を、プログラムの振る舞いで定める規則 でした。プログラムの形ではなく、どの入力に対してどの出力を返すか、で帰属が決まります。

fol_and.ml と itt_dfun.ml を並べると、 MetaPRL の作りが分かります。
どちらも同じ declare・prim・sequent { … } という構文で書かれています。

fol_and.ml は一階論理の「かつ」を定義し、itt_dfun.ml は Nuprl 型理論の「関数型」を定義しています。

対象論理が違うだけで、土台の項言語と、規則を書く構文は同じ です。

Nuprl 自体のソースコードは公開されていないので、 Nuprl 型理論をコードとして読める公開資料は、この theories/itt/ が唯一です。

出典：jyh/metaprl, theories/itt/core/itt_dfun.ml. https://github.com/jyh/metaprl/blob/master/theories/itt/core/itt_dfun.ml

出典：

jyh/metaprl, theories/fol/fol_and.ml. https://github.com/jyh/metaprl/blob/master/theories/fol/fol_and.ml

jyh/metaprl, doc/htmlman/user-guide/mp-axiom.html（proof extract の用語）

【対話篇 3】 λΠ計算との比較・型なしと複数の型

タロウくん：
対話篇 1 で、「JProver は MetaPRL をプログラミングのツールキットとして使って実装され、特定の論理体系に依存しない汎用的な作りになっています」と説明がありました。

ということは、JProver は、 Dedukti が λΠ計算を採用したみたいに、λΠ計算を採用したか、それと類似した抽象的（汎用的）な論理プログラミング言語を採用したのですか？

また、 MetaPRL 自身もそうですか？

専任講師：
どちらも、λΠ計算を採用せず、別の仕組みに立脚しています。
JProver から見ていきます。

（JProver について）

JProver は、λΠ計算のような論理を記述するメタ言語を採用したわけではありません。
JProver は、一階直観主義論理と古典論理の証明を探索する専用のプログラムです。
対象とする論理は固定されています。

「特定の論理体系に依存しない」というのは、別の意味です。

MetaPRL は、項の構文・α 等価性・単一化・書き換えエンジンといった 低レベルのモジュール群を、汎用的なインタフェースで外部に公開しています。

TPHOLs 2003 の論文は、これを logical toolkit と呼んでいます。

定訳がないため、本記事では「論理ツールキット」と訳します。

JProver は、このツールキットを使って書かれました。

MetaPRL の上に実装されている Nuprl型理論や CZF といった個々の論理理論を参照せずに、項を操作する部分だけを使って 書かれています。

だから「特定の論理体系に依存しない」のです。

（MetaPRL 自身について）

MetaPRL のメタ論理も、λΠ計算ではありません。Hickey の博士論文の第 1.3 節と第 2 章によれば、 MetaPRL のメタ論理は、 Nuprlの項の上の、型なしの二階 Horn 節 です。

Hickey の博士論文は、 Isabelle と Edinburgh LF のメタ論理が、 Nuprl型理論の形式化に直接は適さなかった 理由として、以下の３点を挙げています。

（理由１）
Nuprl の型理論は、一般的な束縛の仕組みを持つ構文を使っており、 Isabelle や LF の構文と合わない。

（理由２）
Nuprl のプログラムは型なしであり、1 つのプログラムが文脈に応じて複数の型を持ちうる。

（理由３）
Nuprl の論理は、計算的な書き換えのための代入と推論規則のための代入という 2 種類の明示的代入（explicit substitution）を使うと最も自然に形式化できる。

そのうえで、Hickey は Isabelle のメタ論理の考え方を借り、それを Nuprl の項の上の 型なし二階 Horn 節として修正した、と述べています。

（Dedukti・Isabelle・MetaPRL のメタ言語を並べます）

名称	メタ言語	型の有無
Edinburgh LF・Twelf	λΠ計算（依存型を持つ型付きラムダ計算）	型付き
Dedukti	λΠ計算 modulo rewriting	型付き
Isabelle	Pure（直観主義高階論理。hereditary Harrop 式）	型付き
MetaPRL	Nuprl の項の上の型なし二階 Horn 節。明示的代入を持つ	型なし

MetaPRL だけが型なしです。

Nuprl のプログラムが型なしなので、それに合わせたのです。

「Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す」で述べた 「計算が先、型が後」という computational type theory の順序が、メタ言語の設計にも現れています。

タロウくん：
「2 つ目。 Nuprl のプログラムは型なしであり、1 つのプログラムが文脈に応じて複数の型を持ちうる。」が目を引きました。

この「文脈に応じて複数の型を持ちうる」ということと、「型なし」である（Nuprl ですから、computational type theory を採用しているから、型なしと理解しました）ということの 2 つが、 MetaPRL を理解する鍵になりそうな気配を感じています。

専任講師：
その直観は正しいです。
2つは同じことの表と裏で、computational type theory の帰結です。

（「型なし」の意味）

「Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す」で述べたとおり、computational type theory では、先にプログラムがあり、型はあとから決まります。

プログラムはそれ自体では型を持ちません。

型は、「こういう振る舞いをするプログラムの集まり」という条件です。

あるプログラムが型 $A$ に属するかどうかは、そのプログラムの振る舞いが $A$ の条件を満たすかどうかで判断します。

だから、 Nuprl のプログラムは 型なし です。
プログラムに型が貼り付いているのではなく、判断によって型への帰属が決まります。

この「型なしの項に、計算の振る舞いを見て後から型を割り当てる」という考え方は、Dana Scott が 1976 年に発表した型なしラムダ計算のモデルに遡ります。

型なしの項の集まりの上に、「どの項とどの項を同じ型の要素と見なすか」という部分同値関係（PER） を置くことで、型を後から定めます。

PERモデル と呼ばれ、プログラミング言語理論では広く使われる技法です。

しかし、この考え方をそのまま定理証明支援系の型システムとして実装したものは、筆者が調べた範囲では Nuprlの系統（Nuprl・MetaPRL・RedPRL）以外には見当たりませんでした。

computational type theory は、定理証明支援系固有のものです。

出典：
D. S. Scott, "Data Types as Lattices", SIAM Journal on Computing 5(3), pp. 522-587, 1976.

（「文脈に応じて複数の型を持ちうる」の意味）

さて。

型がプログラムに貼り付いていないなら、同じプログラムが複数の型の条件を満たすことがあります。

たとえば、恒等関数 λx. x を考えます。

自然数を受け取って自然数を返す、という振る舞いをするので、nat → nat に属します。
真偽値を受け取って真偽値を返す、という振る舞いもするので、bool → bool にも属します。

どの入力に対しても入力をそのまま返すので、どの型 $A$ についても A → A に属します。

Lean 4 や Rocq では、λx. x を書くとき、x の型を先に宣言します。
fun (x : Nat) => x と fun (x : Bool) => x は、別のプログラムです。

Nuprlでは、λx. x は 1 つのプログラムで、文脈に応じて nat → nat にも bool → bool にも属します。

もう 1 つ、部分型（subtype） の例があります。

Nuprl では、自然数の型は整数の型の部分型 です。
自然数 3 は、nat に属し、同時に int にも属します。
3 というプログラムは 1 つで、型が 2 つあるということです。

タロウくん：
1 つのプログラムが複数の型に属する、という仕組みは、Haskell の多相型でも実現されている のではないですか？

専任講師：
そのとおりです。
型付き言語でも、似たことは実現されています。

Haskell の多相型 forall a. a -> a は、恒等関数 id を Int -> Int としても Bool -> Bool としても使えるようにする仕組みです。

TypeScript の交差型 A & B は、1 つの値が型 A と型 B の両方に属することを表します。

Scala の部分型 は、自然数の型が整数の型に含まれる、という関係を表します。

これらはすべて、「1 つのプログラムが文脈に応じて複数の型に属する」ことを、型付き言語の中で実現する仕組み です。

📌 中上級者向けコラム：Nuprl の「複数の型」と、多相型・部分型は同じではない

Nuprl で「一つの項が複数の型を持てる」と言うとき、中心にあるのは、型注釈のない同じ項について、文脈に応じて「この型の要素である」と判断できることです。

Haskell のパラメトリック多相、オブジェクト指向言語の部分型、交差型も、一つのプログラムを複数の型の観点から扱う仕組みです。ただし、どのような意味で複数の型を認めるか、型検査をどう行うかは、Nuprl の方式と同じではありません。

したがって本文の主張は、「型付き言語では一つのプログラムを複数の型で扱えない」という意味ではありません。

新しい帰属の仕方を、型システムの規則としてあらかじめ組み込むのか、項に対する外側の判断として後から与えるのか、という設計の違い を述べています。

タロウくん：
では、型なし言語の強み は、どこにあるのですか？

専任講師：
実現のしやすさ にあります。

型付き言語 では、多相型・交差型・部分型のそれぞれを、型システムの機能としてあらかじめ組み込んでおく必要 があります。

Haskell は多相型を持ちますが、部分型を持ちません。
TypeScript は交差型と部分型を持ちますが、Haskell のような多相型の推論は限定的 です。

3 つの仕組みを 1 つの型システムに組み合わせると、型検査が複雑になり、型推論が決定不能になる場合もあります。

新しい種類の「文脈に応じた帰属」が必要になれば、型システムそのものを拡張しなければなりません。

ここまでが 型付き言語 です。

次に、型なし言語 について見ていきます。

型なし言語 では、項に型が貼り付いていません。
どんな型への帰属も、「この項はこの型の条件を満たすか」という判断として、後から与えられます。

型システムを拡張せずに、新しい型を定義して、既存の項がその型に属するかを判断することができます。
さらに、多相型・交差型・部分型に相当する帰属が、すべて同じ「判断」の仕組みで扱えます。

タロウくん：
それは、実務の場面では何の役に立つのですか？

専任講師：
同じプログラムを、複数の性質の証明に使い回したい場合 に、力を発揮することが期待されます。

たとえば、ある通信プロトコルのプログラム があるとします。

そのプログラムについて、

「メッセージを失わない」という性質

と、

「メッセージの順序を保つ」という性質

を、別々に証明したい。

そんな場面を考えてみて下さい。

型付き言語 では、それぞれの性質を表す型を用意し、プログラムにその型を付けて証明することになります。
2つの型を同時に付ける には、交差型のような仕組みが必要 です。

型なし言語 では、プログラムは 1 つのまま、「メッセージを失わないプログラムの型」に属するという判断と、「順序を保つプログラムの型」に属するという判断を、別々に与えることができるのです。

プログラムを書き換えたり、型を付け直したりする必要がありません。

ただし、以上の考察は、筆者個人の見解です。

Nuprl が持つ強みが、実務上どう役立ったかを述べた一次資料は、見当たりませんでした。

MetaPRL の動機となった Ensemble の検証で、この強みが使われた可能性はありますが、一次資料で確認することはできませんでした。

（これが MetaPRL のメタ論理を型なしにした理由です）

Hickey の博士論文の第 1.3 節の原文は、次のとおりです。

Second, programs in a Nuprl system are untyped: a program may have multiple types that depend on the context in which the program is used.

（筆者訳）第２に、Nuprl のシステムにおけるプログラムは型なしである。
1つのプログラムは、そのプログラムが使われる文脈に応じて、複数の型を持ちうる。

1つのプログラムは、そのプログラムが使われる文脈に応じて、複数の型を持ちうる。

λΠ計算のような型付きのメタ言語で Nuprl を符号化しようとすると、 Nuprl のプログラムに 型を付けて表さなければなりません。

しかし、1 つのプログラムが複数の型を持つなら、どの型を付ければよいか決まりません。
型付きのメタ言語と、型なしのプログラムは、噛み合わないのです。

だから、Hickey は MetaPRL のメタ論理を型なしにしました。

Nuprl の項をそのまま扱い、型への帰属は判断として別に扱う。
computational type theory の順序を、メタ論理のレベルでも守ったのです。

タロウくん：
それなら、 Dedukti で Nuprl の証明を扱えないのも、同じ理由ですか？

専任講師：
筆者の見当では、同じ理由が関わっています。

「なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜」で、 Nuprl・MetaPRL・RedPRL・redtt・coolttのいずれにも、Dedukti　の翻訳器が確認できなかった 、と述べました。

そして、「Dedukti の符号化は型検査が決定可能な体系を前提としており、 Nuprl の系統は型検査が決定不能なので噛み合わない」という見方を示しました。

いま述べた「型なしのプログラムを型付きのメタ言語で表せない」という困難は、その見当と同じ理由に根ざしています。

型付きのメタ言語では型検査が決定可能になり、型なしのプログラムを扱う体系では型検査が決定不能になる。

どちらも、型がプログラムに貼り付いているか、判断として別にあるか、という違い の現れです。

ただし、これは筆者の見立てです。

Nuprl の証明を Dedukti に翻訳することが原理的に不可能だ、と述べた資料は見当たりませんでした。

出典：

J. J. Hickey, "The MetaPRL Logical Programming Environment", PhD thesis, Cornell University, January 2001, §1.3, §2. https://nuprl-web.cs.cornell.edu/documents/Hickey/Hickeythesis.pdf

J. Hickey ほか, "MetaPRL – A Modular Logical Environment", TPHOLs 2003, LNCS 2758, §4.3, §6.

【対話篇 4】階層構造の違いから何を読み取るか

タロウくん：
MetaPRL の上には、 Edinburgh LF と CIC が対象論理として載っている、と先生は言われました。一方で、 Dedukti は LF （λΠ計算）を土台にして、その上に CIC を載せます。

つまり、こういう階層構造ですね。

	土台	対象
Dedukti	λΠ計算（LF）	CIC・HOL・一階論理 …
MetaPRL	型なし二階 Horn 節（Nuprl の項の上）	Nuprl 型理論・CZF・LF・CIC・HOL・一階論理 …

Dedukti では土台にある LF が、 MetaPRL では対象として載っています。
この違いから、何を読み取るべきですか？

専任講師：
3つのことが読み取れます。

（1 つ目。LF は、土台にもなれば、対象にもなる）

「【Dedukti入門 ③】Logical Framework とは何か ── 1967 年の Automath から Isabelle、1987 年の Edinburgh LF、そして Dedukti へ」で、logical framework とは「ひとつの型理論を土台に固定し、その上に複数の論理を載せる仕組み」 と述べました。

LF は、その土台の代表でした。

しかし MetaPRL は、 LF を対象として載せています。

LF の推論規則を、MetaPRL のメタ論理で記述したのです。
Hickey の博士論文は、これを「LF の予備的な形式化」と呼んでいます。

つまり、 LF は 絶対的な土台ではありません。

何を土台にするかは、設計者の選択です。

より低い層に別の土台を置けば、 LF も対象論理のひとつになるのです。

（2つ目。土台の型の有無が、証明の検査の仕方を決める）

Dedukti の土台 λΠ計算は、型付きです。
CIC の証明を Dedukti に翻訳すると、λΠ計算の項になります。

その項が正しく型付けされているかを、 Dedukti の型検査器が判定します。
土台の型検査が、そのまま対象論理の証明の検査になります。

MetaPRL の土台は、型なし です。
対象論理の証明が正しいかどうかは、土台の型検査では判定することができません。

対象論理の推論規則を適用して導出を構築する、という形で確かめます。
土台の型検査ではなく、対象論理のレベルでの導出の構築が、証明の検査になります。

だから、Dedukti は「証明項を受け取って型検査する」プログラムになり、
MetaPRL は「タクティクで導出を構築する」プログラムになります。

土台の型の有無が、この違いを生んでいます。

（3つ目。型なしの土台は、型付きの枠組みを載せられる。逆は困難）

MetaPRL は、型なしの土台の上に、型付きの枠組み LF を載せました。

型付きの枠組みは、その型付け規則を対象論理の推論規則として記述すれば、型なしの土台の上で表現できます。

逆に、型付きの土台の上に、型なしの体系である Nuprl の型理論を載せられるかは、困難です。

対話篇 3 で述べたとおり、 Nuprl のプログラムは 型なしで、1 つのプログラムが文脈に応じて複数の型を持ちます。

型付きの土台で表そうとすると、どの型を付けるかが決まりません。

タロウくん：
型付きの土台では、本当に載せられないのですか？何か方法はないのですか？

専任講師：
方法はあります。しかし、その方法では、型なしの土台と同じことはできません。

たとえ話で説明しましょう。

日本語の文を、英語の中で扱いたいとします。

日本語の文をそのまま英語の文として読むことはできません。

しかし、日本語の文を「文字列」として英語の中に持ち込み、「この文字列は、日本語として正しい文である」と英語で述べることはできます。

型付きの土台で Nuprl の項を扱うのも、同じです。

Nuprl の項を、Term という 1 つの型のデータとして λΠ計算の中に持ち込みます。

そして、「この Term 型のデータは、 Nuprl の自然数の型に属する」という命題を、λΠ計算の中で書きます。

この方法を、深い埋め込み（deep embedding） と呼びます。
この方法なら、 Nuprl の型理論を、λΠ計算の中で「論理として」記述できます。

しかし、持ち込んだ日本語の文を、英語の文法で読むことはできません。

文字列として持ち込んだ以上、それは文字列であって、日本語の文としての意味は、英語の側で改めて定義し直さなければなりません。

同じく、Term 型のデータとして持ち込んだ Nuprl の項を、 Nuprl の項として計算することはできません。

項の計算は、Term 型のデータに対する操作として、λΠ計算の側で改めて定義し直さなければなりません。

Nuprl の型なしの計算をそのまま行うのではなく、 Nuprl の計算の仕組みを λΠ計算の中で作り直してから、その上で計算することになります。

型なしの土台なら、 Nuprl の項をそのまま項として扱い、そのまま計算できます。持ち込んだ日本語の文を、日本語のまま読めるのと同じです。

つまり、型付きの土台でも Nuprl の型理論を「記述する」ことはできますが、 Nuprl の項を「型なしのまま計算しながら扱う」ことはできません。型なしの土台の利点は、後者にあります。

この非対称から、 Dedukti の翻訳器一覧に Nuprl 系が 1つも無いことと、 MetaPRL が LF や CIC を載せられたことの両方が説明できます。

タロウくん：
ここまでの話を、型なしの土台と型付きの土台で何ができて何ができないか、という形で整理してもらえますか？

専任講師：
表にします。

	型なしの土台（MetaPRL）	型付きの土台（Dedukti・Isabelle）
土台の言語	Nuprl の項言語（型なし二階 Horn 節）	λΠ計算 modulo rewriting・Isabelle/Pure
型検査	決定不能	決定可能
証明の検査	定理証明エンジニア（人）がタクティクで導出を組み立てる	証明項を受け取れば、型検査器が自動で再検査する
型なしの体系（Nuprl の型理論）を載せる	できる。型なしのまま計算しながら扱える	記述はできる（deep embedding）が、型なしのまま計算することはできない
型付きの枠組み（LF・CIC）を載せる	できる	できる
論理どうしの関係を記述する	できる（導出規則、derived rule によるモデル翻訳）	できる（符号化の翻訳）
他の定理証明支援系の証明を持ち込む	できない	できる（証明項を翻訳して再検査）

土台が型なしか型付きかで変わるのは、2 つの行だけです。

「型なしの体系を載せる」 と 「他の定理証明支援系の証明を持ち込む」 です。

それ以外の行、型付きの枠組みを載せることと、論理どうしの関係を記述することは、どちらの土台でもできます。

つまり、型なしの土台を選ぶと得るもの は、「型なしの体系をそのまま計算しながら載せられること」 、
失うもの は、「他の定理証明支援系の証明を持ち込んで自動で再検査すること」 です。

型付き の土台を選ぶと、この 2 つが入れ替わります。

タロウくん：
用途から見ると、どうなりますか？

専任講師：
用途別に、利点と欠点を並べてみましょう。

用途	型なしの土台（MetaPRL）	型付きの土台（Dedukti・Isabelle）
大規模なソフトウェアシステムの検証	利点：プログラムを型なしのまま扱えるので、実際のプログラムコードについて推論しやすい。 MetaPRL は Ensemble の検証のために作られた	欠点：プログラムに型を付けて符号化する必要がある
複数の論理を 1 つのシステムで扱う	利点：10 以上の論理を載せ、導出規則で関係づけた実績がある	利点：同じくできる。 Isabelle は HOL・ZF・FOL を載せている
他の定理証明支援系の証明を再検査する	欠点：できない。型検査が決定不能なので、証明項を受け取って自動で検査する仕組みが成り立たない	利点： Dedukti の中心的な用途。 Lean 4・Rocq・HOL Light の証明を翻訳して再検査する
証明を自動化する	欠点：型検査が決定不能なので、自動化はタクティクによる部分的なものに留まる。 MetaPRL の `autoT` や JProver がその例	利点：型検査が決定可能なので、証明項があれば必ず有限時間で検査が終わる

MetaPRL が LF や CIC を「載せた」というのは、それらの推論規則を MetaPRL のメタ論理で記述した、という意味です。

載せた LF や CIC が、本来の LF や CIC の全機能を忠実に再現しているかは、別の問題です。

Hickey の博士論文は LF について「予備的な形式化」と述べており、完全な再現とは述べていません。

CIC についても、README.md は「hosts」と述べるだけで、忠実さの程度には触れていません。

出典：

J. J. Hickey, "The MetaPRL Logical Programming Environment", PhD thesis, Cornell University, 2001, §1.1.

jyh/metaprl README.md. https://github.com/jyh/metaprl

【対話篇 5】 pointwise と pairwise は MetaPRL でどうなっているか

タロウくん：
「なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜」の中上級者向けコラムで、pointwise functionality と pairwise functionality という 2 つの方式が出てきました。

あれは MetaPRL ではどうなっていますか？

専任講師：
先に、何の話かを説明しましょう。

型理論 では、「x が自然数なら、x + 1 も自然数である」のような判断を扱います。

この判断には、暗黙の約束が含まれています。
「x に等しい 2 つの値を代入したら、x + 1 の結果も等しくなる」という約束です。

この約束を functionality と呼びます。

この約束の決め方には、2つの方法があります。

自然数の例で説明しましょう。

pointwise（1 点ずつ）
まず x に 3 を入れると決める。そのうえで、3 と等しい値、たとえば 2 + 1 や 1 + 2 を x に入れても、結果が 3 + 1 と等しくなることを約束する。
次に x に 5 を入れると決めて、5 と等しい値について同じことを約束する。
値を 1 つずつ固定して、そのたびに約束する。
pairwise（対ごと）
x に入れる 2 つの値を、たとえば「3 と 2 + 1」「5 と 4 + 1」「7 と 3 + 4」のように、等しい値の組として並べる。
どの組を取っても、2 つの値を x に入れた結果が等しくなることを、一度に約束する。
値を 1 つずつ固定するのではなく、等しい値の組すべてについて、まとめて約束する。

両者の違いは、「先に 1 つの値を決めてから、その値と等しいものを考える」か、「等しい値の組を最初から 2つ並べて考える」か、という順序の違いです。

数学的には、量化の順序が異なります。

Nuprl は pointwise を採りました。Stuart Allen が考案した方式で、自然数の帰納法（induction）のような強い規則を使えるようになります。

その代わり、Let 規則（証明を 2 段階に分けて組み合わせる基本的な規則）が一般には成り立たなくなります。

pairwise は、Nogin が MetaPRL の開発の中で再発見した方式で、Let 規則が成り立ちます。

その代わり、pointwise でしか成り立たない別の規則が使えなくなります。

前掲の記事のコラムで扱った Kopylov の博士論文は、 MetaPRL の開発の一部として書かれたものです。

（MetaPRL での実装状況）

筆者が GitHub の theories/itt/ を確認したところ、 MetaPRL は両方の方式を別々のモジュールとして持っています。

theories/itt/core/itt_pairwise.ml
pairwise でのみ成り立つ Let 規則（let_rule）。
作者は Kopylov。コメント：「pointwise では成り立たず、quotientElimination2 規則と矛盾する」
theories/itt/extensions/pointwise/itt_pointwise.ml
pointwise でのみ成り立つ 2 つの規則（hypSubstPointwise、contextSubstPointwise）。コメント：「どちらも Let 規則と矛盾する」
theories/itt/core/itt_struct3.ml
両方の方式で成り立つが、証明が異なる導出規則の集まり

つまり、Kopylov の博士論文で分析された「どちらの方式でどの規則が成り立つか」が、そのまま MetaPRL の理論ファイルとして実装されています。

利用者は、pointwise の規則を使うモジュールと pairwise の規則を使うモジュールのどちらかを選んで、理論を組み立てます。

タロウくん：
前掲の記事のコラムでは、「Let 規則が pointwise で成り立たない理由は、Kopylov の博士論文に書かれていない」とありました。

専任講師：
そのとおりです。ところが、 MetaPRL のソースコードのコメントに、手がかりがありました。

itt_pairwise.ml のコメントは、pairwise の Let 規則が pointwise では「quotientElimination2 規則と矛盾する」と述べています。quotientElimination2 は、商型の除去規則です。つまり、Let 規則と商型の除去規則は、pointwise の意味論（semantics）のもとでは両立しません。

なぜ両立しないのか、その証明はコメントには記されていません。

しかし、「商型の除去規則との衝突」という具体的な手がかりが得られました。

前掲の記事のコラムで「理由は書かれていない」と述べたことを、ここで少し補います。

出典：

jyh/metaprl, theories/itt/core/itt_pairwise.ml

jyh/metaprl, theories/itt/extensions/pointwise/itt_pointwise.ml

jyh/metaprl, theories/itt/core/itt_struct3.ml

A. Kopylov, "Type Theoretical Foundations for Data Structures, Classes, and Objects", PhD thesis, Cornell University, 2004, §2.2. https://www.cs.cornell.edu/people/kopylov/papers/thesis/thesis.pdf

【対話篇 6】動機と目的

タロウくん：
Executive Summary を読みました。

Nuprl は、Common Lisp で実装されているのですね。

僕は Common Lisp は未学習ですが、Lisp は学んだことがあります。

丸括弧がひたすらネストされていて、データも、プログラム（ソースコード）も、どちらも丸括弧がネストされた同じ表記方法をとるので、コードをデータとして取り扱うことができるので、メタプログラミングが得意なんですよね？

たしか、プログラムが別のプログラムを編集するメタプログラミングが、1960 年代か 70 年代でしたか、Eurisko として世界中で注目されたこともあったと、どこかで読みました。

専任講師：
Lisp の性質については、そのとおりです。コードとデータが同じ形で書かれるので、プログラムがプログラムを操作しやすい。この性質を homoiconicity（同像性）と呼びます。

Eurisko については、時期を訂正します。

Eurisko は、Douglas Lenat がスタンフォード大学で 1970 年代末から開発し、1981 年と 1982 年に Traveller という戦略ゲームの全米大会で優勝して注目を集めました。1980 年代初頭です。

Lisp で書かれ、自分自身のヒューリスティクスを書き換えながら発見を行う、という設計 でした。

出典：D. B. Lenat, "EURISKO: A Program That Learns New Heuristics and Domain Concepts", Artificial Intelligence 21(1-2), pp. 61-98, 1983.

Nuprlが Lisp で実装された理由は、時代の事情によるところが大きいです。

1984年当時、記号処理や人工知能の研究では Lisp が標準の言語でした。

コーネル大学の PRL グループは Symbolics 社の Lisp マシンを使っており、 Nuprl の初版はその上で動きました。

1986 年の Nuprl の本によれば、約 6 万行の Lisp と数千行の ML で書かれています。

出典：
R. L. Constable ほか, Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986, Overview. https://nuprl-web.cs.cornell.edu/book/Overview.html

なお、 Nuprl の制御には ML の変種が使われています。

ML は、もともとエディンバラ大学の LCF という定理証明支援系のために、タクティクを書く言語として作られました。

LCF の ML は Lisp の上に実装されていたので、 Nuprl が Lisp の上に ML を載せる構成をとったのは、LCF の伝統に沿ったものです。

出典：
M. Gordon, R. Milner, C. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, LNCS 78, Springer, 1979.

タロウくん：
そして、 MetaPRL は Common Lisp ではなく、OCaml で実装されているのが面白いと思いました。

Nuprl 系の各定理証明支援系でも、実装言語が Common Lisp だったり、OCaml だったりするのは、理論的な理由があるのでしょうか。

それとも、実装者が得意な言語がたまたま実装言語として採用されただけ、なのでしょうか。

専任講師：
理論的な理由と、時代の事情と、実装者の選択が、重なっています。

理論的な理由から述べます。LCF 流の定理証明支援系では、タクティクを ML の関数として書きます。

ML は、LCF のためにこの目的で設計された言語です。

そのため、LCF の系統に属する定理証明支援系は、ML 系の言語で実装されるのが伝統です。

HOL は Standard ML、 Isabelle も Standard ML、 Coq は OCaml です。

MetaPRL も LCF 流のタクティク証明支援系なので、ML 系の OCaml を選ぶのは、この伝統に沿っています。

時代の事情として、1980 年代には Lisp が記号処理の標準でしたが、1990 年代には ML 系の言語が成熟し、性能も向上していました。Hickey の博士論文によれば、 MetaPRL の前身 Nuprl-Light という名前は、Caml-Light（OCaml の前身）を使ったことに由来します。 Nuprl 4 の Lisp 実装が遅かったことが動機のひとつで、Nuprl-Light は Nuprl 4 より 100 倍以上速くなりました。

出典：
J. J. Hickey, "The MetaPRL Logical Programming Environment", PhD thesis, Cornell University, January 2001, §1.1. https://nuprl-web.cs.cornell.edu/documents/Hickey/Hickeythesis.pdf

実装者の選択も関わっています。Hickey は OCaml を選び、その後 OCaml のビルドシステム OMake を作り、2013 年には『Real World OCaml』の共著者に なっています。

OCaml への深い関与が、 MetaPRLの実装言語の選択と無関係ではないと考えられます。

Nuprl の系統をまとめると、次のようになります。

RedPRL・redtt・cooltt の開始時期は、GitHub のリポジトリの記録（最初の Issue の日付、および README の記述）にもとづく概算です。

定理証明支援系	実装言語	開始時期
Nuprl	Common Lisp。制御は ML の変種	1984 年
MetaPRL	OCaml	1996 年（Nuprl-Light として。1998 年に改名）
RedPRL	Standard ML	2016 年頃（2018 年の LFMTP で論文発表。GitHub は 2023 年 4 月にアーカイブ）
redtt	OCaml	2018 年頃（GitHub の最初の Issue が 2018 年 8 月）
cooltt	OCaml	2019 年頃（2019 年の論文 blott の実装から派生）

出典：

RedPRL/sml-redprl（GitHub）. https://github.com/RedPRL/sml-redprl

RedPRL/redtt（GitHub）. https://github.com/RedPRL/redtt

RedPRL/cooltt（GitHub）. https://github.com/RedPRL/cooltt

The RedPRL Development Team, "The red* family of proof assistants". https://redprl.org/

Nuprl だけが Lisp で、それ以降はすべて ML 系です。

1990 年代以降に作られた定理証明支援系は、LCF の伝統に従って ML 系を選んでいます。
実装言語が Lisp か ML 系かは、その定理証明支援系が作られた時代を反映しています。

タロウくん：
そうなんですね。
そうすると、 MetaPRL が設計された動機と目的は、なんですか？

専任講師：
動機は、Ensemble という分散通信システムの検証にありました。

先に、Ensemble とは何かを説明します。Ensemble は、コーネル大学で開発された群通信（group communication）のツールキットです。複数の計算機のあいだで、メッセージを確実に届け、順序を保ち、故障に耐える、といった働きをするソフトウェアの部品です。

TPHOLs 2003 の論文によれば、BBN・Nortel Networks・NASA が、軍事と商用の両方で利用していたようです。さらに、コーネル大学の PRL グループは、Ensemble の検証と自動最適化に Nuprl を活用していた実績があります。

同じ論文が、 MetaPRL の始まりを次のように述べています。

The MetaPRL project (which was initially called NuPRL-Light) was started by Jason Hickey as a part of Ensemble verification effort to simplify formal reasoning about the program code and to address scalability and modularity limitations of NuPRL-4.

（筆者訳）MetaPRL 計画（当初は NuPRL-Light と呼ばれた）は、Ensemble の検証の一環として Jason Hickey が始めたものである。プログラムコードについての形式的な推論を簡単にし、NuPRL-4 のスケーラビリティとモジュール性の限界に対処するためであった。

つまり、 Nuprl 4 では Ensemble のような大きなシステムの検証に手が回らなかった。
それを解決するために、 Nuprl を小さく、モジュール化して、速く作り直した。

それが MetaPRL の出発点です。

タロウくん：
どれくらい速くなったのですか？

専任講師：
Hickey の博士論文によれば、 Nuprl 4 と比べて 100 倍以上速くなりました。
モジュール化と OCaml による再実装で達成した数字です。

さらに、複数のプロセッサに処理を分散させれば、いっそう速くなります。

タロウくん：
Nuprl-Light という名前は、どこから来たのですか？

専任講師：
博士論文に、名前の由来が書かれています。

Isabelle と Edinburgh LF の logical framework の考え方と、Caml-Light という OCaml の前身の言語を組み合わせたことから、Nuprl-Light と名付けられました。

「Light」は、Caml-Light の Light であり、同時に Nuprlを軽くしたという意味 も重ねています。

1998 年に、モスクワ国立大学のチームが計画に参加しました。このときに、 MetaPRL に改名されました。

タロウくん：
目的のほうは？

専任講師：
Hickey の博士論文が、2つの原則として述べています。

（１つ目）

大規模なソフトウェアシステムの設計方法は、問題の部分領域ごとに適した複数の言語・方法論・精密化の技法を含む。したがって、形式システムは複数の論理を定義できなければならず、それは定義上 logical framework である。

（２つ目）

その枠組みは、論理理論のあいだの形式的な関係を表現できなければならない。
システムを部品に分解する問題に対処するためである。

博士論文の要旨の原文は、次のとおりです。

MetaPRL was built to provide a modular, abstract logical framework where multiple designs can be expressed and related.

（筆者訳）MetaPRL は、複数の設計を表現し、関係づけられる、モジュール化された抽象的な logical framework を提供するために作られた。

Hickey 自身の個人的な動機も、博士論文に書かれています。コーネル大学に入る前、Bellcore で 10 年間、VLSI 設計に携わっていた。設計の概要を作るのは楽しいが、そのあとの開発作業に時間を取られる。設計の概要を与えたら、計算機が完成品を作ってくれないか。その願いが、PRL の「精密化によるプログラム開発」という考え方と合致した、と述べています。

出典：

J. J. Hickey, "The MetaPRL Logical Programming Environment", PhD thesis, Cornell University, January 2001, 要旨および §1.1.

J. Hickey ほか, "MetaPRL – A Modular Logical Environment", TPHOLs 2003, §1.

【対話篇 7】実際に活用されたか

タロウくん：
そして、実装された後、実際にその目的で活用されたのですか？

専任講師：
活用されました。TPHOLs 2003 の論文と博士論文から、次の実績が確認できます。

（Ensemble の検証）

MetaPRL の出発点となった目的です。博士論文の謝辞に、Nancy Lynch・Robbert van Renesse・Mark Hayden・Mark Bickford との共同研究として、Ensemble の検証と最適化に取り組んだことが書かれています。

（複数の論理の実装）

Nuprl 型理論をモジュール化して再定式化したもの、構成的および古典的な一階述語論理、Aczel の構成的集合論 CZF が、 MetaPRL の上に実装されました。CZF から Nuprl 型理論への関係づけは完全で、CZF の定理を Nuprl 型理論の中でそのまま使えます。

GitHub の README.md は、最終的に MetaPRL の上に実装された理論を、次のように列挙しています。

It implements Nuprl-style constructive/intuitionistic type theory (ITT) and hosts a remarkable range of related formal theories in one system ── Aczel's constructive set theory (CZF), the Edinburgh Logical Framework (LF), the Calculus of Inductive Constructions (CIC), higher-order and first-order logic, Kleene algebra with tests, justification logic, a compiler intermediate representation (FIR), and a POPLmark-challenge development ── with theories connected by derived-rule model translations.

（筆者訳）Nuprl 流の構成的・直観主義的型理論（ITT）を実装し、関連する形式理論の驚くべき範囲を 1 つのシステムに収めている。その範囲とは、Aczel の構成的集合論（CZF）、Edinburgh Logical Framework（LF）、Calculus of Inductive Constructions（CIC）、高階論理と一階論理、テスト付き Kleene 代数、正当化論理、コンパイラ中間表現（FIR）、POPLmark challenge の開発である。これらの理論は、導出規則によるモデル翻訳で接続されている。（derived-rule model translations。定訳がないため、本記事では「導出規則によるモデル翻訳」と訳した）

（JProver）

一階直観主義論理の完全な自動証明器で、 MetaPRL をツールキットとして使って実装されました。
対話篇 1 で述べたとおり、 MetaPRL の型理論と Nuprl に統合され、さらに Coq にも統合されました。

（コンパイラの形式化）

ML 系言語を x86 アセンブリにコンパイルする過程を、 MetaPRL の項と書き換え規則で形式的に記述する研究が行われました。

Hickey と Nogin の 2006 年の論文「Formal Compiler Construction in a Logical Framework」が、その成果です。

（抽象代数の形式化）

Xin Yu が、CZF の上で群の公理から出発して、部分群・準同型を形式化し、Klein の四元群を具体例として構成しました。

（基本的な数論の自動化）

Bryukhov・Kopylov・Krupski・Nogin が、 MetaPRL の上で基本的な数論を実装し、その証明を自動化しました。

タロウくん：
産業での利用はありますか？

専任講師：
コーネル大学の Nuprl System ページに、次の記述があります。

It is now used at Hughes Research Laboratory and at Moscow State University among other places.

（筆者訳）MetaPRL は現在、Hughes Research Laboratory とモスクワ国立大学をはじめとする場所で使われている。

Hughes Research Laboratory は、HRL Laboratories の旧称です。

Nogin が 2006 年に移った研究所で、DARPA や DHS の計画を請け負う産業の研究機関です。

MetaPRL は HRL で使われていました。
ただし、このコーネル大学のページがいつの時点の記述かは、ページに記されていません。
また、HRL でどの計画にどう使われたかも、この記述からは分かりません。

Ensemble は BBN・Nortel Networks・NASA が使っていましたが、それは Ensemble というツールキットの話であって、 MetaPRL がそれらの組織で使われたということではありません。

HRL での利用を裏づける別の資料として、HRL Laboratories の 2019 年の米国特許があります。

「ソフトウェアのセキュリティ目標をコードの性質に翻訳するシステム」という特許で、 MetaPRL を利用可能な定理証明器として挙げ、その理由を 4 つ述べています。

logical framework であること、コンパイラ実装での実績があること、ヒューリスティクスの指定がしやすいこと、証明の再利用がしやすいこと、です。

ただし、特許は「非限定的な例として」と述べており、この特許の発明で実際に MetaPRL が使われたかどうかは特許本文からは分かりません。

コーネル大学のページの記述と合わせると、HRL で MetaPRL が使われていたことは確からしいですが、製品や運用システムに組み込まれたかどうかは、筆者が確認した範囲では分かりません。

研究資金は、米海軍研究局の MURI 計画、DARPA、米空軍、Lee Center、NSF から出ています。

出典：

J. Hickey ほか, "MetaPRL – A Modular Logical Environment", TPHOLs 2003, §6.

jyh/metaprl README.md. https://github.com/jyh/metaprl

J. Hickey, A. Nogin, "Formal compiler construction in a logical framework", Higher-Order and Symbolic Computation 19(2-3), pp. 197-230, 2006.

US Patent 10,402,584. https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/10402584

【対話篇 8】いつ作られ、いまも使われているか

タロウくん：
いつ設計・開発された言語（定理証明支援系）で、2026 年 9 月のいまもつかわれていますか？

専任講師：
年表にします。

年	出来事
1969 年	Bates と Constable が PRL 方法論を始める
1983 年	最初の PRL システム λ-PRL が公開される
1984 年	Nuprl 1 が公開される
1992 年	Hickey がコーネル大学の博士課程に入る
1996 年 1 月	MetaPRL が構想される（コーネル大学の「MetaPRL history and people」ページによる）
1996 年	Nogin が計画に参加する
1997 年	Nuprl-Light として CADE-14 で発表される
1998 年	モスクワ国立大学のチームが参加する。MetaPRL に改名される
2001 年 1 月	Hickey の博士論文。version 0.6 が公開されている
2003 年	TPHOLs 2003 で 15 名の共著論文が発表される
2006 年	Hickey と Nogin のコンパイラ形式化の論文が出る。Nogin が HRL Laboratories に移る
2010 年 10 月	svn.metaprl.org の metaprl/ への最終コミット
2017 年	開発が凍結される（README.md の記述による）
2019 年	HRL Laboratories の特許が MetaPRL を利用可能な定理証明器として挙げる
2026 年 7 月	GitHub の jyh/metaprl に historical status banner が追加され、2017 年の凍結が明記される

（2026 年 9 月のいま、使われているか）

筆者が確認した範囲では、活発な利用は確認できません。根拠は 3 つです。

1 つ目。GitHub の jyh/metaprl リポジトリの README.md に、次のように明記されています。

Status: archived / historically frozen (2017). Preserved as a research artifact and a record of two decades of proof-assistant engineering.

（筆者訳）状態：アーカイブ済み、2017 年に歴史的に凍結。研究成果物として、また 20 年にわたる証明支援系工学の記録として保存されている。

このバナーは 2026 年 7 月 21 日のコミット「Add historical status banner (2026 portfolio triage)」で追加されました。凍結そのものは 2017 年です。svn.metaprl.org の記録では、metaprl/ への最終コミットは 2010 年 10 月 18 日です。

2 つ目。同じ README.md が、復活に何が要るかを述べています。

A working build targets OCaml 4.05 with camlp5 7.02, driven by a 0.9.8-era OMake; none of those are drop-in against current toolchains. The mathematics in theories/ is written in MetaPRL's own camlp5 quotation syntax ── extended concrete syntax realised through camlp5 quotations and grammar extensions ── spread across several hundred source files (over 500 .ml files, the bulk of them using these term-quotation constructs). Reviving the system therefore means either resurrecting the exact legacy toolchain or porting both the quotation front end and the build to modern equivalents, on top of the system's own bootstrap of syntax extensions and filters. That is a substantial, research-grade porting project rather than a routine version bump.

（筆者訳）動作するビルドは OCaml 4.05 と camlp5 7.02 を対象とし、0.9.8 系の OMake で駆動される。いずれも現在のツールチェーンにそのまま差し替えられるものではない。theories/ の数学は MetaPRL 独自の camlp5 quotation 構文（camlp5 の quotation と文法拡張によって実現された拡張具象構文）で書かれており、数百のソースファイル（500 を超える .ml ファイルで、その大半がこの項 quotation 構文を使っている）に広がっている。したがってシステムを復活させるには、当時のツールチェーンをそのまま再現するか、quotation のフロントエンドとビルドの両方を現代の等価物に移植するかしなければならず、しかもシステム自身の構文拡張とフィルタのブートストラップの上で行うことになる。これは、routine な版の更新ではなく、相当な、研究水準の移植計画である。

OCaml 4.14.1 ではビルドできませんでした。
上の記述が、その理由です。

3つ目。

2010 年の svn 最終コミット以降、 MetaPRL を使った新しい研究成果は、筆者が確認した範囲では見当たりません。2019 年の特許は、2000 年代の成果を引用したものです。

タロウくん：
なぜ凍結されたのですか？

専任講師：
理由を述べた資料は、見当たりませんでした。
README.md にも、論文にも、凍結の理由は記されていません。

しかし、理由を推測することはできます。

Nogin が 2006 年に HRL Laboratories に移り、Hickey が Caltech から Google に移った。
主要な開発者が産業に移ったあと、svn への最終コミットが 2010 年で止まった。これらの事実は分かっていますが、それが凍結の理由だと述べた資料は見当たりません。

出典：

jyh/metaprl README.md. https://github.com/jyh/metaprl

svn.metaprl.org/commitlogs/. http://svn.metaprl.org/commitlogs/

【対話篇 9】後継は何を残したか

タロウくん：
MetaPRL 自体は凍結されたということですが、 MetaPRL の後継は、学術研究や産業でどのような実績がありますか？

専任講師：
MetaPRL の直接の後継システムは、筆者が確認した範囲では存在しません。

そこで「後継」という言葉を、3 通りに解釈して扱います。

Nuprl 系統の継続
MetaPRL の研究者の後の仕事
MetaPRL から生まれたプログラム

の3者です。

（Nuprl 系統の継続）

MetaPRL は Nuprl 4 の限界に対処するために作られましたが、 Nuprl 自体も並行して開発が続きました。

Nuprl 5
コーネル大学の Nuprl System ページによれば、FDL（Formal Digital Library）は Nuprl 5 の一般名で、Web サービスとして構想されていました。

Nuprl 4 はサポートを終了しています。
Nuprl 5 は既定でクラウドで動き、ローカルで動かすための仮想マシンも配布されています。

Nuprl in Coq
Rahli と Bickford が、 Nuprl の一部を Coq で実装し、検証しました。
Nuprl の意味論の正しさを、別の定理証明支援系で確かめようとする研究です。

EventML
Nuprl と協働する関数型プログラミング言語で、2012 年の ShadowDB（原論文の題は "A Replicated Database on a Synthesized Consensus Core"、合意アルゴリズムの核を合成して作った複製データベース）、2015 年の AVoCS 論文（Multi-Paxos の実装が実際に運用されているデータベースシステムで使われている）、2017 年の crash-tolerant state machine replication systems の論文に至ります。

前掲の記事「Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す」で引用した「実際に運用されているデータベースシステム」は、この ShadowDB を指している可能性が高いです。

ただし、AVoCS 論文の要旨はデータベースの名前を明記しておらず、断定はできません。

Nuprl を使った cubical type theory の意味論の形式化。Bickford が 2020 年に「Formalization of Cubical Type Theory in Nuprl」と「Cubical type theory with several universes in Nuprl」を発表しています。

ここで、区別が要ります。

Nuprl が De Morgan cubical を「採用する」
→ Nuprl 自身の型理論を cubical にする。前掲の記事で「該当なし」と述べたもの
Nuprl の中で De Morgan cubical を「形式化する」
→ Nuprl を使って、cubical type theory の意味論（cubical set モデル）を数学の対象として記述し、その正しさを証明する。 Nuprl 自身の型理論は非 cubical のまま

Bickford の 2020 年の仕事は、後者です。

Coq の中で cubical set モデルを形式化しても Coq が cubical になるわけではないのと同じで、 Nuprl の中で cubical type theory を形式化しても Nuprl は cubical になりません。

前掲の記事「なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜」で書いた「Cohen らの論文の意味論の大部分が Mark Bickford によって Nuprl で形式的に検証された」も、後者の意味です。整合しています。

前者（Nuprl が De Morgan cubical を採用したもの）は、筆者が確認した範囲では存在しません。

前掲の記事の表で「De Morgan cubical type theory で区間 I を扱える」かつ「computational type theory を採用」の欄を「該当なし」としたことは、本記事の時点でも変わりません。

現状。PRL Project の出版物一覧は 2020 年で止まっています。2021 年以降の出版物は、筆者が確認した範囲では一覧に掲載されていません。

（MetaPRL の研究者の後の仕事）

Jason Hickey
コーネル大学で博士号（2001 年）、Caltech（カリフォルニア工科大学）の助教授を経て、Google のソフトウェアエンジニアになりました。

Google では、Google のサービスを支える全世界規模の計算基盤（大規模分散計算資源の管理とスケジューリングのソフトウェア）を設計・開発するチームに属しています。

2013 年に『Real World OCaml』（O'Reilly）を Yaron Minsky・Anil Madhavapeddy と共著しました。

Aleksey Nogin
コーネル大学で博士号（2002 年 8 月）、Caltech の博士研究員（MetaPRL の開発コーディネータ兼主開発者）を経て、2006 年に HRL Laboratories に移りました。

HRL では 2022 年まで在籍し、DARPA の HACMS（High-Assurance Cyber Military Systems）、DHS の CloudCOP などの計画の PI を務め、2016 年に Center for Secure and Resilient Systems を設立し、約 3,100 万ドルの予算でサイバーセキュリティとソフトウェア信頼性の計画を率いました。

HRL の特許「ソフトウェアのセキュリティ目標をコードの性質に翻訳するシステム」は、 MetaPRL によるコンパイラ形式化の研究を引用しています。その後、Red Balloon Security の Head of Research を経て、Leidos の Formal Methods Engineer になりました。

Alexei Kopylov
コーネル大学で博士号（2004 年）のあと、Caltech、HRL Laboratories に移りました。

2003 年の LICS で発表した依存交差型（dependent intersection）は、Aaron Stump らの Cedille という定理証明支援系の基礎理論に引き継がれています。

MetaPRL の型理論研究が、別の定理証明支援系に引き継がれた具体例です。

（MetaPRL から生まれたプログラム）

JProver
opam に coq-jprover というパッケージがあります。

説明文によれば、JProver は Stephan Schmitt が最初に実装し、Nogin が MetaPRL に統合し、その後 Huang Guan-Shieng が MetaPRL から必要な ML コードを抽出して Coq に適応しました。

対応する Coq の版は 8.5（2016 年公開）と 8.6（2018 年公開）で、8.6 が最終です。
それ以降の Coq・Rocq への対応は、8.6 で止まっています。

OMake
Hickey が MetaPRL のビルドのために作ったビルドシステムで、ocaml-omake/omake として継続しています。

著者は Aleksey Nogin・Jason Hickey・Gerd Stolpmann で、現在のメンテナは Gerd Stolpmann です。

最新版 0.10.7 は 2024 年 12 月に opam に公開され、9 つのパッケージから使われています。

Fedora、Alpine Linux、MacPorts、Arch Linux で配布されています。

MetaPRL 自体は 2017 年に凍結されましたが、そのビルドのために作られた OMake は生き残っています。

タロウくん：
樹形図にしてもらえますか？

専任講師：
縦長の樹形図にします。水色の枠が 2026 年 9 月時点で継続しているもの、灰色の枠が凍結・終了したもの、金色の枠が論文として残っているが実装の継続はないもの、白い枠が区切りの見出しです。

この樹形図は、「 MetaPRL から派生したもの」と「 MetaPRL と並行して続いた Nuprl 系統」の両方を含んでいます。

Nuprl 5 は MetaPRL の後継ではなく、 MetaPRL が置き換えようとした Nuprl 4 の後継です。

樹形図では、その旨を Nuprl 5 の枠の中に明記しています。

出典：

Cornell University, PRL Project, "Nuprl System". https://nuprl-web.cs.cornell.edu/html/NuprlSystem.html

Cornell University, PRL Project, Knowledge Base. https://nuprl-web.cs.cornell.edu/PRLSeminar

O'Reilly 著者ページ（Hickey）. https://www.oreilly.com/pub/au/5794

The Org（Nogin）. https://theorg.com/org/red-balloon-security/org-chart/aleksey-nogin

dblp（Kopylov）. https://dblp.org/pid/06/588.html

"Syntax and Semantics of Cedille". https://arxiv.org/pdf/1806.04709

Rocq Prover packages, coq-jprover. https://rocq-prover.org/p/coq-jprover

ocaml-omake/omake（GitHub）. https://github.com/ocaml-omake/omake

ここまでのまとめ

本記事では、9 つの対話で MetaPRL を見てきました。

（対話篇 1）

MetaPRL は、 Nuprl の computational type theory を土台にした logical framework です。 Dedukti と構造は同じですが、土台が型なしである点が違います。 Dedukti は証明項を翻訳して再検査するのに対し、 MetaPRL は内部で定義された論理どうしを関係づけます。JProver の Coq 統合は、証明の移動ではなく、証明を作るプログラムの移動でした。

（対話篇 2）

型なしの土台とは、 Nuprl の項言語です。演算子の名前と束縛付きの部分項からなり、型を持ちません。fol_and.ml で、一階論理の「かつ」が、この項言語と camlp5 quotation 構文でどう書かれているかを読みました。

（対話篇 3）

MetaPRL のメタ論理は λΠ計算ではなく、型なし二階 Horn 節です。 Nuprl のプログラムが型なしで文脈に応じて複数の型を持つため、メタ論理も型なしにする必要がありました。

（対話篇 4）

LF は土台にも対象にもなります。土台の型の有無が、証明の検査の仕方を決めます。型なしの土台は型付きの枠組みを載せられますが、逆は、記述はできても型なしのまま計算することはできません。土台が型なしか型付きかで変わるのは、「型なしの体系を載せる」と「他の定理証明支援系の証明を持ち込む」の 2 点だけです。

（対話篇 5）

MetaPRL は pointwise と pairwise の両方をモジュールとして持っています。ソースコードのコメントに、Let 規則が pointwise で成り立たない理由の手がかり（商型の除去規則との衝突）がありました。

（対話篇 6）

動機は Ensemble の検証にありました。 Nuprl 4 のスケーラビリティとモジュール性の限界に対処するため、 Nuprl を小さく速く作り直したのが Nuprl-Light で、100 倍以上速くなりました。

（対話篇 7）

Ensemble の検証、10 以上の論理の実装、JProver、コンパイラの形式化、抽象代数の形式化に使われました。コーネル大学のページによれば HRL Laboratories でも使われていましたが、製品や運用システムに組み込まれたかどうかは分かりません。

（対話篇 8）

1996 年に構想され、2017 年に凍結されました。復活には研究水準の移植計画が要ります。凍結の理由を述べた資料は見当たりませんでした。

（対話篇 9）

直接の後継は存在しませんが、 Nuprl 系統・研究者・プログラムの 3 つの経路で派生物が生き残っています。 Nuprl 5 と EventML は産業で実際に使われ、Kopylov の依存交差型は Cedille に引き継がれ、OMake は 2024 年も更新されています。

（Executive Summary の結論に戻ります）

9 つの対話を踏まえて、Executive Summary で掲げた結論を確かめます。

土台に型付きの言語を置いた logical framework にしかできないことは、他の定理証明支援系が出力した証明項を持ち込み、型検査器が自動で再検査することです。

土台に型なしの言語を置いた logical framework にしかできないことは、 Nuprl の型理論のように項に型が貼り付いていない体系を、その項の計算をそのまま行いながら扱うことです。

型付きの枠組みを載せることと、論理どうしの関係を記述することは、どちらの土台でもできます。

MetaPRL は、コーネル大学が開発した分散通信システム Ensemble の検証のために 1996 年に構想され、1998 年に MetaPRL と改名されました。

Ensemble は研究に留まらず、BBN・Nortel Networks・NASA が軍事と商用の両方で使いました。

MetaPRL 自体が製品や運用システムに組み込まれたかどうかは、筆者が確認した範囲では分かりません。

2017 年に凍結され、直接の後継は存在しませんが、 Nuprl 5・EventML・OMake・Cedille の基礎理論に、派生物が生き残っています。

MetaPRL は、型なしの言語を土台にした logical framework の、筆者が調べた範囲では唯一の例です。

1 つのプログラムを文脈に応じて異なる型に帰属させる処理が多い用途では、型なしの土台の方が向いています。

土台に型付きの言語を置くべきか、型なしの言語を置くべきかには、一般的な答えはなく、用途で決まります。

証明の相互運用が目的なら型付き、型なしの体系をそのまま扱うことや文脈に応じた帰属が目的なら型なし、どちらでもなければ自動化しやすい型付きが実務では扱いやすい、というのが筆者の見解です。

【型付きの土台の方が優れている点】

項目	型付きの土台（Dedukti・Isabelle）	型なしの土台（MetaPRL）との比較
型検査	決定可能。必ず有限時間で終わる	型なしの土台では決定不能
証明の再検査	証明項を受け取れば、型検査器が自動で再検査する	型なしの土台では、定理証明エンジニア（人）がタクティクで導出を組み立てる必要がある
他の定理証明支援系との連携	Lean 4・Rocq・HOL Light の証明を翻訳して持ち込める（証明の相互運用）	型なしの土台では、この仕組みが成り立たない
自動化	証明項があれば、人手を介さずに検査が終わる	型なしの土台では、自動化はタクティクによる部分的なものに留まる

【型なしの土台の方が優れている点】

項目	型なしの土台（MetaPRL）	型付きの土台（Dedukti・Isabelle）との比較
型なしの体系を扱う	Nuprl の型理論のような、項に型が貼り付いていない体系を、項の計算をそのまま行いながら扱える	型付きの土台では、データとして記述はできるが、項の計算の仕組みを作り直す必要がある
文脈に応じた型への帰属	1 つのプログラムを、型システムを拡張せずに、文脈に応じて異なる型に帰属させられる	型付きの土台では、多相型・交差型・部分型を型システムに組み込む必要があり、組み合わせると型検査が複雑になる
新しい型の追加	新しい型を定義し、既存の項がその型に属するかを判断として後から与えられる	型付きの土台では、新しい種類の型が必要になると、型システムそのものを拡張しなければならない
プログラムコードの検証	実際のプログラムコードを型なしのまま扱えるので、大規模システムの検証に向く。 MetaPRL は Ensemble の検証のために作られた	型付きの土台では、プログラムに型を付けて符号化する必要がある

logical framework の用途は、土台の型理論の選び方で決まります。
MetaPRL は、型なしの土台を選んだときに何が起きるかを、20 年の開発で示しました。

📌 用語のミニ解説

📌 本文に登場した用語の、初心者向けミニ解説

MetaPRL（メタピーアールエル）

コーネル大学の PRL グループで、Constable の指導のもと Jason Hickey が博士研究として設計し、実装した logical framework です。 Nuprl の computational type theory を土台にして、その上に複数の論理を載せられます。1996 年に構想され、1997 年に Nuprl-Light として発表され、1998 年に改名され、2017 年に凍結されました。

logical framework

論理体系そのものを記述するための言語です。ひとつの型理論を土台に固定し、その土台を用いて複数の論理体系を記述します。 Edinburgh LF、 Twelf、 Isabelle/Pure、 Dedukti、 MetaPRL が属します。

項言語（term language）

MetaPRL の型なしの土台です。演算子の名前と、束縛変数付きの部分項からなります。 Nuprl の項の構文をそのまま使っています。

メタ言語（meta-language）

別の言語について語るための言語です。英語の文法を日本語で説明するとき、説明に使う日本語がメタ言語で、説明される英語が対象言語です。logical framework では、論理体系を記述するための言語がメタ言語で、記述される論理体系が対象言語です。本記事では「土台」と呼んでいます。

camlp5 quotation

OCaml の構文拡張の仕組み camlp5 を使って、 MetaPRL の項言語を OCaml のソースコードの中に書けるようにした記法です。declare・prim・prim_rw・sequent { … } などが、この記法です。言語ではなく、記法です。

dT（decompose タクティク）

MetaPRL の主要なタクティクです。dT 0 は結論の形を見て intro リソースから合う規則を選んで適用し、dT n（n は 1 以上）は n 番目の仮説の形を見て elim リソースから合う規則を選んで適用します。規則の名前を指定せず、形から自動で選ぶ点が、 RedPRL の refine との違いです。

intro リソース・elim リソース

MetaPRL で、推論規則を登録しておく登録簿です。{| intro [] |} というアノテーションを付けた規則は intro リソースに、{| elim [] |} を付けた規則は elim リソースに登録されます。dT は、この登録簿から規則を探します。

深い埋め込み（deep embedding）

ある体系を、別の体系の中に「データ」として持ち込む方法です。 Nuprl の項を、λΠ計算の中で Term という 1 つの型のデータとして表し、「この Term が Nuprl の型 A に属する」を Term 上の述語として書く、というのがその例です。持ち込んだ体系の計算は、持ち込み先で改めて定義し直す必要があります。

二階 Horn 節

Prolog の基礎になっている Horn 節を、述語や関数そのものを変数にできる二階の形に拡張したものです。 MetaPRL のメタ論理は、 Nuprl の項の上の型なし二階 Horn 節です。推論規則を「前提の並びから結論を導く」という Horn 節の形で記述します。

proof extract

推論規則に付いている証明の計算的内容を定義する項です。前提の証明から結論の証明を組み立てるプログラムにあたります。prim and_intro … = pair{'a; 'b} の pair{'a; 'b} がそれです。

Ensemble

コーネル大学で開発された群通信のツールキットです。複数の計算機のあいだでメッセージを確実に届け、故障に耐える働きをします。BBN・Nortel Networks・NASA が使っていました。 MetaPRL の動機は、Ensemble の検証にありました。

JProver

一階直観主義論理の完全な自動証明器です。Stephan Schmitt が実装し、Nogin が MetaPRL に統合し、Huang Guan-Shieng が Coq に適応しました。 Coq 8.6 が最終対応版です。

OMake

Hickey が MetaPRL のビルドのために作ったビルドシステムです。 MetaPRL から独立して ocaml-omake/omake として継続し、2024 年 12 月に 0.10.7 が公開されました。

pointwise functionality と pairwise functionality

「等しい値を代入したら等しい結果になる」という約束の 2 つの決め方です。pointwise は 1 つの値を先に固定してから約束し、pairwise は等しい値の組すべてについてまとめて約束します。 Nuprl は pointwise、 MetaPRL は両方をモジュールとして持ちます。

Cedille

Aaron Stump らが開発した定理証明支援系です。Kopylov の依存交差型を基礎理論のひとつとしています。

実機検証について

本記事では、 MetaPRL を筆者の環境で動かすことを試みましたが、ビルドに至りませんでした。

検証環境

構成要素	版
OCaml	4.14.1
MetaPRL	master（最終コミット 2026 年 7 月 21 日。GitHub jyh/metaprl をクローン）

検証できたこと

GitHub の jyh/metaprl をクローンし、theories/ ディレクトリの構成と、theories/fol/fol_and.ml・theories/itt/core/itt_pairwise.ml・theories/itt/extensions/pointwise/itt_pointwise.ml・theories/itt/core/itt_struct3.ml のソースコードを読んだ。
doc/htmlman/user-guide/mp-axiom.html で、proof extract の用語を確認した。
mk/defaults で、要求される OCaml の版が 4.02.3 または 4.05.0 であることを確認した。

検証できなかったこと・注意

MetaPRL のビルドは行っていない。README.md が述べるとおり、OCaml 4.05・camlp5 7.02・OMake 0.9.8 系のツールチェーンが必要で、OCaml 4.14.1 では動かない。README.md はこれを「研究水準の移植計画」と呼んでいる。
したがって、本記事のコードはすべて、GitHub のソースコードを読んだものであり、筆者の環境で実行した結果ではない。対話篇 2 の fol_and.ml の解説は、コードの読解にもとづく。
Nuprl 5 ・EventML・JProver・OMake も、筆者の環境では実行していない。

訂正一覧

公開後に訂正した箇所を、ここに追記していきます。現時点ではありません。

本記事の接続先

Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す
https://qiita.com/etale_cohomology/items/a830a5ac5013a298fb97
computational type theory の「計算が先、型が後」という順序を扱いました。本記事の対話篇 3 で、 MetaPRL のメタ論理が型なしである理由の背景です。
なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜
https://qiita.com/etale_cohomology/items/4035a0b3f4d40766437c
MetaPRL を名前だけ挙げました。pointwise と pairwise のコラムがあります。本記事の対話篇 5 で、その続きを扱いました。
【Dedukti入門 ③】Logical Framework とは何か ── 1967 年の Automath から Isabelle、1987 年の Edinburgh LF、そして Dedukti へ
https://qiita.com/etale_cohomology/items/517744003ff48cd77079
logical framework の 5 者比較表を掲げました。本記事の対話篇 1 で、 MetaPRL の行を加えました。
【Dedukti入門 ④】Dedukti に、産業実績はあるのか
https://qiita.com/etale_cohomology/items/184400900114ca3e4a39
Dedukti の翻訳器一覧を掲げました。 Nuprl 系の翻訳器が無いことの背景が、本記事の対話篇 3 と 4 にあります。
λProlog とは何か ── AI が数学を証明する時代、定理証明系 Rocq の内側で働く知られざる言語
https://qiita.com/etale_cohomology/items/98b416523f468dc64959
論理プログラミングの系統を扱いました。 MetaPRL の「論理プログラミング環境」という性格と、メタ論理の Horn 節が、この記事とつながります。
依存型を使わないIsabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか
https://qiita.com/etale_cohomology/items/6987c76966a3513cd6e0
Isabelle/Pure という型付きのメタ論理と、Isar という宣言型の証明記述方式を扱いました。 MetaPRL のメタ論理は Isabelle の考え方を型なしに修正したもので、本記事の「本記事について」と対話篇 3 で対比しました。
Haskell から始める型理論の家系図 — 単純型付きラムダから HoTT まで
https://qiita.com/etale_cohomology/items/f2aa70cdc826e15979a4
型理論の系譜を単純型付きラムダ計算から HoTT まで辿りました。 Twelf を論理プログラミングと依存型の合流として紹介しており、本記事の対話篇 1 で参照しました。
【Arend 連載（最終回）】AIによる数学定理証明プロジェクトは Lean 4 を採用した ── Arend 言語仕様の設計判断は、それでも学ぶ意義はあるか
https://qiita.com/etale_cohomology/items/3b332aa9c22ebe838c5c
証明の記述方式（Isar・タクティク・項スタイル）の 3 分類を表にまとめました。本記事の「本記事について」で、PRL 系がタクティク方式であることを述べる際に参照しました。

出典一覧

J. J. Hickey, "The MetaPRL Logical Programming Environment", PhD thesis, Cornell University, Ithaca, NY, January 2001. https://nuprl-web.cs.cornell.edu/documents/Hickey/Hickeythesis.pdf
J. Hickey, A. Nogin, R. L. Constable, B. E. Aydemir, E. Barzilay, Y. Bryukhov, R. Eaton, A. Granicz, A. Kopylov, C. Kreitz, V. N. Krupski, L. Lorigo, S. Schmitt, C. Witty, X. Yu, "MetaPRL – A Modular Logical Environment", TPHOLs 2003, LNCS 2758, pp. 287-303. DOI: 10.1007/10930755_19. https://www.cs.uni-potsdam.de/ti/kreitz/PDF/03tphols-metaprl.pdf
J. Hickey, A. Nogin, "Formal compiler construction in a logical framework", Higher-Order and Symbolic Computation 19(2-3), pp. 197-230, 2006.
A. Nogin, "Theory and Implementation of an Efficient Tactic-Based Logical Framework", PhD thesis, Cornell University, August 2002.
A. Kopylov, "Type Theoretical Foundations for Data Structures, Classes, and Objects", PhD thesis, Cornell University, 2004. https://www.cs.cornell.edu/people/kopylov/papers/thesis/thesis.pdf
A. Kopylov, "Dependent Intersection: A New Way of Defining Records in Type Theory", LICS 2003, pp. 86-95. DOI: 10.1109/LICS.2003.1210048
jyh/metaprl（GitHub）. https://github.com/jyh/metaprl
jyh/metaprl, theories/fol/fol_and.ml. https://github.com/jyh/metaprl/blob/master/theories/fol/fol_and.ml
jyh/metaprl, theories/itt/core/itt_dfun.ml. https://github.com/jyh/metaprl/blob/master/theories/itt/core/itt_dfun.ml
svn.metaprl.org/commitlogs/. http://svn.metaprl.org/commitlogs/
Cornell University, PRL Project, "Nuprl System". https://nuprl-web.cs.cornell.edu/html/NuprlSystem.html
Cornell University, "MetaPRL history and people". https://www.cs.cornell.edu/jyh/metaprl/mp-people.html
Cornell University, PRL Project, Knowledge Base. https://nuprl-web.cs.cornell.edu/PRLSeminar
V. Rahli, D. Guaspari, M. Bickford, R. L. Constable, "Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML", AVoCS 2015, ECEASST Vol. 72. https://eceasst.org/index.php/eceasst/article/view/2195
US Patent 10,402,584, "System and method for translating security objectives of computer software to properties of software code", HRL Laboratories, 2019. https://image-ppubs.uspto.gov/dirsearch-public/print/downloadPdf/10402584
O'Reilly, Jason Hickey 著者ページ. https://www.oreilly.com/pub/au/5794
The Org, Aleksey Nogin. https://theorg.com/org/red-balloon-security/org-chart/aleksey-nogin
dblp, Alexei Kopylov. https://dblp.org/pid/06/588.html
A. Stump ほか, "Syntax and Semantics of Cedille", arXiv:1806.04709. https://arxiv.org/pdf/1806.04709
Rocq Prover packages, coq-jprover. https://rocq-prover.org/p/coq-jprover
ocaml-omake/omake（GitHub）. https://github.com/ocaml-omake/omake
nLab, "NuPRL". https://ncatlab.org/nlab/show/NuPRL
D. S. Scott, "Data Types as Lattices", SIAM Journal on Computing 5(3), pp. 522-587, 1976.
R. Harper, F. Honsell, G. Plotkin, "A Framework for Defining Logics", LICS 1987, pp. 194-204. 拡張版：Journal of the ACM 40(1), pp. 143-184, 1993.
B. C. Pierce, Types and Programming Languages, MIT Press, 2002.
D. B. Lenat, "EURISKO: A Program That Learns New Heuristics and Domain Concepts", Artificial Intelligence 21(1-2), pp. 61-98, 1983.
M. Gordon, R. Milner, C. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, LNCS 78, Springer, 1979.
R. L. Constable ほか, Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986. https://nuprl-web.cs.cornell.edu/book/
S. F. Allen ほか, "The Nuprl Open Logical Environment", CADE-17, LNAI 1831, pp. 170-176, 2000.
RedPRL/sml-redprl（GitHub）. https://github.com/RedPRL/sml-redprl
RedPRL/redtt（GitHub）. https://github.com/RedPRL/redtt
RedPRL/cooltt（GitHub）. https://github.com/RedPRL/cooltt
The RedPRL Development Team, "The red* family of proof assistants". https://redprl.org/

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up