【Dedukti入門 ②】Lean 4 の型理論も HOL Light の高階論理も、なぜ同じ言語で書けるのか ── Dedukti の言語 λΠ計算 modulo rewriting を実物のコードで読む

この連載について

本記事は、Dedukti という言語を扱う連載の 2回目 です。
全体で何回になるかは決めていません。

回	扱うこと
初回	定理証明支援系が出力した証明項を、翻訳器が .dk ファイルに翻訳し、Dedukti が検査する仕組み
2 回目（本記事）	Dedukti の言語そのもの。識別子の宣言と書き換え規則の 2種類で、論理体系と型理論を記述する
3 回目	Logical Framework という考え方。Edinburgh LF、Twelf、Isabelle/Pure との関係
4 回目	Dedukti の実績と限界。年表、翻訳器、利用者、産業配備

初回記事 はこちらです。

この記事について

初回記事では、翻訳器 が 符号化ファイル という 固定ルール を持っていること、符号化ファイル には 識別子の宣言 と 書き換え規則 が記述されていることを述べました。ただし、その内容には足を踏み入れませんでした。

連載２回目 となるこの記事では、その内を主題として取り上げます。
コード例を見ながら、次の 2 点を説明します。

1. 識別子の宣言 だけで、命題論理の推論規則 を 記述できる こと。
2. 書き換え規則 を 加える と、証明項が小さくなる こと。

コードはすべて筆者の環境で実行し、Dedukti が .dk ファイルの型検査を通すことを確かめました。

なお、実行環境と手順については、記事末尾の 「実機検証について」 に掲載しております。

前回の 初回記事をお読みでない方でも 、この記事を単体の記事としてお読みいただくことができるように執筆致しました。

本記事中の専門用語は、初出時にわかりやすく解説するように心がけました。また、記事末尾にも用語のミニ解説を置きました。

入門者向けの分かりやすい解説を優先する執筆方針をとりましたので、中上級者や専門家の方からご覧になると、厳密な議論を欠いている点や、議論を単純化している点など、精密な定義をするようご指導をいただいてしまう点もあろうかとは思いますが、分かりやすさを優先した故の簡便的な説明や定義付けであることをご寛恕頂けますと幸いです。

本記事の流れ

金色の枠が対話篇、📌 は折り畳みコラムです。
本文は、対話篇とコラムをすべて飛ばしても、上から下へ通して読めるように書いてあります。

---

第 1 章 ── 共通の言語の正体

λΠ計算 modulo rewriting

ここまで、「共通の言語」 という表現を繰り返してきました。
ここで、「共通の言語」に与えられた学術的な名称を紹介します。

.dk ファイル に記述されるのは、「λΠ計算 modulo rewriting」（ラムダ・パイ計算 モジュロ・リライティング） の 項 です。

「λΠ計算 modulo rewriting」 は、複数の単語で構成された名詞です。
そこで、単語の構成要素に切り分けて、その意味を見ていきます。

「λΠ計算 modulo rewriting」 は、次の3つの構成要素から成ります。

• $λΠ$ ── ギリシャ文字のラムダとパイです。
  $λ$ は 関数を作る記号 であり、
  $Π$ は 関数の型を表す記号 です。

この $λΠ$ は、「この 2 つを持つ 計算体系 である」、という意味です。

なお、$Π$ は円周率の $π$ と同じギリシア文字の大文字ですが、円周率とは関係ありません。

• rewriting ── 書き換え のことです。
  「この式は、この式に置き換えてよい」という指示 を、書き換え規則 と呼びます。
  たとえば、「plus 2 2 は $4$ に置き換えてよい」という 規則です。
   
• modulo ── 「〜のもとで」 という意味のラテン語です。
  数学にあっては、「7 は 4 を法（modulo）として 3 に等しい」のように使い、ある約束のもとで 2 つを同じとみなす、という場面で姿を現す言葉です。
  「λΠ計算 modulo rewriting」の文脈では、「書き換え規則のもとで」という意味合い になります。
  書き換えた結果が一致すれば、2 つの式を同じものとして扱う、ということです。
   
  以上を整理すると、「λΠ計算 modulo rewriting」 とは、「λ と Π を持つ計算体系に、書き換え規則を足したもの」 という意味になります。

ところで、項 とは何でしょうか。

項 は、この計算体系の文法にしたがって組み立てた 式のこと です。

プログラミング言語でいう「式」にあたります。.

dk ファイルに記述される中身は、すべて 項 です。

「λΠ計算 modulo rewriting」 の項 とは、次の 3 つを組み合わせて作った式のことです。

• 変数 。$a$ や $x$ のように、あとで値が入る箇所を表す記号です。
   
• $λ$（ラムダ）による 関数の定義 。「x を受け取って、○ を返す関数」を表します。Dedukti のファイルでは x => ○ と記述します。
   
• $Π$（パイ）による関数の型。「型 $A$ の値 $x$ を受け取って、型 $B$ の値を返す関数」という型を表します。Dedukti のファイルでは x : A -> B と記述します。ここで $B$ は、返り値の型です。
   
  $x$ に入る値によって、$B$ がどの型になるかが 変わる、という書き方 もできます。
  たとえば n : Nat -> Vector n と書くと、n に 3 が入れば返り値の型は Vector 3、n に 5 が入れば Vector 5 になります。このように、値によって決まる型 のことを、依存型 と呼びます。

ところで、関数の型 に $Π$ という記号わざわざをあてがう（紐づける）必要性について、腑に落ちないと思われた方もおられるかもしれません。

これは、集合の直積に由来 します。

$x$ に入る値によって $B$ がどの型になるかが変わるとき、そうした関数をすべて集めた集合 は、$x$ が取りうる値それぞれに対応する $B$ の 直積 と一致します。

直積 は、数学では $Π$（総乗）の記号 で書き表します。
そこから、依存型の関数の型 を $Π$ 型 と呼ぶようになりました。

同じ理由で、「$x$ の値と、それに応じた型 $B$ の値の組」を集めたものは、$Σ$ 型（依存和） と呼ばれます。

こちらは 足し算 の $Σ$ に由来します。

Deduktiという言語そのものに備わっているのは $Π$ だけです。
$Σ$ は、必要になったときに 符号化の中で宣言 します。

ここまでは、型付きラムダ計算と同じ です。

「λΠ計算 modulo rewriting」 が、依存型に加えて持つのが、書き換え規則 です。

書き換え規則 とは、「この式は、この式に置き換えてよい」という指示です。

たとえば「plus 2 2 は 4 に置き換えてよい」という規則を記述しておくと、Dedukti は型検査のときに plus 2 2 と 4 を同じものとして扱います。

modulo rewriting という名前は、「書き換え規則のもとで」という意味 です。

証明が項として記述される 理由は、次のとおりです。

「$A$ ならば $A$」という命題の証明は、「$A$ の証明を受け取って、受け取った $A$ の証明をそのまま返す 関数 」として表現することが可能です。

関数を項として記述したもの が、 証明項 です。

Dedukti は、証明項の型を検査 し、型が「A ならば A」という命題 に一致するかを判定 します。

なぜ、複数の論理体系を 1 つの言語に記述できるのか

依存型 と 書き換え規則 の 2つ で、Lean 4 の 型理論 も、Rocq の 型理論 も、HOL Light の 高階論理 も、記述することができます。

記述する先は、拡張子が .dk のテキストファイルです。

.dk ファイルに何をどう書いてよいかを定めた文法が、λΠ計算 modulo rewriting です。依存型と書き換え規則の 2 つは、この文法が備えているものです。

この記事ではこれ以後、この文法のことを 言語 と呼びます。
プログラムを書くための文法を C 言語や Python と呼ぶのと同じ使い方です。

（ なお、上記で「言語」という単語を用いたのは、この記事独自の定義です。
Dedukti の 開発チーム Deducteam の文書では、 「λΠ計算 modulo rewriting」 は logical framework または type system と呼ばれ、Dedukti は その実装（implementation） と呼ばれています。
「言語」という語は Dedukti 自体を指して使われることもあり、厳密な使い分けはされていません ）

では、λΠ計算 modulo rewriting（という「言語」）で書かれた .dk ファイルが、どのようなものかを見ておきます。次の 4 行は、命題論理の含意を記述したものです。

    prop     : Type.
    def Prf  : prop -> Type.
    imp      : prop -> prop -> prop.

    [a, b] Prf (imp a b) --> Prf a -> Prf b.

