自作してふんわり眺める依存型【定理証明】
2025/06/28ぼく「Geminiさん、依存型を実装して詳しく理解したいのですが良い資料ありませんか?」
Gemini「A tutorial implementation of a dependently typed lambda calculusっていう論文がおすすめです」
というわけで
依存型について理解するために、A tutorial implementation of a dependently typed lambda calculusを読みました。
この記事は、理論編と実装編に分かれています。
理論編では、上記の論文で示されている構文、型付け規則、評価規則をざっくりと紹介しようと思います。できるだけ難しい用語は使わず、自分のための補足説明も入れていこうと思います。
実装編では、本論文のコードをTypeScriptへ写経します。
リポジトリ:https://github.com/sititou70/lambda-pi
そして、より実践的な例として、すべての自然数 について
が成り立つことの証明を構築します。
理論編
抽象構文
抽象構文とは、主に理論編の中で使用する構文です。プログラムや型をテキストで表して議論するために使用します。
を任意の項(プログラム)、 (ロー)を任意の型、 (カッパ)を任意のカインド(型の型)とします。
ここでさっそく驚きポイントなのですが、今回の体系ではこれら3つを構文上で区別しません。これにより型の中に項が書けるようになって、項に依存した型で依存型というわけです。前回の記事で、「依存型の中では型とプログラムのどっちを書いているのか混乱する」と言っていたやつですね。
前置きが長くなりましたが、今回の抽象構文は以下のようになります。
-
- (注釈された項)
- が 型であるという主張です。
- TypeScriptの型注釈に似ています。
- (型の型)
- 型の型を表します。
- 型(命題)を受け取る関数を型付けしたいときに使う感じです。これにより、「すべての命題について〜」というような命題が定義できます。詳しくは前回の記事の、カリーハワード同型対応の説明を参照ください。
- (依存関数型)
- 関数型(アロー型)の依存型バージョンです。
- 「 の変数 を受け取って、 型の項を返す関数の型」という意味です。
- 命題を表す際によく使います。例えば、 と書くと、「自然数 について、 ( を使った等式の型などが書ける)が成り立つ」という意味になります。
- (変数)
- (適用)
e(e')
の意味です。
- (ラムダ抽象)
- 関数のことです。 が引数で が関数本体です。
- 型が付く項です。
- 今回の構文では の型を明示しません。後述する型付け規則を見るとわかるのですが、注釈によって対応する の からわかるので不要みたいです。
- (自然数型)
- (自然数のゼロのコンストラクタ)
- (自然数の後者のコンストラクタ)
- の次の数を表します。
- (自然数の除去)
- 自然数に関する示したい命題( )について、Zeroのケース( )と、Succのケース( )で成り立つことが言えるなら、任意の自然数( )で命題が成り立つと言っていいよという意味です。
- :自然数を受け取って型(命題)を返す関数です。最終的に示したい命題です。
- : 型の項です。つまり、 がゼロで成り立つ証明です。
- :自然数 と、 型の項を受け取ると、 型の項を返す関数です。つまり、示したい命題がある自然数で成り立つことを仮定して、次の自然数でも成り立つことを示す証明です。
- :natElimを適用する自然数です。自然数であれば何でも良いです。
- 最終的に、この項には 型が付きます。 は自然数であれば何でも良かったので、すべての自然数に対して が成り立つ気持ちです。
- 高校の数学の授業でやった、数学的帰納法に似てますね。
- ElimはEliminatorの略だそうで、Rocq(旧Coq)のelimタクティックと語源が一緒っぽいです。このへんあまり詳しくないのですが、最終的に自然数 が消えるので、除去規則的な意味でEliminatorと言ってるんすかね?
- 自然数に関する示したい命題( )について、Zeroのケース( )と、Succのケース( )で成り立つことが言えるなら、任意の自然数( )で命題が成り立つと言っていいよという意味です。
- (Eq型)
- (Eqのコンストラクタ)
- の意味です。
- これはRocqでのEqの定義に似ています。
- (Eqの除去)
- ある型( )があって、その型の等式に関する示したい命題( )について、Reflのケースで命題が成り立って( )、ある左辺の値( )と右辺の値( )があって、それらが実際に等しい( )ならば命題が成り立つという意味です。
- :両辺の値の型です。今回の証明では主に です。
- :最終的に示したい命題で、左辺の値、右辺の値、左辺と右辺が等しいというEq型の値を受け取って、命題を返す関数です。
- : 型の値 を受け取ると、 型の値を返す関数です。これはReflコンストラクタに対応したケースですね。
- : 型の左辺の値です。
- : 型の右辺の値です。
- : 型の値です。 と が本当に等しいのか示してみろということです。
- 最終的に、この項には 型が付きます。等しいすべての と について、 が成り立つというわけです。
- RocqでのEqの帰納的な定義を思い出して、Eqに対する帰納法の原理と考えるとわかりやすいかもです。
- ある型( )があって、その型の等式に関する示したい命題( )について、Reflのケースで命題が成り立って( )、ある左辺の値( )と右辺の値( )があって、それらが実際に等しい( )ならば命題が成り立つという意味です。
- (注釈された項)
型付け規則
型付け規則は、さきほどの構文にどのような型が付くのかを定義します。
さっそく、 (注釈された項)の型付け規則であるT-Annを見てみましょう。
この分数のような記法は「線の上(仮定)のすべての式が成り立つならば、線の下(結論)の式が成り立つ」という意味です。
や は、型付け判別式で、「コンテキスト のもとで、 に 型が付く」という意味です。
はコンテキストで、変数と型のマッピングを保持しています。TypeScript風に書くとMap<variable, type>
みたいなやつです。今回の規則ではただあるだけという感じですが、他の規則ではコンテキスト内のマッピングを取得(Map.prototype.get()
)したり、コンテキストに新しいマッピングを追加(Map.prototype.set()
)したりもします。簡単のために詳しい定義は割愛します。
は型推論モードを、 は型検査モードを意味します。これは双方向型検査と呼ばれる仕組みのようで、今回のような強い型システムで型推論する手法の1つだそうです。正直むずかしいので、最初はこの上下の矢印を無視して読むくらいが良いかもしれません。詳しくはMizunashi Manaさんの「双方向型検査: 検査と構築の融合」が参考になります
は、 を評価すると最終的に になるという意味です。ここで驚きポイントその2なのですが、今回の計算体系では、型検査の際に評価(プログラムの実行)が発生する場合があります(!)
以上を踏まえて、もう一度T-Annを見てみましょう。
まず結論をみると上矢印があるので、注釈された項は推論モードで扱える(項だけから型がわかる)と言っています。実際、 の型が と明示されているのでそれはそうだよなという感じです。
推論の具体的なステップは、仮定部分を見るとわかります。まず仮定の最初の式では、 が 型であることを検査していますね。これにより、注釈の型の部分に項が書かれているような不正なケースを弾いています。
それがOKなら仮定の次の式によって、 を評価して、最終的な評価結果である を得ます。ここで私は最初「型を評価するってなに?」となったので、つまづきポイントだと思います。
今回の体系では項と型を区別していないので、型に対する評価規則も定義されます(後の評価規則の節で説明します)。なので、 も評価すると別の形になるかもしれません。具体的には、型が項に依存しているかもしれず(依存型)、型の中に評価すると形が変わる項があるかもしれません。なので、型付け規則全体を通して、型は評価したうえで検査に使用する方針に統一されているようです。これにより、「評価すると実質的に同じになる型」を同一視できるようになります。
実際、仮定の最後の式では、 が 型である(つまり注釈が正しい)ことを、評価後の型を使って検査していますよね。
残りの型付け規則(長いです)
以下のT-Star規則は、
無条件で(前提なしに) の型は であると言っています。「ほんとか?」という感じですが、ここは簡単のためにこうなっているそうなので、いったん受け入れましょう。
次はT-Pi規則です。
結論を見ると、依存関数型は型なので、その型は常に (型の型)であるとわかります。項だけから型がわかるので推論モードにできます。
という記法は、コンテキスト に変数 が 型であるというマッピングを追加するという意味です。
仮定を見ると、変数 に注釈されているのが型であること、それを評価してコンテキストに追加した上で、依存関数の本体もまた型であることを要求しています。依存関数型はラムダ抽象の型の気持ちなので、その本体も型じゃないとおかしいのは納得です。
次のT-Var規則では、
変数に対応する型をコンテキストから取得して終わりです。
次はT-App規則です。
仮定を見ますと、まず、演算子( )について何らかの依存関数型であることを要求しています。要するに、ラムダ抽象で引数を渡せるよね?と確認してる気持ちですね。
次に、被演算子( )について、演算子の引数の型と一致することを検査しています。渡す側の型と受け取る側の型が一致してないとダメなのはそう。
は、 に(自由に)現れる を に置き換える(代入する)という意味です。
適用の最終的な型は、演算子が返す型になります。ただし、依存関数型は引数を取るので、本体に現れる を、被演算子の型に置き換えて、さらに評価したものになります。
次のT-Chkは少し分かりづらいです。
これまでの規則の仮定とかで、 があって色々検査する場面がありました。そこで検査対象の項 が推論モードで扱える場合、推論を実行して実際に 型になれば、検査したことにしていいよ、と言っています。まぁそれはそう。
T-Lam規則は、
ラムダ抽象が依存関数型を持っていることを検査するには、引数とその型の束縛を作成したうえで、本体の型検査をすればいいということです。
今回の体系では、推論モードで扱えない項はラムダ抽象のみです。
ここからは自然数に関する規則です。T-Nat規則は、
無条件で が 型であると言っています。はい。
T-Zero規則は、
無条件で が 型だと言っています。#0は自然数
T-Succ規則は、
の中身 が 型なら、 もまた 型だよ、ってことです。簡単ですね。
T-NatElim規則でいきなり難しくなります。
自然数に対する帰納法の原理を頭の片隅に置きながら、おちついて1つずつ読んでいきます。
まず は、最終的に示したい自然数に関する命題です。命題なのでPropositionの頭文字pを使っています。ちなみに論文ではMotiveのmを使ってましたが、pの方が好きなのでここではそうしています。
仮定の最初の式は、 が自然数を受け取って命題(型)を返す関数であることを表しています。 は、束縛した変数を使用しない依存関数型 の略記です。
次と、その次の式は、 が「 をゼロに適用したときの証明」になっていることを検査しています。帰納法の基底ケースの証明が正しいか確認してる感じです。
さらに次と、その次の式は、 が「ある自然数 と、 で が成り立つという証拠があると仮定したとき、 でも が成り立つという証明」になっているかを検査しています。これは帰納法の帰納ケースの証明の検証に対応します。
仮定の最後の式で、natElimを適用する対象 が自然数であることを検査します。自然数の帰納法の気持ちなので、自然数にしか適用できません。
これだけの仮定が成り立つと、結論として 型をつけられます。 に必要な仮定は自然数であることだけなので、すべての自然数について が成り立つと言っているのと同じです。
最後に、Eq型に関する規則を見ていきます。この図は論文には無かったので、今回の説明のために作成しました。
まず、T-Eq規則は、
が型で、 と が 型を持つなら、 もまた型であるという主張です。めっちゃあたりまえですね。
T-Refl規則は、
が型で、 が 型を持つなら、 は 型であると言っています。これはReflがEqのコンストラクタなので当たり前です。
逆に、Eq型を付けられる規則がこれしかないので、「自分自身に対してのみ等式が成立する」という性質を表しているとわかります。(これをライプニッツ等値性と言うらしいです。等値性の定義には、他にも流派があるらしいです。
最後はT-EqElim規則です。
これは、Eqの帰納法の気持ちを表しています。
まず仮定を見ていきます。最初の式は、Eqの左辺と右辺の型である が、実際に型であることを確かめています。
次と、その次の式では、示したい命題 が、Eqに関する命題の型になっているかを確かめています。
さらに次と、その次の式では、Reflコンストラクタに対応するケースの証明 が、意図した型になっているかを検査しています。 型のすべての値について、自分自身と等しいというReflの仮定が得られるので、その仮定を使って を示さないといけません。コンストラクタが複数ある自然数と違って、証明のケースはこの1つだけで終わりです。
残りの式では、 、 、 について意図したとおりの型が付くことを確認して終わりです。
ここまでの仮定が成り立つと、最終的に 型が結論できます。 、 、 に必要な仮定を考えると、 型でお互いに等しいすべての と について がいえるとわかります。
これで型付け規則はおわりです。おつかれさまでした!
評価規則
今回の最終的な目標は定理の証明なので、型(命題)とプログラム(証明)が合っているかを型検査できれば良いです。なので型付け規則だけ考えれば良い、と思っていた時期が僕にもありました。
この体系では型検査の途中に評価もするので、評価規則もまじめに勉強しないとダメでした。
というわけで、評価規則を1つ見てみましょう。E-Ann規則は以下のようになっています。
注釈された項の後の部分が に評価されるなら、もとの注釈された後全体も に評価して良い、と言っています。
つまり、注釈された型情報を捨てて評価しているという感じです。TypeScriptっぽいですね。
現時点で記事がかなり長くなっている自覚があります。なので、のこりの規則は畳んでおきます。
残りの評価規則
E-Star規則では、
は に評価されると言っています。正直、 を評価したいなんて1度も思ったこと無いですが、今回の体系では項、型、カインドの区別が無いので、カインドに対する評価が実行される場合もあるため、こういう定義も必要みたいです。
E-Pi規則では、
注釈部分と本体部分を評価しています。型の中に項があるかもしれませんからね。
E-Var規則は、
変数は評価しても変わらないということです。
E-AppLam規則では、
まず、演算子を評価してラムダ抽象にします。次に、その本体の引数を被演算子で置き換えて、さらに評価しています。一般的な関数適用そのままですね。
一方でE-AppNeutral規則は、演算子がすぐにはラムダ抽象にならない場合に使う評価規則です。
ここで で表されているのはニュートラル項(Neutral Term)です。これは今回初めて触れた概念なので、正直理解がかなり怪しいのですが、現時点での認識で書いてみます。
この規則は、演算子が未定だが、適用を表現しておきたい場合に使われるという印象です。例えば、自然数に対する帰納法の原理の型を書きたい場合、 型の を引数で受け取ることになります。そして、 が成り立つべきだとか、 がどうだとかいう主張を型レベルで書くはずです。
ここで、帰納法の原理の型を検査したいとします。いま、 は帰納法の原理が実際に使用されるまで未定の変数で、ニュートラル項と考えられます。演算子が未定なので、 や といった項は、これ以上変形できません。
だからといって評価を失敗扱いにすると、帰納法の原理の型検査も失敗してしまいます。なので、 や もまたニュートラル項として捉え、適用の形を保ったまま、値の一種として考えます。これにより、「 が に適用されている状態」とか「 に が適用されている状態」を取り回せるようになります。
このように、項の一部が未定であるためにこれ以上簡約できないが、値の一部として扱っておきたいというのがニュートラル項の気持ちである……という理解です。かなりふんわりした説明ですが今回はそういう記事なのでゆるしてください。 Normal forms and neutral termsも参考になりました。
次はE-Lam規則です。
これは、ラムダ抽象の本体だけを評価しても良いという規則です。普段とは違う評価戦略で新鮮ですね。
ここからは、自然数に関する規則です。E-Nat規則は、
は評価しても変わらないと言っています。
同様に、E-Zero規則によれば、
は評価しても です。
E-Succ規則は、
の中身を評価しても良いということです。実際、数学の命題を書いていると、中身に足し算や掛け算などのプログラムが現れるのはよくあります。
次のE-NatElimZero規則は、
が具体的に である場合の評価をします。その場合、 型である (をさらに評価したもの)に評価してやれば良いですね。
同様に、E-NatElimSucc規則は、
が で表される場合の評価です。この場合も、 に必要な値を渡して評価してやれば良いだけです。
の1つ前の自然数である に関する命題の証明は、 によって再帰的に求めているのが興味深いです。引数のサイズが減っているので許されている感じがありますね。
E-NatElimNeutralは、
E-AppNeutralと同じような理由のやつです。natElimを適用する自然数 が未定の場合でも、適用しているという事実を扱いたい場合があるので必要な気持ちです。
いよいよラストスパートで、Eqに関する規則です。これも論文に図がないので、私が雰囲気で書きました。
まず、E-Eqは、
その中身を評価しても良いという規則です。
E-Reflも同じで、
中身を評価できます。さきほどの自然数のときと同じで、数学をやっていると や の中身を評価して同一視したい場合がけっこうあるので重要です。
E-EqElimReflは、
eqElimの適用対象である が で構築されている場合の評価で、 や と等しい値 が得られるので、それを に渡せば評価結果が得られます。
最後に、E-EqElimNeutralは、
eqElimの適用対象である がニュートラル項である場合の規則です。eqElimをニュートラル項に適用している状態を表現しておきたいので必要な気持ちです。
実装編
理論編の内容をTypeScriptに実装しました。論文ではHaskellによる実装が示されているので、それを写経した感じです。
リポジトリ:https://github.com/sititou70/lambda-pi
まず、配列を使って項を表すことにしました。パーサーとかを考えたくなかったからです。
抽象構文をもとに、以下のような具象構文を定義します。
export type TermInferable =
| ["Ann", TermCheckable, TermCheckable]
| ["Star"]
| ["Pi", TermCheckable, TermCheckable]
| ["Bound", number]
| ["Free", Name]
| [TermInferable, ":@:", TermCheckable]
| ["Nat"]
| ["NatElim", TermCheckable, TermCheckable, TermCheckable, TermCheckable]
| ["Zero"]
| ["Succ", TermCheckable]
| ["Eq", TermCheckable, TermCheckable, TermCheckable]
| ["Refl", TermCheckable, TermCheckable]
| [
"EqElim",
TermCheckable,
TermCheckable,
TermCheckable,
TermCheckable,
TermCheckable,
TermCheckable
];
export type TermCheckable = ["Inf", TermInferable] | ["Lam", TermCheckable];
項には、推論可能な項(推論モードで扱える項)と検査可能な項(検査モードで扱える項)があり、構文レベルで区別されています。
次に、これらの項を検査するための関数を用意します。
export const typeInferable =
(index: number) =>
(context: Context) =>
(term: TermInferable): Type => {
// ...
};
export const typeCheckable =
(index: number) =>
(context: Context) =>
(term: TermCheckable) =>
(type: Type): void => {
// ...
};
推論モードと検査モードの2種類の関数があります。推論モードの関数では、項を受け取って推論結果の型を返しています。一方で検査モードの関数では、項と型を受け取って、項にその型が付くか検査して、最終的には何も返しません。検査に成功するとそのまま終了して、失敗すると例外を投げます。index
とかContext
とかType
の説明は省略します。詳しい解説は論文を参照ください。
次に、評価のための関数も用意します。
export const evalInferable =
(term: TermInferable) =>
(env: Env): Value => {
// ...
};
export const evalCheckable =
(term: TermCheckable) =>
(env: Env): Value => {
// ...
};
推論可能な項のための関数と、検査可能な項のための関数を2種類作りました。ただ、評価には推論モードや検査モードという考えはないです。単純に型検査器と実装を対応させて見やすくするためにこうしました。
どちらの関数も、項を受け取って評価結果の値を返しています。例によって、Env
やValue
の説明は省略します。
関数内部の具体的な実装は、基本的には理論編の規則をそのまま対応させればOKです。
例えば、T-Annを実装したいとします。これは推論モードの規則なので、typeInferable
関数の中に次のように書けば良いです。
if (term[0] === "Ann") {
const [_, exp, type] = term;
typeCheckable(index)(context)(type)(["VStar"]);
const evaluetedType = evalCheckable(type)([]);
typeCheckable(index)(context)(exp)(evaluetedType);
return evaluetedType;
}
注釈の項と型について、型がカインド型であることを検査し、それを評価したうえで、項にその型が付くことを検査しています。
T-Annと見比べると、同じことをやっているとわかります。
ただ、Haskellの型検査の実装と、論文中の型付け規則が違っている箇所がいくつかありました。例えば、Haskellの方では評価された項を使っているが、規則の方には評価するとは特に書かれていないということがありました。この場合は、基本的にはHaskellの方を優先していますが、まぁケースバイケースの雰囲気でなんとかしました。
かんたんな証明を書いてみよう
実装ができたのでさっそく証明を書いていきましょう。
まず、足し算x + y
を以下のように定義します。
const plus: TermCheckable = [
"Lam", // arg: x
[
"Inf",
[
"NatElim",
// NatElim_prop
// 自然数xについて、自然数yを受け取るとx + yを返す関数があるという命題です。
[
"Lam", // arg: x
[
"Inf",
[
"Pi",
// 自然数yを受け取ると
["Inf", ["Nat"]],
// 自然数x + yを返す
["Inf", ["Nat"]],
],
],
],
// NatElim_propZero
// xがゼロのときは、yが与えられたらそれをそのまま返す関数(恒等関数)が足し算の実装になります。
// ["Inf", ["Bound", 0]]は直前のLamで受け取った引数を表します。0はド・ブラウン・インデックスです。つまり、一番内側で束縛された変数を参照しています。
[
"Lam", // arg: y
["Inf", ["Bound", 0]], // y
],
// NatElim_propSucc
// xがSuccの形で書ける、つまりxの前者x'がある場合です。
// x'と、prop x'(つまり、足し算をx'に適用した項)を受け取って、足し算の実装を返せば良いです。
[
"Lam", // arg: x'
[
"Lam", // arg: prop x'
[
// 足し算の実装。yを受け取ってx + yを返します。
// まず、「x' +」の意味のprop x'があるので、それをyに適用して「x' + y」を作ります。
// あとはそれをSuccすれば、「Succ (x' + y)」、つまり「Succ(x') + y」ということで結局「x + y」が計算できたことになります。
"Lam", // arg: y
[
"Inf",
[
"Succ",
[
"Inf",
[
["Bound", 1], // prop x'
":@:",
["Inf", ["Bound", 0]], // y
],
],
],
],
],
],
],
// NatElim_nat
// NatElimをxに適用します
["Inf", ["Bound", 0]], // x
],
],
];
const plusType: TermCheckable = [
"Inf",
[
"Pi",
// 自然数xを受け取って
["Inf", ["Nat"]],
[
"Inf",
[
"Pi",
// 自然数yを受け取ったら
["Inf", ["Nat"]],
// x + yの自然数を返します
["Inf", ["Nat"]],
],
],
],
];
export const plusAnn: TermInferable = ["Ann", plus, plusType];
手始めに「すべての自然数nについて、 」の命題と証明を構築してみましょう。
まず、命題を型で表現します。
// 「自然数nを受け取って、0 + n = n型を返す関数」の型
const plusZeroLType: TermCheckable = [
"Inf",
[
"Pi",
// 自然数nを受け取って
["Inf", ["Nat"]],
// 以下の型を返します
[
"Inf",
[
"Eq",
// 自然数に関する等式があって、
["Inf", ["Nat"]],
// 左辺は0 + n
[
"Inf",
[
[
// さっき作った足し算を使います
plusAnn,
":@:",
["Inf", ["Zero"]], // 0
],
":@:",
["Inf", ["Bound", 0]], // n
],
],
// 右辺はn
["Inf", ["Bound", 0]], // n
],
],
],
];
この型が付く関数があれば、目的の命題が示されたことになります。そのような関数は、実は以下のように簡単に書けます。
// nを受け取って、Refl Nat nを返します。
// Rocqがわかる人向けだと、intro n. reflexivity.しただけです。
const plusZeroLProof: TermCheckable = [
"Lam", // arg: n
["Refl", ["Inf", ["Nat"]], ["Inf", ["Bound", 0]]],
];
というのも、命題の型の左辺が評価されて簡単になるからです。
- まず
plusAnn
を0に適用していますが、plusAnn
の定義より恒等関数に評価されます。 - 次に恒等関数を
n
に適用しています。当然、評価結果はn
です。
で、右辺もn
なので、その値はRefl Nat n
で良いということです。
このことを型検査で確かめてみます。
// 証明を命題で注釈します
export const plusZeroLAnn: TermInferable = [
"Ann",
plusZeroLProof,
plusZeroLType,
];
test("check plusZeroL", () => {
// 証明に命題の型が付くか検査します
typeInferable(0)([])(plusZeroLAnn);
});
検査を実行します。
✓ check plusZeroL 1ms
Test Files 1 passed (1)
無事に成功しました。これでOKです!
足し算プログラムに要求される性質の1つを、依存型を使って検証したということになります。
ちなみに、命題と証明を合わせたplusZeroLAnn
は、JSONで表すと509文字でした。
もう少しむずかしい問題
ができたら、 もやりたくなるのが人間です。
しかし、その証明は難しいです。先程は、足し算を0に適用したので恒等関数に評価されていました。しかし今回は に適用するので、そこから先に評価が進みません(ニュートラル項になります)。
コイツを示すには、自然数に対する帰納法が必要です。
// nを受け取って、n + 0 = n型の値を返します
const plusZeroRProof: TermCheckable = [
"Lam", // arg: n
[
"Inf",
// 自然数の帰納法をnに対して使います
[
"NatElim",
// NatElim_prop
// 示したい命題です。nを受け取って、n + 0 = n型を返します
[
"Lam", // arg: n
// n + 0 = n型の項(省略)
],
// NatElim_propZero
// 基底ケース:nがゼロの場合、命題が成り立つことを示す必要があります。今回は0 = 0を示すだけなのでかんたんです
["Refl", ["Inf", ["Nat"]], ["Inf", ["Zero"]]],
// NatElim_propSucc
// 帰納ケース:nの前者n'があって、prop n'を仮定してprop n、つまりprop (Succ n')型の値を返す必要があります。
[
"Lam", // arg: n'
[
"Lam", // arg: n' + 0 = n'
// ここでprop (Succ n')型の値を返すのがゴールです
// 1. Refl Nat (Succ n')を使って以下が示せます。
// (Succ n') = (Succ n')
// 2. 帰納法の仮定「n' + 0 = n'」を使って、左辺のn'をn' + 0に書き換えます
// (Succ (n' + 0)) = (Succ n')
// 足し算の定義を思い出すと、これは以下の式と同じです。
// (Succ (n')) + 0 = (Succ n')
// 4. これはprop (Succ n')なのでOKです
],
],
// NatElim_nat
["Inf", ["Bound", 0]], // 帰納法をnに対して使います
],
],
];
ちなみに、帰納法の中で等式の書き換えが必要ですが、そのためにはeqIndRという別の定理が必要です。eqIndRの詳細は割愛しますが、示すにはEqの帰納法を使います。
が になっただけで、帰納法が2つも必要になるのはおもしろいですね。
今回の命題と証明をJSONで表すと、2,366文字でした。
まぁ実際には、足し算の定義が重複して入っているのでもっと短く書けるとは思うのですが、それでも感覚としては先程よりむずかしい問題だったと分かりますね。
最終問題
この記事の冒頭で言っていた、すべての自然数 について
である証明をやりたいと思います。
流れは以下のようになります。
- 足し算を定義する
- 掛け算を定義する
- から までの総和を計算する関数を定義する
- ならば の証明を書く
- 等号の書き換えに使う定理の証明を書く
- の証明を書く(さっきやったやつです)
- の証明を書く
- の証明を書く
- 「 」を使う
- 「 ならば 」を使う
- 「 」を使う
- の証明を書く
- の証明を書く
- 「 」を使う
- 「 ならば 」を使う
- 「 」を使う
- の証明を書く
- の証明を書く
- の証明を書く
- 「 」を使う
- 「 ならば 」を使う
- 「 」を使う
- 「 」を使う
- の証明を書く
- 「 ならば 」を使う
- 「 」を使う
- 「 」を使う
やばいです。
工夫したこと
ユーティリティの作成
上記の証明項をすべて手書きしようとするのはマズいです。けが人が出ます。
証明には、長い式がたくさん出現すると予想されますので、そのためのユーティリティを作成しました。例えば、 という項を書きたいとします。普通に書くと
const expr = [
"Inf",
[
"Eq",
["Inf", ["Nat"]],
[
"Inf",
[
[mulAnn, ":@:", ["Inf", ["Bound", 0]]],
":@:",
[
"Inf",
[
[plusAnn, ":@:", ["Inf", ["Bound", 1]]],
":@:",
["Inf", ["Bound", 2]],
],
],
],
],
[
"Inf",
[
[
plusAnn,
":@:",
[
"Inf",
[
[mulAnn, ":@:", ["Inf", ["Bound", 0]]],
":@:",
["Inf", ["Bound", 1]],
],
],
],
":@:",
[
"Inf",
[
[mulAnn, ":@:", ["Inf", ["Bound", 0]]],
":@:",
["Inf", ["Bound", 2]],
],
],
],
],
],
];
めっちゃ長いです。でもmakeEqExpr
というユーティリティを使うと
const expr = makeEqExpr(
[["x", "*", ["y", "+", "z"]], "=", [["x", "*", "y"], "+", ["x", "*", "z"]]],
new Map([
["x", ["Inf", ["Bound", 0]]],
["y", ["Inf", ["Bound", 1]]],
["z", ["Inf", ["Bound", 2]]],
])
);
と書けます。
さらに、makeEqExpr
に渡す配列すら書くのが面倒だったので、テキスト形式で書いてGeminiくんに変換してもらってました。
Rocqでの証明
今回自作した型検査器には、エラーの内容を親切に表示する機能などを付けていません。検査に失敗した場合、どこで失敗したのかがわからないので、証明項を書き間違えたのか、証明そのものの考え方がおかしいのか判断が付きません。
そこで、まず同等の証明を先にRocqで完成させ、そのコードを今回の環境に移植するという方法をとりました。
え?本末転倒じゃないかって?私もちょっと思いました。
ですが今回の目的は、依存型への理解を深めることと、検査器がちゃんと動くかの検証です。
Rocqで書いたのと同等の証明が自作の型検査器でどのように扱われるかは興味深いですし、実際、この証明の最中に検査器のバグをいくつか見つけられました。
証明完成!
✓ check main 135ms
Test Files 1 passed (1)
check main
が、最終問題の証明を検査するテストケースです。検査は135msで完了しました。
ちなみに、命題と証明をJSON文字列にしてみると、576,085文字になります。
ターミナルエミュレータの設定を変更し、文字サイズを1pxにすることで、
すべての項を表示して遊べます。
たのしいですね。
怒られたので設定を戻しました。
発展的な話題
論文の最後の方に、今回の体系は健全ではないことが書かれています。
あまり詳しいことはわからないのですが、どうやらT-Star規則がマズいようで、
が 自身に属するので、自己言及のようなことができて、おかしくなってしまうみたいです。
なので、厳密には型検査をパスしても証明が正しいとは言えないです。しかし、今回の目的は依存型を学ぶことなので、考えることを減らして理解に集中できるのはむしろ良かったと思います。
この問題を解決する方法として、グロタンディーク宇宙という考え方があるそうです。意味はまったくわかりませんが、声に出したくなるかっこよさがありますね。
余談:ぼくとGeminiくん
今回の記事を書くにあたって、型付け規則や評価規則をTeX形式に起こすために、論文のPDFからコピーしてきたテキストをGeminiくんに変換してもらっていました。
以下は、T-Pi規則の仮定部分を変換する際にGeminiくんが出してきたDiffですが、
$$
\dfrac
{
- 0 ` ρ ::↓ ∗
- ρ ⇓ τ
- 0, x :: τ ` ρ′ ::↓ ∗
+ \begin{aligned}
+ & \Gamma \vdash \rho ::_\downarrow * \\
+ & \rho \Downarrow \tau \\
+ & \Gamma, x :: \tau \vdash \rho' ::_\downarrow *
+ \end{aligned}
}
{
+ \Gamma \vdash (\forall x :: \rho. \rho') ::_\uparrow *
}
\quad\text{(T-Pi)}
$$
論文のテキストを与えていない結論部分まで、なぜか完璧に生成しています。
ぼく「結論部分は変換元のテキストを示していないはずですが、あなたは完璧に推論しました。依存関数の型付け規則を知識に持っているということですか……?」
Gemini「はい、ご推察の通り、依存関数の型付け規則に関する知識を持っています。……(中略)……提供されたドキュメント全体の文脈、定義、および他の規則のパターンを総合的に分析することで、欠落している情報を補完することが可能です。」
本記事の内容を読んだそうですが、この時点では抽象構文と、T-Ann、T-Starまでしか書いていなかったので、そこまでの知識から推論したらしいです。すごい。
また、ただ記法を変換するだけではなく
Gemini「T-NatElimの前提は、論文の意図を汲んで整形し、明らかにタイポと思われるm kをm lに修正」
とも言ってきました。
そうなんです。論文には実際にタイポがあって、図と本文を比べるとわかります。
ただ、今回Geminiくんに渡したのは図の情報だけ、つまりタイポがある間違った情報だけでした。当然、Tex記法の間違った式が出てくるはずで、それを手動で修正する想定でした。ところが、規則の意味を解釈したのか「明らかにタイポ」として勝手に正しく修正してしまいました。
さらに、Eqの型付け規則と評価規則に関しては論文にも図がないので、分数表示の雛形だけ用意していて、後で自作する予定でした。しかし、Geminiくんはそこも生成してきました。
結果的には、型付け規則に関してはほぼ正解で、評価規則については全て間違いのようでした。評価の方に関しては、生成の時点で本文中に情報が無かったので、まぁ想定通りです。型付けの方の生成に成功しているのがむしろすごいです。
というわけで、sititou70いらないかもですね。いつの日か、AIが人生を自動化してくれるといいなと思います。
まとめ
依存型がある計算体系について理論を勉強し、それをTypeScriptで実装しました。
- 項、型、カインドの区別がないとどうなるか
- 型を評価するとはどういうことか
- なぜ型検査中に評価が必要なのか
などについて、理解が深まったと思います。
最終的には、足し算、掛け算、総和を実装し、 から までの総和に関する命題と証明を構築しました。
この命題は、3年前にはじめて定理証明系というものに触れたときの記事である「Idrisでふんわり眺める依存型」でも取り上げました。同じ命題を自作の検査器でも扱えてうれしいです。
最後に、A tutorial implementation of a dependently typed lambda calculusのおかげで今回の記事が書けました。著者の皆さん、ありがとうございました。
単純型付きラムダ計算を拡張する方法で段階的に説明されており、また実装に困ったらHaskellによるコードも参照できるのでおすすめです。
依存型初心者なので、おかしなところがあれば教えていただけると嬉しいです。
それでは!