上記のコードを、1 行ずつ解説します。

1 行目 prop : Type.

prop という識別子を新しく宣言しています。: Type は「prop は型である」という意味です。Type は、この言語が最初から持っている識別子で、「これは型だ」と述べるために使います。

では、prop とはどういう型でしょうか。命題を集めた型です。「2 は素数である」も「1 + 1 = 2」も、prop という型に属します。プログラミング言語でたとえるなら、整数を集めた型に int という名前が付いているのと同じで、命題を集めた型に prop という名前を付けた、ということです。

この 1 行によって、Dedukti は prop という型を使えるようになります。逆にいえば、この 1 行を書くまで、Dedukti は命題というものを知りません。命題を扱いたいなら、まず命題の型を宣言するところから始めます。

2 行目 def Prf : prop -> Type.

Prf という識別子を宣言しています。

prop -> Type は「prop に属するものを 1 つ受け取って、型を返す」という意味です。

命題 a を渡すと、Prf a という型が返ります。
Prf a は「命題 a の証明が属する型」です。

命題 a が証明できるとき、Prf a に属する項が存在します。
行頭の def は、この識別子が書き換え規則の左辺に現れることを Dedukti に伝える印です。
4 行目で実際に現れます。

3 行目 imp : prop -> prop -> prop.

imp という識別子を宣言しています。
prop -> prop -> prop は「prop に属するものを 2 つ受け取って、prop に属するものを返す」という意味です。

命題 a と命題 b を渡すと、imp a b という新しい命題が返ります。
imp a b は「a ならば b」を表します。

ここまでの 3 行が、識別子の宣言です。

prop -> Type のように、矢印を使って「何を受け取って何を返すか」を書く部分が、依存型の書き方 にあたります。

4 行目 [a, b] Prf (imp a b) --> Prf a -> Prf b.

書き換え規則 です。
行頭の [a, b] は、この規則の中で a と b を変数として使う、という宣言です。
--> の左が置き換え前、右が置き換え後 です。

左辺の Prf (imp a b) は「a ならば b、という命題の証明が属する型」です。右辺の Prf a -> Prf b は「a の証明を受け取って、b の証明を返す関数の型」です。

この規則は、その 2 つを同じものとして扱ってよい、と述べています 。

つまり、「a ならば b を証明すること」と「a の証明から b の証明を作る関数を書くこと」は同じだ、と 1 行で宣言しています 。

（画像内に 2 か所、誤りがあります。「関数書くこと」は「関数を書くこと」、Prf は def Prf が正しい表記です）

λΠ計算 modulo rewriting で書けるものは、識別子の宣言と、書き換え規則の2種類しかありません。

これ以後、記事に掲載するコードは、識別子の宣言 と、書き換え規則 の どちらか です。

Dedukti は、この言語で書かれた .dk ファイルを読み込み、型検査するプログラムです。

言語の名前が λΠ計算 modulo rewriting、
プログラムの名前が Dedukti です。

この記事では、言語そのもの を指すときは λΠ計算 modulo rewriting と表記し、
プログラム を指すときは Dedukti と記載します。

ここまで、λΠ計算 modulo rewriting がどういう言語なのかについて、論じてきました。

それでは、なぜ、この2種類だけで、Lean 4 の型理論や HOL Light の高階論理まで
記述できるのでしょうか？

仕組みは 2 つ あります。
以下、順に見ていきます。

仕組み 1 ── 推論規則を、記号の宣言として記述する

論理体系 は、記号と推論規則の集まり です。

記号 と 推論規則 は、そのまま 識別子の宣言として .dk ファイルに記述されます 。

命題論理の含意を例にします。
まず、記号を 3 つ宣言します。

prop : Type.
Prf  : prop -> Type.
imp  : prop -> prop -> prop.

• 1 行目は、命題の全体を表す型 prop を宣言しています。
• 2 行目は、命題 a を受け取って「a の証明の型」を返す Prf を宣言しています。
• 3 行目は、命題 a と命題 b から命題「a ならば b」を作る imp を宣言しています。

次に、含意の推論規則を 2 つ宣言します。

imp_intro : a : prop -> b : prop -> (Prf a -> Prf b) -> Prf (imp a b).
imp_elim  : a : prop -> b : prop -> Prf (imp a b) -> Prf a -> Prf b.

imp_intro が 含意の導入規則 です。

「a の証明から b の証明を作る関数」を受け取って、「a ならば b」の証明を返す、と読みます。

imp_elim は、含意の除去規則 です。

除去規則 とは、すでに組み立てた命題を 使う側の規則 です。

「a ならば b」という命題をすでに持っているとき、そこから b を取り出すには、a の証明が必要です。

この規則は、「a ならば b」の証明と a の証明を受け取って、b の証明を返す、と読みます。
数学の証明で「A ならば B が成り立つ。いま A が成り立つ。よって B が成り立つ」と書く場面が、これにあたります。

• 導入規則 が 命題を組み立てる側
• 除去規則 が 組み立てた命題を使う側

です。

論理体系の推論規則は、この 2 種類が対になっています。
含意だけでなく、連言にも選言にも、それぞれ導入規則と除去規則があります。

教科書に書かれた推論規則が、そのまま識別子の型として記述できています。

ここまでで、論理体系の定義が終わりました。

この定義 の上で、証明を項として 書き表すことができます。
「a ならば a」の証明です。

def identity : a : prop -> Prf (imp a a)
  := a : prop => imp_intro a a (x : Prf a => x).

Dedukti は、この項の型を検査します。

宣言した imp_intro の型と、組み立てた項が整合していれば、Dedukti はこのコードの型検査を通します。

このコードは、筆者の環境で型検査を通りました。

ところで、論理体系が変われば、宣言する記号と規則も変わります。

• 高階論理であれば、量化子の規則を宣言し、
• Lean 4 の型理論であれば、宇宙と帰納型の規則を宣言します。

宣言の中身は変わりますが、宣言を記述する言語は同じです。
Dedukti のソースコードにも、手を加える必要はありません。

仕組み 2 ── 計算による等しさを、書き換え規則で吸収する

仕組み 1 だけでは足りません。

Lean 4 と Rocq は、型検査の途中で 計算を行い、計算した結果が同じなら同じ型だと判定します 。
この判定を 定義的等価性（definitional equality） と呼びます。
定義的等価性の中身は、型理論ごとに違います 。

書き換え規則 が、この違いを吸収します。

（画像の左側で、下段の2つの図形は同じ輪郭を意図しています。また、右側の .dk ファイル内の矢印は、塗りつぶしと輪郭線で描き分けられていますが、両者に違いはありません。いずれも書き換え規則を表しています）

prop     : Type.
def Prf  : prop -> Type.
imp      : prop -> prop -> prop.

[a, b] Prf (imp a b) --> Prf a -> Prf b.

最後の行が 書き換え規則 です。

「a ならば b の証明の型」は「a の証明から b の証明への関数の型」 に置き換えてよい、と宣言しています 。

含意の導入規則と除去規則を、独立した記号として宣言していません。

関数を作ることが導入規則にあたり、関数を適用することが除去規則にあたる、と規則そのもので言い切っています。

この宣言の上では、「a ならば a」の証明は 恒等関数そのもの になります。

def identity : a : prop -> Prf (imp a a)
  := a : prop => x : Prf a => x.

ところで、仕組み 1 で掲載したコードにあった imp_intro が消えています。

Dedukti が型検査の途中で Prf (imp a a) を Prf a -> Prf a に書き換え、恒等関数の型と一致させたからです。このコードは、筆者の環境で型検査を通りました。

書き換え規則の役割 は、ここにあります。

Dedukti の型検査器は、2 つの型が等しいかどうかを判定するとき、書き換え規則を繰り返し適用します。

適用できる規則がなくなるまで書き換え、それ以上書き換えられない形にしてから、2つを見比べます。
この繰り返しの適用が、計算にほかなりません。

plus 2 2 を 4 にするのも、Prf (imp a a) を Prf a -> Prf a にするのも、規則を適用して式を変形していく点では 同じ です。

前者を計算と呼ぶなら、後者も計算です。

ここから、次のことが言えます。

元の論理体系で計算として処理されていた部分を、Dedukti の型検査器の計算として、そのまま処理できます。片方で計算だったものが、もう片方でも計算になります。

書き換え規則が無ければ、この部分は証明項の中に明示的な手順として現れ、証明項は大きくなり、元の証明とは形が離れます。

なお、書き換え規則の中身は、定理証明支援系によって異なります。

Lean 4 の定義的等価性は Lean 4 用の書き換え規則として、
HOL Light の定義的等価性は HOL Light 用の書き換え規則として、
それぞれ別々の .dk ファイルに記述します。

書き換え規則を記述するときに使う言語は、どちらも「λΠ計算 modulo rewriting」です。

（画像内の矢印は、いずれも書き換え規則を表しています。長さや太さ、灰色の棒との組み合わせに違いがありますが、これらの違いに意味はありません。規則の本数と並びが定理証明支援系によって異なることを示しています）

仕組み 1 と 仕組み 2 の対比

比べる項目	仕組み 1（宣言だけ）	仕組み 2（書き換え規則あり）
記述する対象	論理体系の推論規則	論理体系の定義的等しさ
.dk ファイルでの書き方	記号の宣言	書き換え規則
含意の書き方	imp_intro と imp_elim を宣言する	[a, b] Prf (imp a b) --> Prf a -> Prf b. と宣言する
「a ならば a」の証明項	a => imp_intro a a (x => x)	a => x => x
Dedukti が行うこと	項の型を検査する	書き換えたうえで、項の型を検査する
証明項の大きさ	推論規則の適用が項に残るため、大きくなる	書き換えが肩代わりするため、小さくなる

（画像内の x ⇒ x は、本文中の x => x と同じものです。Dedukti の実際の構文は => です）

「論理体系の違い」と「型理論の違い」

個々の定理証明支援系は、それぞれ立脚する論理体系や型理論が異なります。

論理体系の違い と、型理論の違い を切り分けて詳しく見ていきます。

Dedukti の .dk ファイルに記述する識別子の宣言と書き換え規則は、
論理体系の違いによっても、型理論の違いによっても変わります。

変わるのは、以下の部分 です。

• 宣言する識別子の名前と型
• 書き換え規則の左辺と右辺

例えば、論理体系が 命題論理 の場合は、imp を宣言しますが、一階述語論理 であれば、forall が加わります。

また、型理論が CIC の場合は、「宇宙の階層」を宣言しますが、Martin-Löf 型理論 であれば、恒等型 Id を宣言することになります。

変わらないのは、記述できるものの種類です。

どの論理体系であっても、（また、）どの型理論であっても、.dk ファイルに書き込めるものは 識別子の宣言 と 書き換え規則 の 2 種類だけ です。

Dedukti のソースコードを書き換える必要もありません。

*取り扱う定理証明支援系が準拠する論理体系や型理論が変わったとき は、
その定理証明支援系を受け持つ翻訳器の側で対応 します。

翻訳器の設計者が、新しい論理体系や型理論を識別子の宣言と書き換え規則として記述 し、
符号化ファイルとして翻訳器に同梱 します。

Dedukti は、何も変えないまま、翻訳器が出力した .dk ファイルの読み込みと
型検査を行うだけです。

論理体系によって変わるもの、変わらないもの

論理体系の違い によって変わるものは 2つです。

1つ目 は、命題を作る記号 です。

• 命題論理 の場合は、含意 imp、連言 and、選言 or を宣言します。
• 一階述語論理 であれば、これに 全称量化子 forall と存在量化子 exists が加わります。
• HOL Light の高階論理 ならば、量化子が関数や述語にも及ぶため、量化子の宣言の型が変わります。

以上が、１つ目（論理体系の違いによって変わるもの）です。

2つ目 は、推論規則 です。

古典論理 なら、二重否定除去 ── 「A でないことはない」から「A である」を導く規則 ── を宣言します。

直観主義論理 では、二重否定除去を宣言しません。宣言する記号が 1 つ減るだけで、体系が変わります。

論理体系 が変わっても、変わらないもの は 3つあります。

1つ目 は、記述の手段が、記号の宣言 と 書き換え規則 の 2種類だけであること です。

2つ目は、証明が 項 として書かれることです。
3つ目は、Dedukti が行う処理が 型検査だけであること です。

論理体系	.dk ファイルに記述する内容	Dedukti 本体
命題論理	prop・Prf・imp の宣言と、含意の導入規則と除去規則	変わらない
一階述語論理	命題論理の宣言に加えて、全称量化子と存在量化子の規則	変わらない
直観主義論理	古典論理の宣言から、二重否定除去を外したもの	変わらない
HOL Light の高階論理	型と項の宣言と、関数や述語にも及ぶ量化子の規則	変わらない

型理論によって変わるもの、変わらないもの

型理論 によって変わるものは 2つ です。

1つ目 は、型を作る規則 です。
Lean 4 と Rocq が立脚する CIC であれば、 「宇宙の階層」 と 帰納型 を 作る規則 を 宣言 します。

Agda が立脚する Martin-Löf 型理論 であれば、依存和・依存積 と、恒等型（identity type）Id を 宣言 することになります。

2つ目 は、定義的等しさ（definitional equality） です。
CIC では、帰納型の再帰子が計算を行います 。
「再帰子を zero に適用した結果は、基底の場合の値に等しい」といった等しさです。この等しさを、書き換え規則として記述 します。

Martin-Löf 型理論 では、恒等型（identity type）の除去規則 J が計算を行います} 。この計算も 書き換え規則として記述 します。

型理論 が変わっても変わらないものは、論理体系の場合と同じ3つ です。

• 記述の手段が2種類だけであること。
• 証明が項として書かれること。
• Dedukti が行う処理が型検査だけであること

以上３点です。

画像プロンプト 06（論理体系と型理論が変わっても、変わらないもの）

型理論	立脚する定理証明支援系	.dk ファイルに記述する内容	Dedukti への符号化
CIC（Calculus of Inductive Constructions）	Rocq、Matita	宇宙の階層、帰納型、再帰子の計算規則	CoqInE として公開されている
CIC の変種	Lean 4	CIC の内容に加えて、Lean 4 固有の宇宙と定義的等しさの規則	lean2dk として公開されている
Martin-Löf 型理論	Agda	依存和・依存積、恒等型（identity type）Id、除去規則 J の計算規則	Agda2Dedukti として公開されている
量的型理論（Quantitative Type Theory）	Idris 2	変数の使用量の注釈を含む型の規則	筆者が調べた公開資料の範囲では確認できませんでした
ホモトピー型理論（区間型を持つ依存型理論）	Arend	区間型と、道の型の規則	筆者が調べた公開資料の範囲では確認できませんでした

2種類の違いをまとめると

論理体系の違いも、型理論の違いも、どちらも、dk ファイルの中身の違いとして現れます。

どちらの違いも、記号(識別子)の宣言と書き換え規則という2つの記述がどう変わるのか、という点に帰着します。

Dedukti は、読み込んだ .dk ファイルが何を宣言しているかを問わず、項の型を検査します。

共通言語とは、具体的に何か

以上をまとめます。

ここでいう 共通言語 とは、「λΠ計算 modulo rewriting」のこと です。

この言語で記述できるものは2種類しかありません。

• 記号（識別子）の宣言
• 書き換え規則

の２つです。

皆様と一緒に眺めてきたコードに綴られていたものは、記号（識別子）の宣言 か 書き換え規則 の どちらか でした。

取り扱う定理証明支援系が立脚する論理体系の相違点 は、Dedukti の中ではなく、.dk ファイルの中身の違いとして現れます。

• Lean 4 の型理論を記述した .dk ファイル、
• HOL Light の高階論理を記述した .dk ファイル
• というように、取り扱う定理証明支援系の数だけ .dk ファイルが並びます。

Dedukti が行うのは、読み込んだ宣言と書き換え規則のもとで、項の型を検査することだけです。

このように、複数の論理体系の推論規則を記述するための言語 を、Logical Framework と呼びます。

「λΠ計算 modulo rewriting」 は、Logical Framework のひとつ です。

Logical Framework という考え方は、1987 年に Edinburgh LF として提案されました。

提案したのは、英国スコットランドのエディンバラ大学に在籍していた Robert Harper、Furio Honsell、Gordon Plotkin の 3 名です。

同年7月、米国ニューヨーク州イサカで開かれた国際会議 LICS（Symposium on Logic in Computer Science）で報告され、1993 年に学術誌 Journal of the ACM に掲載されました。

言語実装の歴史をたどると、Edinburgh LF の代表的な実装は Twelf です。

Frank Pfenning と Carsten Schürmann が 1999 年の国際会議 CADE で報告しました。

Twelf は、プログラミング言語や論理体系の仕様を記述 し、その体系についての性質を証明する用途 で使われてきました。

Dedukti は、Edinburgh LF の言語であるλΠ計算 に、書き換え規則を足したもの です。

言語の系譜としては Edinburgh LF に連なりますが、目的は違います。

詳しくは、連載 3 回目 で扱います。

出典

• R. Harper, F. Honsell, G. Plotkin, "A framework for defining logics", Journal of the ACM 40(1), 1993, pp. 143-184. https://dl.acm.org/doi/10.1145/138027.138060
• F. Pfenning, C. Schürmann, "System Description: Twelf — A Meta-Logical Framework for Deductive Systems", CADE 1999. https://www.cs.cmu.edu/~fp/papers/cade99.pdf

Logical Framework という考え方そのもの ── どこから来て、Dedukti 以外に何があるのか ── は、連載 3 回目で扱います。

---

対話篇 ── Dedukti は、論理体系と型理論のどちらを受け付けるのか

連載第２回目となるこの記事は、論理を記述する共通の言語と、小さな証明検査器という考えを、実機で確かめます。

確かめることは次の 2つ です。

1つ目 は、古典論理や直観主義論理といった論理体系を、記号（識別子）の宣言と書き換え規則の組として、Dedukti のファイル（拡張子 .dk）に記述できることです。

2つ目 は、その論理体系にしたがって組み立てた証明項を、Dedukti の証明検査器が型検査によって受理し、誤ったものを拒否することです。

筆者の手元の環境で以下の実機検証を行いました。

まず最初に、Lambdapi で証明を記述し、Dedukti のファイル形式に変換します。

次に、変換したファイルを、Dedukti の証明検査器が独立に型検査しました。
その結果、Deduktiは、正しい（証明は成立する）と判定しました。

ところで、Deduktiにもできないことがあります。

どの定理証明支援系の証明も、Deduktiに翻訳できるわけではないのです。

ここには、２つの制約が横たわっています。

1つ目 は、定理証明支援系ごとに専用の翻訳器が要ることです。

翻訳器が無ければ、その定理証明支援系の証明を Dedukti のファイルに変換する手段がありません。

たとえば Dedukti は Idris 2 の証明を扱うことができません。

Idris 2 から Dedukti への翻訳器は、少なくとも本記事筆者が調べた公開資料の範囲では、見つかりませんでした。

翻訳器が公開されているのは、Lean・Rocq・Agda・Isabelle・HOL Light・PVS などです。

2つ目 は、翻訳器がある定理証明支援系でも、その言語機能すべてを扱えるとは限らないこと です。

翻訳器が対応していない機能を使った証明は、Dedukti のファイルに変換できません。

また、産業界での利用実績は、筆者が調べた公開資料の範囲では確認できませんでした。

本稿から皆様にお伝えしたいメッセージは、以下になります。

「定理証明器が受け入れた」の信頼は、どこに置くべきか ── その置き場所を小さくする研究が、Dedukti という実物として存在する。

ここで、読者の皆様が抱かれるかもしれない疑問点を、対話篇の形式で取り上げてみたいと思います。

タロウくん：
先生、初回記事の一覧表を見て気になったことがあります。

Dedukti が「異なる定理証明支援系の証明を共通言語に翻訳できる」と言うとき、翻訳元は、複数の論理体系なのですか？ 複数の型理論ですか？ それとも、両方ですか？

一覧表は、以下の表のことです。

定理証明支援系	土台の論理体系・型理論
Lean 4	Calculus of Inductive Constructions（CIC）の変種
Rocq（旧 Coq）	CIC
Matita	CIC
Agda	Martin-Löf 型理論の系統
Idris 2	量的型理論（Quantitative Type Theory）
Arend	ホモトピー型理論（区間型を持つ依存型理論）
Isabelle/HOL	高階論理（HOL）
HOL Light	高階論理（HOL）
PVS	高階論理＋述語による部分型
ACL2	一階論理（型なしの Lisp 上）
Metamath	置換規則のみ（論理は利用者が定義）

（連載初回の記事に掲載した表です。本記事だけを読む方のために再掲します）

専任講師：
両方です。
Dedukti が読み込む .dk ファイルには、論理体系も型理論も、同じ言語で書き表せます。順に説明します。

📌 厳密性を担保した説明をすると……「同じ言語で書き表せる」とは何か

論理体系と型理論が、数学的に同じものになる、という意味ではありません。

論理体系 には、命題があり、推論規則があり、証明があります。
その一方で、型理論 には、型があり、項があり、型付けがあり、宇宙や帰納型があります。

この2つの内容は、別のもの です。

Dedukti が用意するのは、両方を同じ言語の上に書き写す仕組み です。

対象となる論理や型理論を、Dedukti の項・型・宣言・書き換え規則として符号化 します。

そのうえで、それぞれの体系の証明を、Dedukti の型検査で検査できる形にします。

したがって、ここでいう共通化は、論理を1つに統一することではありません。
異なる論理と型理論を、共通の言語の上で書き表せるようにすること です。

まず、言葉を確かめる必要があります。

上の表の右の列には、2種類のものが混ざっています。

1 つは 論理体系 です。
高階論理や一階述語論理のように、「命題があり、推論の規則があり、規則に従って証明を進める」という形をしたものです。

表では、Isabelle/HOL や HOL Light の土台がこれです。

もう 1 つは 型理論 です。
CIC や Martin-Löf 型理論のように、 「型があり、項があり、型検査で正しさを確かめる」という形をしたもの です。

表では、Lean 4 や Rocq や Agda の土台がこれです。

（画像の右側で、木は型と項の組み立てを表しています。「型検査」は木の一部ではなく、組み立てた全体に対して行う操作です）

タロウくん：
形が違うように見えます。
Dedukti は、どちらを受け付けるのですか？

専任講師：
どちらも受け付けます。
コードを見て確認しましょう。

論理体系から Dedukti への翻訳器 は、すでに公開されています。

• HOL Light の高階論理を翻訳する hol2dk。
• 一階述語論理の自動証明器 Zenon Modulo の出力。
• B メソッドや TLA+ の集合論。Isabelle/HOL からの翻訳器。

型理論から Dedukti への翻訳器 も、すでに公開されています。

• Rocqの CIC を翻訳する CoqInE。
• Agda の Martin-Löf 型理論を翻訳する Agda2Dedukti。
• Lean 4 を翻訳する lean2dk。
• PVS の型理論を翻訳する Personoj。

翻訳器だけではありません。

Dedukti を作るに至った研究そのものにも、論理体系の研究と、型理論の研究の 2 つがあります。

型理論 の側からは、2007 年の Cousineau と Dowek の論文が出ています。
型理論の一族（Pure Type System）をすべて λΠ計算 modulo rewriting に埋め込めることを示した論文です。

論理体系 の側からは、Dowek が以前から研究していた deduction modulo があります。
一階論理・高階論理・集合論を扱ってきました。

2つの系譜が、Dedukti で合流しています。

タロウくん：
なぜ、形の違うものを、1 つの言語で受け付けられるのですか？

専任講師：
Dedukti が読み込む .dk ファイルには、論理体系も型理論も、同じ言語で記述できるからです。

「同じ言語」とは、λΠ計算 modulo rewritingのことです。
記述できるものは 2 種類しかありません。識別子の宣言と、書き換え規則です。

論理体系を記述するときも、型理論を記述するときも、使う道具はこの 2 種類だけです。

命題論理の含意を記述するときは、prop・Prf・imp という識別子を宣言し、[a, b] Prf (imp a b) --> Prf a -> Prf b. という書き換え規則を書きます。

Lean 4 の型理論を記述するときは、Sort・Pi・El という識別子を宣言し、宇宙の階層や帰納型の計算規則を書き換え規則として書きます。

宣言する識別子の名前も、書き換え規則の中身も変わります。

しかし、書ける種類は 2 つのままです。

Deduktiは何も変わりません。

読み込んだ .dk ファイルが命題論理を宣言していようと、Lean 4 の型理論を宣言していようと、Dedukti が行うのは、宣言された識別子の型を照合し、書き換え規則を適用しながら、項の型を検査することだけです。

なお、この 2 種類 ── 識別子の宣言の集まりと、書き換え規則の集まりの組 ── には、Dedukti での呼び名があります。理論（theory） と呼ばれています。

命題論理を記述した .dk ファイルは命題論理の理論、
Lean 4 の型理論を記述した .dk ファイルは Lean 4 の理論、

というように呼びます。

なぜ理論と呼ぶのか は、本記事の第 3 章で扱います。

また、複数の論理体系や型理論を、このようにひとつの言語で記述できるようにする仕組みそのもの を、Logical Framework と呼びます。

Logical Framework については、連載3回目の記事で扱います。

論理の 「命題」 は、Dedukti では 型として 書きます。
論理の 「証明」 は、その型を持つ項として 書きます。

命題は型であり、証明は項である ── この 対応 （カリー=ハワード対応）があるので、論理の証明も、型理論の項も、どちらも Dedukti の項として同じ土俵に乗せることができるんです。

タロウくん：
では、論理体系と型理論で、翻訳の手間は同じですか。

専任講師：
同じではありません。

論理体系 を埋め込むときは、命題を表す型 と、証明を表す型 を 1 つずつ用意して、推論の規則を書き換え規則として並べれば足ります。
いわば、一段浅い符号化 です。

型理論 を埋め込むときは、型・項・宇宙の階層・帰納型といった、型理論の部品そのもの を Dedukti の項として写す必要があります。
符号化は深くなり、難所が増えます。

次回以降の記事で述べる難所 ── 宇宙多相（universe polymorphism）や 依存パターンマッチ（dependent pattern matching） ── は、主に 型理論 の側の話です。

タロウくん：
最後にもう1つだけ、教えてください。
Logical Framework という名前は「論理の枠組み」ですよね？

型理論も扱えるのに、なぜ「論理」なのですか？

専任講師：
名前の由来が、論理の側にあるからです。

元祖の Edinburgh LF （1987 年）は、名のとおり「論理を定義するための枠組み」として作られました。

Dedukti は、その LF に書き換え規則を加えたもの です。

加えた動機は、計算を持つ型理論を効率よく埋め込むため でした。

つまり Dedukti は、論理向けに作られた枠組みを、型理論も扱えるように拡張したもの です。

名前は元祖から受け継ぎ、扱える範囲は広がった、と理解してください。

タロウくん：
整理します。

• 翻訳元は論理体系でも型理論でもよい。
• Dedukti の上では、どちらも「宣言と書き換え規則の組」という同じ形になる。
• ただし、型理論のほうが符号化は深い。
• 名前の「論理」は元祖からの受け継ぎ。

専任講師：
そのとおりです。

---

第 2 章 ── Dedukti という処理系そのもの

Dedukti は、フランスの国立研究機関 Inria の Deducteamというチーム で開発されてきた Logical Framework です。

中心人物の 1人が Gilles Dowek です。

Dedukti という名前は、エスペラント語で 「推論する」 を意味する動詞に由来します。

Dedukti の土台の計算体系は、λΠ-calculus modulo rewriting と呼ばれます。本記事の第1章で述べた 依存型 と 書き換え規則 を、名前の由来から 3 つの部品に分けて読み直します。

• λ ── 関数を作り、適用する。ラムダ計算です。
• Π ── 依存型。「$n$ を受け取って、長さ $n$ のベクトルを返す」のように、型 が 値 に 依存 できます。

ここまでは、Edinburgh LFと同じ です。
なお、Edinburgh LF については連載3回目の記事で取り上げる予定です。

• modulo rewriting ── 書き換え規則。利用者が「左辺を右辺に置き換えてよい」という規則を宣言でき、型検査器はその規則で計算しながら型を比べます。
  これは、LF にはなかった部品 です。

📌 厳密性を担保した説明をすると……どんな書き換え規則でも足してよいのか

どんな書き換え規則でも足してよいわけではありません。

型検査 を実際に行うには、書き換え が 計算として扱える性質 を持っている必要があります。

重要な性質が 2 つあります。

• 停止性（termination） ── 書き換えを続けても、いつか止まること。止まらない規則を入れると、型検査器 も止まりません。
   
• 合流性（confluence） ── どの順番で書き換えても、結果が食い違わないこと。順番で答えが変わると、型 が等しいかどうかが決まりません。

この記事に登場する足し算や含意の例は、仕組みを見るための小さな規則です。

実際に大きな理論を Dedukti に埋め込む研究では、その理論の書き換え規則が停止性（termination）と合流性（confluence）を持つことを示すこと 自体が、大きな仕事 になります。

λΠ計算に書き換え規則を加える 、という考え方は、Dedukti の出発点 にあたります。

この考え方が提案された原論文は、 2007 年の Cousineau と Dowek の論文です。

D. Cousineau, G. Dowek, "Embedding Pure Type Systems in the lambda-Pi-calculus modulo", TLCA 2007（Typed Lambda Calculi and Applications, 8th International Conference, Paris, France, June 26-28, 2007）, Lecture Notes in Computer Science, vol. 4583, Springer, pp. 102-117. > https://doi.org/10.1007/978-3-540-73228-0_9 > arXiv 版：https://arxiv.org/abs/2310.12540

なお、「書き換え規則」について、原論文では、「計算規則（computation rules）」 と表現されています。

書き換え規則を繰り返し適用することが計算にあたる ため、文献によっては 計算規則 と呼ばれるのです。

原論文から、要旨の一文を引用してみます。

It can be extended, in a very simple way, by adding computation rules.

（筆者訳）それ（λΠ 計算）は、計算規則を加えることで、ごく単純なやり方で拡張できる。

出典：D. Cousineau, G. Dowek, "Embedding Pure Type Systems in the lambda-Pi-calculus modulo", TLCA 2007. https://arxiv.org/abs/2310.12540

λΠ計算に計算規則（つまり、書き換え規則）を加えると、λΠ計算 modulo になります。

modulo は「〜のもとで」という意味で、ここでは「書き換え規則のもとで」を指します。

原論文が示したのは、この拡張によって、Pure Type System をすべて埋め込めるということ でした。論文要旨から引用します。

We show in this paper that this simple extension is surprisingly expressive and, in particular, that all functional Pure Type Systems, such as the system F, or the Calculus of Constructions, can be embedded in it.

（筆者訳）本論文では、この単純な拡張が驚くほど表現力に富むこと、とりわけ、System F や Calculus of Constructions といった、関数的な Pure Type System はすべて、その中に埋め込めることを示す。

出典：D. Cousineau, G. Dowek, "Embedding Pure Type Systems in the lambda-Pi-calculus modulo", TLCA 2007. https://arxiv.org/abs/2310.12540

**ここまでが、原論文の要旨に書かれていることです。**論文の題名も「Embedding Pure Type Systems in the lambda-Pi-calculus modulo」であり、Pure Type System の埋め込みが、この論文の主題です。

Pure Type System とは、 依存型を持つ型理論をまとめて扱うための枠組み です。

型理論ごとに違うのは、どんな sort（種）を持つか、sort どうしがどう関係するか、といった点 です。

sort とは、型そのものを分類する名前 です。

Pure Type System は、その違いを設定の差として表します。

設定を変えれば、System F という型理論にも、Rocq が立脚する Calculus of Constructions にもなります。

1つの枠組みで、多数の型理論を言い表せるのです。

つまり原論文は、個々の型理論を 1 つずつ埋め込んでみせたのではありません。
Pure Type System という枠組みごと埋め込めること を示しました。

（左右で図形の数が揃っていませんが、いずれも同じ型理論の集まりを表しています）

Calculus of Constructions は、Rocq や Lean 4 が立脚する CIC の土台にあたる型理論です。この結果があるので、Rocq や Lean 4 の証明を Dedukti で検査する道が開けています。

補足の出典

• H. Barendregt, "Lambda Calculi with Types", Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993.
• G. Dowek et al., "Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory", arXiv:2311.07185. https://arxiv.org/abs/2311.07185

なお、この計算体系の名前には、文献によって表記のゆれがあります。次節で整理します。

タロウくん：
先生、少し混乱してきました。

Dedukti の土台は Edinburgh LF だと聞きました。いま出てきたのは Pure Type System です。この 3 つは、どういう関係なのですか。

専任講師：
役割が違います。順に整理します。

Edinburgh LF は、Dedukti の土台です。

1987 年に提案された枠組みで、その言語が λΠ計算です。Dedukti の言語 λΠ計算 modulo rewriting は、この λΠ計算に書き換え規則を足したものです。名前に λΠ が入っているのは、そのためです。

Pure Type System は、土台ではありません。

埋め込まれる側です。Lean 4 や Rocq が立脚する型理論をまとめて扱うための枠組みで、Dedukti の中に記述される対象にあたります。

タロウくん：
土台と、記述される対象、ということですか。

専任講師：
そのとおりです。初回記事の言い方に当てはめると、こうなります。

Edinburgh LF の系譜にあるのが、符号化ファイルを書くための言語です。Pure Type System は、その言語で記述される中身のほうです。

タロウくん：
では、2007 年の論文は、何を示したのですか。

専任講師：
その 2 つがつながることを示しました。

Edinburgh LF の言語 λΠ計算に書き換え規則を足すと、Pure Type System という枠組みごと、その中に記述できる。これが 2007 年の結果 です。

タロウくん：
書き換え規則を足す前 は、記述できなかったのですか。

専任講師：
記述はできます。
ただし、証明項が大きくなります。

Edinburgh LF には書き換え規則がありません。

そのため、型理論が計算として処理していた部分を、証明の中に明示的な手順として書き並べる必要が出ます。

書き換え規則を足すと、その部分を Dedukti の型検査器の計算が肩代わりしてくれるようになります。 本記事の「仕組み 2」で見たとおりです。

タロウくん：
3 つの関係が見えてきました。

専任講師：
表にまとめます。

	何にあたるか	Dedukti との関係
Edinburgh LF	論理体系を記述するための枠組み。言語は λΠ計算	Dedukti の土台。ここに書き換え規則を足したものが λΠ計算 modulo rewriting
Pure Type System	型理論をまとめて扱うための枠組み	Dedukti の中に記述される対象
λΠ計算 modulo rewriting	Dedukti が読み込む .dk ファイルの言語	Edinburgh LF の言語に書き換え規則を足したもの

用語の注意 ── 3 つの表記が併存している

この計算体系の名前には、文献によって 3 つの表記があります。
違いは、modulo の後ろに何が付くかです。

• λΠ-calculus modulo

modulo の後ろに何も付きません。2007 年の原論文の表記です。

• λΠ-calculus modulo theory

modulo の後ろに theory が付きます。
Dowek の後年の論文、および Dedukti のシステム記述論文の題名で使われています。

ここでいう theory （理論）とは、識別子の宣言の集まりと、書き換え規則の集まりの組のこと です。

1 つの論理体系や型理論が、1 つの理論にあたります 。
本記事の第 3 章で扱います。

Lean 4 の理論 を読み込めば Lean 4 の証明を検査でき、
HOL Light の理論 を読み込めば HOL Light の証明を検査することができます。

Dedukti が .dk ファイルを読み込むたびに、理論は差し替えられます 。
この表記は、その点を強調しています。

• λΠ-calculus modulo rewriting

modulo の後ろに rewriting が付きます。
Assaf らの論文の表記であり、実装側の自称でもあります。
書き換えという機構を強調 した表記です。

Dedukti の証明検査器がどの表記を使っているかを確かめました。
筆者の環境でビルドした Dedukti の証明検査器のヘルプには、次のように表示されます。

dkcheck - An implementation of the lambdaPi calculus modulo rewriting

（筆者訳）dkcheck ── 書き換え規則付き λΠ 計算の実装

出典：Dedukti v2.7 の dk --help の出力（筆者の環境）。GitHub リポジトリの説明文も同じ表記。https://github.com/Deducteam/Dedukti

Dedukti の証明検査器が名乗っていたのは、modulo rewriting でした。

本記事では、Dedukti の証明検査器が使っている表記に合わせて、modulo rewriting に統一します。

実機検証 1 ── 自然数と足し算

ここから、筆者の環境で実際に動かします。
環境の詳細は記事末尾にまとめます。

最初のファイルは、自然数と足し算です。

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).

def two  : Nat := s (s z).
def four : Nat := s (s (s (s z))).

#ASSERT (plus two two) == four.
#EVAL (plus two two).

--> が書き換え規則です。

plus z n は n に、plus (s m) n は s (plus m n) に置き換えてよい、と宣言しています。

最後の 2 行は、plus two two が four に簡約されることの表明と、実際の評価です。

検査結果です。

s (s (s (s z)))
[SUCCESS] nat.dk was successfully checked.

実機検証 2 ── 論理の埋め込み、「modulo」の実物

第 3 章の LF 版を、書き換え規則で書き直します。

prop : Type.
def Prf : prop -> Type.
imp : prop -> prop -> prop.

(; 書き換え規則: 「a ならば b の証明」は「a の証明から b の証明への関数」;)
[a, b] Prf (imp a b) --> Prf a -> Prf b.

(; 恒等関数が「a ならば a」の証明として型検査を通る ;)
def identity : a : prop -> Prf (imp a a) := a : prop => x : Prf a => x.

(; 三段論法 (a→b)→(b→c)→(a→c) も関数合成として通る ;)
def syllogism : a : prop -> b : prop -> c : prop ->
                Prf (imp a b) -> Prf (imp b c) -> Prf (imp a c)
  := a : prop => b : prop => c : prop =>
     f : (Prf a -> Prf b) => g : (Prf b -> Prf c) =>
     x : Prf a => g (f x).

本記事の「仕組み 1 と 仕組み 2 の対比」の表で示した差が、実物として出ています。

imp_intro と imp_elim が消え、「a ならば a」の証明が恒等関数 x => x そのものになりました。三段論法の証明は、関数合成 g (f x) そのものです。

これが「modulo」です。
推論を計算で肩代わりさせています。

検査結果です。

[SUCCESS] logic.dk was successfully checked.

📌 厳密性を担保した説明をすると……「推論を計算で肩代わり」とは何か

「推論を計算で肩代わりさせています」という一文を登場させました。

「肩代わり」は、直感をつかむための言い方です。
実際に起きていることを、そのまま書きます。

書き換え規則は、項と項のあいだ、型と型のあいだに、計算による同値性を導入します。型検査器が 2 つの型を比べるとき、この同値性を使います。

上の例では、Prf (imp a b) を Prf a -> Prf b に書き換えられるようにしました。その結果、Prf (imp a a) を持つ項を検査するとき、型検査器はこの書き換えを使って、必要な関数型と一致することを確かめることができるようになります。

書き換え規則が、推論規則を自動で生み出すのではありません。
どの書き換えを許すかは、理論の一部として人間が明示します。

型検査器は、明示された同値性を使うだけです。

実機検証 3 ── 誤った証明の拒否

正しい証明が型検査を通るケースだけを見せるのは、片手落ちです。
誤った証明が、Deduktiによって拒否されるかどうかも、確かめてます。

prop : Type.
def Prf : prop -> Type.
imp : prop -> prop -> prop.
[a, b] Prf (imp a b) --> Prf a -> Prf b.

(; 誤り: 「a ならば b」を恒等関数で証明しようとする。a と b は別の命題 ;)
def bad : a : prop -> b : prop -> Prf (imp a b)
  := a : prop => b : prop => x : Prf a => x.
                             ^^^^^^^^^^^^^^^
                             ここが恒等関数

（注意点）

上記のコード中の ^^^^ の行は、説明のために付けた印です。Dedukti の構文ではありません。このファイルをそのまま dk check にかけると、構文エラーになります。

実行できるファイルとして載せるなら、印の行を外し、本文で位置を示す形になります。

さて。
検査結果です。

[ERROR CODE:101] [wrong.dk] [line:7 column:88]
Error while typing 'x[0]' in context:
[ a : wrong.prop, b : wrong.prop, x : wrong.Prf a ].
---- Expected: wrong.Prf b
---- Inferred: wrong.Prf a

期待された型は Prf bですが、推論された型は Prf aでした。
Dedukti の証明検査器は、この食い違いを見つけて、この証明を拒否しました。

---

第 3 章 ── 「一つの論理」ではなく「論理を記述する」

第 2 章で扱った 3 つの .dk ファイル ── 自然数と足し算を定義した nat.dk、命題論理の含意を定義した logic.dk、誤った証明を書いた wrong.dk ── は、いずれも数行だけの短いコード例でした。

しかし、これらのコードが行っていたことは、実務レベルのコードと実質的には同じことです。

また、いずれも、識別子の宣言 と 書き換え規則 を並べて、1つの論理体系を定義 していました。

Dedukti では、こうして定義したものを 理論（theory）と呼びます。

ところで、なぜ、宣言の集まりと書き換え規則の集まりの組 が、 理論 と呼ばれるのでしょうか？

その理由は、数理論理学で理論という言葉が意味するもの と、対応しているから です。

数理論理学 では、理論 を 「言語と公理の組」 として定めます。

言語 とは、その理論で用いることのできる 記号の一覧 です。

群論ならば、単位元 e、積の演算、逆元を表す記号です。

公理 とは、その理論で 無条件に成り立つとする命題の一覧 です。

再び群論の例を挙げるとすると、結合律、単位元の法則、逆元の法則、が該当しますです。

Dedukti の .dk ファイルを構成する 2 つの部品である、識別子の宣言の集まり
と、書き換え規則の集まり は、それぞれ、言語 と 公理 に対応します。

宣言の集まり が、言語 にあたります。
prop や imp といった記号を、型とともに並べたものだからです。

書き換え規則の集まり が、公理 にあたります。
「この式とこの式は等しい」という 無条件の取り決めを並べたものだから です。

対応がずれる点も1つあります。

数理論理学の公理は「成り立つ命題」ですが、
Dedukti の書き換え規則は、「置き換えてよい向き」を持ちます。

左辺から右辺への一方向です。
向きがあるおかげで、型検査器が規則を計算として実行できるのです。

---

ここまでのまとめ

本記事では、次の 4 点を述べました。

（1 点目）
Dedukti の言語は λΠ計算 modulo rewriting です。依存型と書き換え規則の 2 つを持ちます。

（2 点目）
推論規則は、識別子の宣言として .dk ファイルに書き込むことができます。
命題論理の含意なら、prop・Prf・imp を宣言し、導入規則 imp_intro と除去規則 imp_elim を宣言します。

（3 点目）
書き換え規則を足すと、imp_intro と imp_elim が消えます。
「a ならば a」の証明は恒等関数そのものになります。
推論を、型検査器の計算が肩代わりするからです。

（4 点目）
論理体系の違いも型理論の違いも、.dk ファイルの中身の違いとして現れます。Deduktiは何も変える必要はありません。

次回記事へ

連載第2回目となるこの記事では、Dedukti が用いる言語で、何が記述できるかを見ました。

• 識別子の宣言と書き換え規則という 2 種類だけで、論理体系も型理論も記述できる
• Dedukti 自身は、どの論理体系も内蔵していない

次回（連載第3回目）の記事では、論理体系を記述する側 と、記述されたものを検査する側 を 分ける という考え方が、どこから来たのかを扱います。

Dedukti の場合は、 「論理体系を記述する側」 が、特定の定理証明支援系（Rocq、Agda など）の証明項を .dk ファイルに翻訳する 翻訳器 で、 「記述されたものを検査する側」 は Dedukti でした。

この考え方は、Dedukti が発明したものではありません。

1987 年に提案された Edinburgh LF に始まります。

Edinburgh LF では、 「論理体系を記述する側」 は、一階述語論理や高階論理の推論規則をλΠ計算で記述したファイル です。
「記述されたものを検査する側」 は、そのファイルを読み込むプログラムである Twelf です。

Twelf は、読み込んだファイルに記述された推論規則にしたがって、証明を検査します。

広く使われている定理証明支援系である Isabelle も、同じ作りです。

Isabelle では、「論理体系を記述する側」 が Isabelle/Pure というメタ論理 です。

Pure の上に、対象論理（object logic）として HOL や ZF や FOL が定義されています。

「記述されたものを検査する側」 は、Isabelle の証明検査器 です。
この証明検査器は LCF 方式で作られた小さなプログラムで、対象論理が HOL であっても ZF であっても、行うことは変わりません。

	論理体系を記述する側	記述されたものを検査する側
Dedukti	翻訳器が同梱する符号化ファイル（.dk）。Rocq、Agda、Lean 4 などの論理体系や型理論を、識別子の宣言と書き換え規則として記述したもの	Dedukti の証明検査器。読み込んだ .dk ファイルの項を型検査する
Edinburgh LF	一階述語論理や高階論理の推論規則を、λΠ計算で記述したファイル	Twelf。読み込んだファイルの推論規則にしたがって、証明を検査する
Isabelle	Isabelle/Pure というメタ論理。その上に対象論理（object logic）として HOL・ZF・FOL が定義されている	Isabelle の証明検査器。LCF 方式で作られた小さなプログラム

これらをまとめて、Logical Framework と呼びます。
英語版 Wikipedia に項目があります。

Dedukti が何を受け継ぎ、何を足したのかを、次回の記事で述べます。

---

📌 用語のミニ解説

📌 本文に登場した処理系・翻訳器・考え方の、初心者向けミニ解説

Logical Framework（ロジカル・フレームワーク）

論理そのものを記述するための言語 です。
ふつうの定理証明支援系は、1つの論理 を実装します。

Logical Framework は、論理を定義の対象として 扱います。

1987 年の Edinburgh LF（Harper・Honsell・Plotkin）が源流で、本記事の Dedukti はこの系譜の現在形の 1 つ です。

λProlog（ラムダ・プロローグ）

論理プログラミング言語 Prolog の拡張で、高階の項と束縛を扱えます（Miller・Nadathur）。論理を記述する用途にも使われるため、論理プログラミング型の Logical Framework と位置づけられます。

Dedukti との違いは、計算機が何を実行するかです
── λProlog は導出の探索を実行し、Dedukti（dkcheck）は型検査だけをします。実装の 1 つ ELPI は、Rocq のタクティク開発にも使われています。

Matita（マティータ）

イタリアのボローニャ大学で開発された定理証明支援系です。

Rocq と同じ CIC（帰納構成計算）の系統ですが、小さく作られており、証明項が取り出しやすい構造をしています。

本記事に登場した「Dedukti 経由で複数の体系へ翻訳された算術ライブラリ」は、Matita で書かれたものです。

HOL Light（ホル・ライト）

高階論理（HOL）系の定理証明支援系です（John Harrison）。検査の核が数百行と極めて小さいことで知られます。

実解析・複素解析のライブラリ Multivariate を持ち、ケプラー予想の形式証明（Flyspeck 計画）にも使われました 。

本記事の「2 万定理超を Rocq へ翻訳」の翻訳元 です。

CoqInE（コック・イン・イー）

Rocq（旧 Coq）の証明を Dedukti へ翻訳する変換器です。Rocq のプラグインとして実装されており、標準ライブラリの一部を翻訳した実績があります。

Zenon Modulo（ゼノン・モジュロ）

一階論理の自動証明器 Zenon の拡張です。deduction modulo を組み込み、見つけた証明を Dedukti 形式で出力できます。探索は自動証明器、検査は Dedukti、という分業の実例です。

BWare（ビーウェア）

フランスの研究プロジェクトです（2012〜2016 頃）。B メソッド ── 鉄道など安全性が問われる分野で使われてきた形式手法 ── の証明義務を、自動証明器で証明し、Dedukti で独立に検査する流れを研究しました。

産業の題材に最も近づいた事例ですが、研究プロジェクトであって産業配備そのものではありません。

predicate subtyping と PVS（述語による部分型）

PVS は米国 SRI で開発された定理証明支援系で、航空宇宙分野の検証で広く使われてきました。その特徴が predicate subtyping ── 「0 でない実数」のように、述語で絞り込んだ部分型を作れる仕組みです。強力な半面、型検査が決定不能になります。この珍しい機能をどう符号化するかが、Dedukti 研究の題材になっています。

matching logic と K（マッチング論理）

K は、プログラミング言語の意味論を定義するための枠組みです。

C・Java・イーサリアムの EVM などの意味論が K で定義されてきました。

その論理的基盤が matching logic です。これも Dedukti への符号化の研究対象になっています。

de Bruijn 因子（de Bruijn factor）

序章の de Bruijn 基準（criterion）とは別の概念です。
形式化した数学の長さを、元の非形式の文章の長さで割った比を指します。
Wiedijk が名づけました。形式化すると文章が何倍に膨らむか、という量です。

基準は「証明を独立に検査できるか」、因子は「どれだけ膨らむか」で、名前だけが同じです。

出典：
F. Wiedijk, "The De Bruijn Factor", 2000. https://www.cs.ru.nl/~freek/factor/

---

実機検証について

本記事のコードは、すべて筆者の環境で実行しました。
検証できたことと、できなかったことを分けて記します。

検証環境

構成要素	版	入手経路
OS	Ubuntu 24.04	─
OCaml	4.14.1	apt
dune	3.14.0	apt
menhir	20231231	apt
Dedukti	v2.7（タグ）	GitHub Deducteam/Dedukti をソースビルド
Lambdapi	2.5.1（タグ）＋改変	GitHub Deducteam/lambdapi をソースビルド
bindlib	6.0.0	GitHub からソースビルド
pratter	3.0.1	GitHub からソースビルド
why3	1.6.0	apt

検証できたこと

• 検査 1〜3（第 2 章）は、すべて Dedukti v2.7 の dk check で期待どおりの結果を返した。
   
• dk --help の自称が「lambdaPi calculus modulo rewriting」であることを、実物で確認した。

検証できなかったこと・注意

• Dedukti と Lambdapi の開発版（master）は dune 3.18 以上を要求し、Ubuntu 24.04 の dune 3.14 ではビルドできなかった。安定タグを使った。
   
• Dedukti の README は「opam の版は古いので、リポジトリを clone してインストールすることを推奨する」と述べている。筆者の経験と一致する。
   
• CoqInE、hol2dk、isabelle_dedukti などの翻訳器は、筆者の環境では実行していない。補足節の翻訳器一覧は、一次資料の記述に基づく。

Lambdapi を用いた検査は、後の回に記します。

検証ファイル（nat.dk、logic.dk、wrong.dk、lf.dk）は、本記事に全文を掲載しました。

---

訂正一覧

公開後に訂正した箇所を、ここに追記していきます。現時点ではありません。

関連記事

本記事の接続先

• 論理はひとつではない ── 圏論論理学がつなぐ量子論理・トポス・圏論的量子力学 https://qiita.com/etale_cohomology/items/24858c3bd7c7d6833eaa
   
• if 文も SQL も、実は別々の「論理」だった ── 古典論理から量子論理まで、21 の論理体系を 5 人で議論【対話篇】 https://qiita.com/etale_cohomology/items/4fadbda1ebea7a63f68d
   
• 依存型を使わない Isabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか
  https://qiita.com/etale_cohomology/items/6987c76966a3513cd6e0
  Isabelle/Pure という枠組みの上に HOL・ZF・FOL を載せる構造、sledgehammer による自動化、Isar 記法、seL4 と AWS Nitro Isolation Engine の検証を扱っています。本記事の第 4 章と第 8 章の背景です。
• トポスと論理の関係 ── ひとつのトポス（数学の宇宙）を選ぶと、なぜ古典論理か直観主義論理が決まるのか ── そして、トポス以外の「器」たち https://qiita.com/etale_cohomology/items/5206679c2fd02aea9512
   
• λProlog とは何か ── AI が数学を証明する時代、定理証明系 Rocq の内側で働く知られざる言語
  https://qiita.com/etale_cohomology/items/98b416523f468dc64959
  Prolog を高階論理と単純型付きラムダ計算で拡張した言語、その実装 ELPI、Rocq の拡張言語 Coq-Elpi、高階抽象構文（HOAS）を扱っています。本記事の第 3 章で挙げる論理プログラミング型の枠組みの詳細です。

数珠つなぎ連載（型理論から立方体型理論へ）

（1本目）
https://qiita.com/etale_cohomology/items/365356fa41ed7b4d7829

（2本目）
https://qiita.com/etale_cohomology/items/e3eae170f14f134c8f13

（3 本目）
https://qiita.com/etale_cohomology/items/f2aa70cdc826e15979a4

（4 本目）
https://qiita.com/etale_cohomology/items/75aa5395b5f8c03e1bf2

📚 Arend 連載（全 8 本）

https://qiita.com/etale_cohomology/items/0abc51fe5e2a3eb02f08

https://qiita.com/etale_cohomology/items/8126e8eae37eefdf86f6

https://qiita.com/etale_cohomology/items/61193814df628ace0bf7

https://qiita.com/etale_cohomology/items/679faed081b6cd8be97c

https://qiita.com/etale_cohomology/items/865503fbcfc68b23d759

https://qiita.com/etale_cohomology/items/e80c18c3c35460f316b7

https://qiita.com/etale_cohomology/items/543ba6180aef46a21cbe

https://qiita.com/etale_cohomology/items/3b332aa9c22ebe838c5c

---

出典一覧

• R. Harper, F. Honsell, G. Plotkin, "A Framework for Defining Logics", Journal of the ACM 40(1), 1993.
• D. Cousineau, G. Dowek, "Embedding Pure Type Systems in the lambda-Pi-calculus modulo", TLCA 2007. https://arxiv.org/abs/2310.12540
• A. Assaf, "Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting", TLCA 2015. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.31
• G. Dowek, "Models and Termination of Proof Reduction in the lambda Pi-Calculus Modulo Theory", ICALP 2017. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.109
• T. Felicissimo, "Adequate and Computational Encodings in the Logical Framework Dedukti", FSCD 2022. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.25
• G. Dowek, F. Thiré, "Logipedia: a multi-system encyclopedia of formal proofs", 2023. https://arxiv.org/abs/2305.00064
• Deducteam/Dedukti（GitHub）. https://github.com/Deducteam/Dedukti
• Deducteam/lambdapi（GitHub）. https://github.com/Deducteam/lambdapi
• Deducteam/isabelle_dedukti（GitHub）. https://github.com/Deducteam/isabelle_dedukti
• Deducteam/Agda2Dedukti（GitHub）. https://github.com/Deducteam/Agda2Dedukti
• Deducteam/Dedukti Issue #224. https://github.com/Deducteam/Dedukti/issues/224
• EuroProofNet（公式サイト）. https://europroofnet.github.io/
• EuroProofNet, Tools. https://europroofnet.github.io/tools/
• EuroProofNet, Deliverables 1 and 13. https://europroofnet.github.io/deliverable1/
• EuroProofNet, Deliverable 5. https://europroofnet.github.io/deliverable5/
• EuroProofNet, LFPSI 2025（国際スクール）. https://europroofnet.github.io/LFPSI25/
• J. Cockx, "How to write a translator to Dedukti: The case of Agda"（講演資料）, 2022. https://europroofnet.github.io/_pages/WG1/Jun2022/thiago_and_jesper.pdf
• A. Ranta, "Symbolic Informalization: Fluent, Productive, Multilingual", arXiv:2606.16893, 2026 年 6 月 15 日投稿. https://arxiv.org/abs/2606.16893
• 同論文の日本語版（alphaXiv による訳題「記号的非形式化：流暢、生産的、多言語」。要約は自動生成）. https://www.alphaxiv.org/ja/abs/2606.16893
• F. Wiedijk, "The De Bruijn Factor", 2000. https://www.cs.ru.nl/~freek/factor/
• G. Klein et al., "seL4: Formal Verification of an OS Kernel", SOSP 2009. https://dl.acm.org/doi/10.1145/1629575.1629596
• G. Gonthier et al., "A Machine-Checked Proof of the Odd Order Theorem", ITP 2013, LNCS 7998. https://link.springer.com/chapter/10.1007/978-3-642-39634-2_14
• T. Hales et al., "A formal proof of the Kepler conjecture", Forum of Mathematics Pi, arXiv:1501.02155. https://arxiv.org/abs/1501.02155
• T. Hales, "The Formal Proof of the Kepler Conjecture: a critical retrospective", arXiv:2402.08032. https://arxiv.org/abs/2402.08032
• Inria, Deducteam 2024 Activity Report. https://radar.inria.fr/rapportsactivite/RA2024/deducteam/DEDUCTEAM-RA-2024.pdf