0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@etale_cohomology(Etale Cohomology)

Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す

0
Last updated at Posted at 2026-09-12

thumbnail_picture.jpg

この連載について

本記事は、computational type theory を扱う 前編・後編 2本構成 の 前編 です。

回 扱うこと
前編（本記事） computational type theory とは何か。計算の振る舞い方のどこを境に、同じ型と別の型を分けるのか。研究の歴史と動機の変化。computational type theory を採用した言語と採用しない言語の違い
後編 実際に動かせるプログラムの一覧。論理体系と型理論の多対多の対応。Cartesian と De Morgan という 2 つの系統。De Morgan cubical type theory を採用した言語に computational type theory の実装がない理由

本記事の続編となる 後編記事 のタイトルは、『なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜』 です。

本記事について

本連載（全2回）シリーズが取り上げる computational type theory は、日本語で読める解説ウェブ記事や和文資料が、筆者が調べた限りでは見当たりませんでした。（2026年9月11日現在）

また、computational type theory という専門用語について、定まった和訳も、まだ存在しないように見受けられました。そこで、本連載シリーズでは、英語のまま computational type theory と記載いたします。

本連載シリーズは、筆者が過去にQiitaに公開した記事 「ホモトピー型理論（HoTT）の区間 I に、どの数学的代数構造を入れるか — De Morgan と Cartesian、2 つの立方体型理論から実装言語の地図まで」の連載 4 本目で触れた computational type theory を、独立した主題として扱います。

なお、上記を含めて、筆者が過去に公開した記事をお読みでなくと、本連載記事を単独でお読みいただけるように工夫いたしました。

なお、専門用語 は、初出時点で丁寧に解説するように心がけました。
また、記事末尾に用語の ミニ解説 も置かせていただきました。

Executive Summary ── 前編・後編を通して何を示すのか

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

プログラミング言語の型 は、言語があらかじめ用意した、変えられない枠ではありません。

  • ある 2 つの値を同じ型に入れるか、別の型に分けるか
  • ある 2 つの値を等しいと見なすか、別のものと見なすか

この線引きを、言語設計者が決めたものです。

この線をどこに引くかによって、そのプログラミング言語が得るものと、失うものが変わります。

本シリーズでは、この得失の関係を 「取引」 と呼びます。

（この主張を支える３本の柱）

（1本目の柱）computational type theory では、型と計算の順序が、ふつうの言語と逆である。

Haskell・Rust・Go・TypeScript のように、読者の皆様の多くがお使いの言語では、先に型があります。Int という型は整数の集まりで、その集まりの要素として値が入ります。先に型を決め、あとから値を入れる、という順序です。

computational type theory では、順序が逆です。先に計算の振る舞いがあります。ある計算を実行したときの振る舞いが、ある条件を満たすかどうか。その条件を満たす計算の集まりが、あとから型を成します。先に計算があり、あとから型が決まる、という順序です。

📌 コラム：CTTは「型が後から生まれる」という意味なのか

「型が後から決まる」という説明は入門者には非常に有効です。

ただし、形式的には「プログラムを書いた後でコンパイラが型を推測して付ける」という意味ではありません。

Nuprl系 では型は、項の集合として外から先に与えるのではなく、計算的意味論にもとづいて、どの項がその型に属し、どの項どうしを等しいとみなすかという判断として説明されます。

したがって、「計算が先、型が後」は、プログラミング言語の 型推論の手順 を表す言葉ではなく、型の意味付けの仕方 を表す言葉です。

（２本目の柱）2 つの値を等しいと見なす範囲は、定理証明支援系ごとに違う。

たとえば、この記事で扱う Lean 4・Rocq・Nuprl では、2 + 2 と 4 は 計算した結果の値を比べることで、同じものとして扱えます。

しかし n + 0 と n のように、より一般的な式では事情が変わります。

Lean 4 や Rocq では、こうした等しさを、命題として証明しなければならない 場面があります。

Nuprl では、この 2 つは等しいと見なされます。

等しいと見なす範囲 を 狭く すれば、2 つの値が等しいかどうかを型検査器が自動で判定できます。

その代わり、人間が証明を書かなければならない場面が増えます。

Rocq や Lean 4 は、こちらを選んでいます。

等しいと見なす範囲 を 広く すれば、数学者が等しいと考えるものを、そのまま等しいと記述できます。

その代わり、2 つの値が等しいかどうかを型検査器が自動で判定できなくなり、人間がタクティクを書いて証明を組み立てる必要があります。

Nuprl や RedPRL は、こちらを選んでいます。

本シリーズでは、範囲を狭くすることを「線を手前に引く」、広くすることを「線を奥に引く」と呼びます。

この2つの立場には、それぞれ名前が付けられています。

内包的（intensional） とは、2 つのものが等しいかどうかを、その定義の仕方 ── 中身の形 ── で判定する立場 です。

たとえば λx. x + 0 と λx. x は、定義の形が異なります。
そのため、内包的には、別のもの とみなされます。

Rocq や Lean 4 は、内包的 です。

外延的（extensional） とは、2 つのものが等しいかどうかを、その振る舞い ── 外から見た結果 ── で判定する立場 です。

λx. x + 0 と λx. x は、どの入力に対しても同じ値を返します。
ですから、外延的には、等しい です。

Nuprl や RedPRL は、外延的 です。

  • 線を手前に引く のが 内包的
  • 線を奥に引く のが 外延的 です。

pic_1.jpg

（3本目の柱）等しさの範囲をどこで決めるか、という問いは、定理証明支援系だけの話ではない。

  • Haskell の 型クラス
  • Go の インタフェース
  • TypeScript の 構造的部分型

これらは、2つの型を同じ型として扱うかどうかを、型の名前で決めるか、型の中身の形で決めるか、を選ぶ選択です。

読者の皆様が日々お使いのプログラミング言語の設計にも、似た選択が現れています。

ただし、computational type theory が問うのは「2つの値は等しいか」であるのに対して、構造的部分型 が問うのは「2つの型のあいだで値を代入できるか」です。

問いの立て方は似ていますが、問いの中身は異なります。
本稿は、この区別を取り上げます。

型 を、「言語が用意した、変えられない決まりごと」 として受け止められていた読者の方がおられたとしたら、型とは、何を等しいと見なすかの取り決めであり、その取り決めは言語の設計者が選んだものだ という見方に、本記事をお読みいただくなかで触れていただけましたら幸いです。

📌 厳密性を担保した説明をすると……型は「等しさ」だけでできているわけではない

本文では、この記事の中心問題をつかみやすくするために、「型とは、何を等しいと見なすかの取り決めである」 と強調しました。

ただし、型 が担う役割は 等しさ だけではありません。
たとえば自然数型なら、どの項を自然数として認めるか、自然数を受け取る関数をどう使えるか、といった条件 も 型 の意味に含まれます。

computational type theory で特徴的なのは、型 の意味を説明するとき、要素として認める条件と、要素どうしを等しいと見なす条件を、計算の振る舞いにもとづけて結び付ける点 です。

本稿は、上記のうち、「等しさの線をどこに引くか」 に焦点を絞っています。

本連載シリーズを読む価値。　は、3点 あります。

（ひとつ目）
computational type theory を日本語で扱った資料は、筆者が調べた範囲では見当たりませんでした。本連載シリーズが、日本語で読める最初（あるいは、数少ない）の解説記事になります。

（２つ目）
本稿の記述内容を、手元でコードやソースコードファイルを動かすことで、確かることができます。

筆者は、RedPRL・redtt・cooltt・cubicaltt という4つの言語のプログラムを手元の環境でビルドし、動かしました。

同じ定理を RedPRL と Lean 4 で証明し、証明項を比べた結果 を掲載します。

（３つ目）
本稿に続く 後編記事では、ホモトピー型理論（HoTT） の 区間$I$ を計算できる De Morgan cubical type theory を採用した言語に、computational type theory を実装した言語がない のは、なぜなのか？ という問いに向き合います。

本稿（前編記事）で扱う範囲。

本稿（前編記事）は、以下の 5つの問い に答えます。

  • （1） 計算の振る舞い方の違いを型の違いとして宣言するとき、振る舞い方のどこを境に、同じ型と別の型を分けるのか？
     
  • （2） computational type theory の研究はいつ始まったのか。当初の動機と目的は何か？
     
  • （3） 研究が始まった当初の問題意識と、2026年9月の現在とで、研究の動機と目的は変化したか？
     
  • （4） computational type theory を採用した言語と、採用しない言語とで、何が違うのか？
     
  • （5） 何を等しいと見なすかを設計者が決める、という話は、ふつうのプログラミング言語にも出てくるのか？

前編記事 ではここまでを書きます。

  • 実際に動かせるプログラムの一覧
     
  • 論理体系と型理論の対応
     
  • Cartesian と De Morgan の 2 つの系統

続く 後編記事 では、（すでに述べたとおり、） ホモトピー型理論（HoTT）と Computational type theory との交差領域 に光を当てて、De Morgan cubical type theory を採用した言語に computational type theory の実装がない理由 を取り上げます。

本記事の流れ

対話篇 ── 計算の振る舞い方のどこを境に、同じ型と別の型を分けるのか

タロウくん：
先生、computational type theory という言葉を、たまたま目にする機会がありました。

先生の過去記事の、型理論から立方体型理論への連載 4 本目に、こう書かれていました。

ある計算 M が「Int 型を持つ」とは、M を実行すると必ず、有限のステップで具体的な整数値（0 や -3 や 42 のような）に停止することである。

型は、計算の振る舞い方の一種の「合格基準」として定義されます。「合格基準を満たす計算」が集まって、事後的に型を成す。

集まりが先で計算が後、ではなく、計算が先で型が後、という順序です。

この立場を、専門用語では、「computational（計算的）な意味付け」と呼びます。NuPRL とその後継の証明支援系が採用してきた立場です。

出典：
https://qiita.com/etale_cohomology/items/75aa5395b5f8c03e1bf2

これは、特定の振る舞い方をするデータを、特定の型として定義し、宣言するようなイメージだと受け取りました。

振る舞い方の違いを型の違いとして宣言するとき、振る舞い方のどこを境にして、同じ型と別の型を分けるのですか。

専任講師：
その受け取り方は、半分あたっています。

君の質問に対する答えは、本記事の執筆者が公開済みの記事に、すでに書かれています。少し長いですが、引用します。

「計算による意味付け」とは、どういう立場か

この NuPRL の伝統が持つ独特の姿勢を、分かりやすく説明します。

型理論には、大きく分けて 2 つの意味付けの流儀があります。

流儀 A：型を「集まり」として先に決めておく立場

Haskell を書くとき、多くの方は、おそらく次のように考えておられるのではないでしょうか。

Int という型は、... -2, -1, 0, 1, 2, ... という整数の集まりである。
Bool という型は、True と False の 2 つからなる集まりである。
Int -> Bool は、Int の要素を受け取って Bool を返す関数の集まりである。

先に「型 = 何かの集まり」があり、あとから「その中の要素として、この関数はこう動く」と関数を書く。これが自然な考え方に思えます。ほとんどの型理論の教科書もこの立場を取ります。この立場を、専門用語では、「denotational（外延的、集合的）な意味付け」と呼びます。

流儀 B：型を「計算の振る舞い方」として決める立場

これに対し、NuPRL の伝統は逆の順序を取ります。

先に「計算がどう動くか」を決めておき、あとから「こういう動き方をするものを、この型に住むと呼ぶ」と型を規定するのです。

たとえば、Int という型を先に集合として定めるのではなく、こう考えます。

ある計算 M が「Int 型を持つ」とは、M を実行すると必ず、有限のステップで具体的な整数値（0 や -3 や 42 のような）に停止することである。

型は、計算の振る舞い方の一種の「合格基準」として定義されます。「合格基準を満たす計算」が集まって、事後的に型を成す。

集まりが先で計算が後、ではなく、計算が先で型が後、という順序です。

この立場を、専門用語では、「computational（計算的）な意味付け」と呼びます。NuPRL とその後継の証明支援系が採用してきた立場です。

出典：数珠つなぎ連載 4 本目
https://qiita.com/etale_cohomology/items/75aa5395b5f8c03e1bf2

この引用のうち、「集まりが先で計算が後、ではなく、計算が先で型が後」という一文 が、君の受け取り方を正す部分です。

君は「特定の振る舞い方をするデータを、特定の型として定義する」と受け取りました。
データが先にあって、データに型を付ける、という順序 です。

これは、Haskell や Rust のように、読者の皆様の多くがお使いの言語での順序です。
まず先に Int という型があり、その次に、その型の要素として値が入ります。

引用文が述べているのは、その逆 です。

まず先に、計算の振る舞い があります。
その次に、以下を 判断 します。

  • ある計算を実行したときの振る舞い が、ある条件を満たすかどうか 。
  • その条件を満たす計算の集まり が、あとから 型 を成します。

先に計算があり、あとから型が決まる、という順序 です。
データに型を付けるのではなく、振る舞いが型を成します。

Constable が Nuprl で採った立場が、これです。

なお、引用の中で denotational を 「外延的、集合的」 と訳していますが、本連載シリーズでは、一般的な訳語である 「表示的」 という言葉を用います。

「外延的」 は、あとで出てくる extensional の定訳です。
混同を避けるため、訳語を区別します。

タロウくん：
先程、「ある計算を実行したときの振る舞いが、ある条件を満たすかどうか。
その条件を満たす計算の集まりが、あとから型を成します。

先に計算があり、あとから型が決まる、という順序です」と述べられました。

そうすると、computational type theory を採用する言語において、型の宣言とは、ある式を評価（計算）したときの振る舞い方を宣言するということになるのでしょうか。

  • 評価（計算）したときに、振る舞い方 A になる式は、型 A と宣言する
     
  • 評価（計算）したときに、振る舞い方 B になる式は、型 B と宣言する

というように。

専任講師：
大筋は、その理解で合っています。
その上で、2点、補足説明が必要です。

1 点目。「宣言する」のではなく、「判断する」です。

Haskell で x :: Int と書くとき、プログラマは x の型を宣言しています。
型が先にあり、x をその型に入れる、という順序です。

computational type theory では、順序が逆なので、「宣言」という言葉はふさわしくありません。

  • 最初に式 $M$ があります。
  • 次に、$M$ を評価したときの振る舞いを調べ、その振る舞いが型 $A$ の条件を満たすなら、「$M$ は $A$ に属する」という判断を立てます。記号では M ∈ A と書きます。
    式 が先にあり、判断 がその後に続きます。

RedPRL の 論文 は、この点を次のように述べています。

In computational type theory, types are interpreted not as structured sets, but as behaviors specifying classes of programs.

（筆者訳）computational type theory では、型は構造を持つ集合としてではなく、プログラムの類を指定する振る舞いとして解釈される。

出典：
C. Angiuli, E. Cavallo, K.-B. Hou (Favonia), R. Harper, J. Sterling, "The RedPRL Proof Assistant (Invited Paper)", LFMTP 2018, EPTCS 274, §2. https://arxiv.org/abs/1807.01869

「型は振る舞いである」という言い方が、君の理解と対応します。

ただし、型を宣言するのではなく、型という振る舞いの条件に、式が合うかどうかを判断します 。

なお、「計算が先、型が後」という言い方は、Haskell や TypeScript の型推論
── プログラムを書いたあとにコンパイラが 型を推測する手順 ── を指すものではありません。

型推論は、型が先にある言語の中で、型の記述を省く仕組みです。

computational type theory の「型が後」は、型の意味付けの仕方 ── 型とは 何であるか ── をめぐる言葉です。

pic_2.jpg

2 点目。型 $A$ を定めるとき、決めることが2つあります。

1つ目は、どういう振る舞いをする式が $A$ に属するか。
君が挙げた「振る舞い方 $A$ になる式は型 $A$」が、これです。

もう1つは、$A$ に属する2つの式が、いつ等しいと見なされるか。

たとえば 2 + 2 と 4 は、どちらも自然数の型に属します。
しかし「属する」と決めただけでは、これら2つが等しいかどうかは決まりません。

等しさを別に定める必要 があります。

Nuprl では、型 $A$ を定めることは、この2つ
── 属する条件と、等しさの条件 ──
を 同時に 定めることです。

Allenほか の論文は、型 を、「項の集まりに与える等しさの取り決め」として定義 しています。

この2つ目が、次の問い ── 振る舞い方のどこを境に、同じ型と別の型を分けるのか ── につながります。

タロウくん：
順序が逆、というのは分かりました。

でも、まだ最初の問いに答えてもらっていません。

振る舞い方のどこを境にして、同じ型と別の型を分けるのですか？

専任講師：
その問いには、2 つの答えがあります。
「同じか別か」を決める 境が、2つある からです。

1つ目の境は、型の中での等しさです。

同じ 型に属する 2 つの項が、いつ等しいと見なされるか。

たとえば自然数の型なら、2 + 2 と 4 は等しい。
計算すれば 同じものに行き着くからです。
この境 を動かすと、同じ型の中で、等しいと見なされる項の組が変わり ます。

2つ目の境は、型そのものの等しさです。

2つの型 が、いつ同じ型と見なされるか。
この境 を動かすと、同じ型と見なされる型の組が変わり ます。

この2つ目が、computational type theory の特徴 です。

型もまた項なので、型が等しいかどうかも、計算の振る舞いで決まります。

📌 厳密性を担保した説明をすると……型どうしの等しさには universe の見方も関わる

本文では、「型もまた項なので」と説明しました。
これは、型どうしについても等しさを考える、という直観を伝えるための言い方です。

型理論では、型を項として扱う仕組みを universe（宇宙）で表すことが多く、型と項の関係には階層や表記上の注意があります。

そのため、「型も値とまったく同じ仕方で扱える」と理解すると、単純化し過ぎになります。

ここで必要なのは、より控えめな一点です。

Nuprl 系では、個々の値だけでなく、型どうしについても等しさを判断の対象にし、その扱いを計算的意味論と結び付けている、ということです。

計算の振る舞い方による型の定義と、等しさの定義：コード実装例

タロウくん：
computational type theory を実装した言語で、計算の振る舞いによる型の定義と、等しさの定義を具体的にどういうコードで書くのか、コード付きで教えてください。

専任講師：
いまから、以下の3つの設例を用いて、計算したときのどういう振る舞い方を型として定義するのか、また、等しさをどう定義するのか、3つの言語によるコード実装例を示します。

設例 型の定義 等しさの定義 書ける言語
設例 1 関数 nat から nat への関数の型 すべての入力に対して同じ出力を返せば、等しい RedPRL・redtt・cooltt
設例 2 n を法とする整数 要素は nat のまま 3 で割った余りが同じなら、等しい redtt のみ
設例 3 円周 base という点と、base から base へ戻る loop というパスで作られる型 base から base へ戻る 2 つのパスは、loop を巻いた回数が同じなら、等しい RedPRL・redtt

今回選んだ言語は、RedPRL・redtt・cooltt です。

いずれも Nuprl の系譜（学統）にあるカーネギーメロン大学のグループが開発した定理証明支援系で、筆者の環境で動かしました。

設例2 と 設例3 を 3つの言語すべてで書けない理由は、それぞれの箇所で述べます。

先に、ひとつ明確にしておきましょう。

「型を計算の振る舞いで定義する」という意味論は、Nuprl や RedPRL の設計者が与えたものです。利用者がコードで書くのは、その意味論のもとで「項が型に属する」という判断と、「2 つの項が等しい」という判断です。

以下の 3つの設例 は、型の定義 と 等しさの定義 が ペアになっていること を、コードで示します。

設例 1 ── 関数の型と、関数の等しさ

型の定義
nat から nat への関数の型です。
コードを掲載する各言語とも、関数型は組み込みです。

等しさの定義
2つの関数が等しいとは、すべての入力に対して同じ出力を返すことです。
これを、関数外延性 と呼びます。

具体例として、λx. x + 0 と λx. x が等しいことを示します。
この2つは、定義の形 は異なりますが、どの入力 $x$ に対しても、x + 0 を計算すれば x になるので、同じ出力を返します。

コードを掲載する各言語とも、n + 0 = n を帰納法で示した plus/zero/r を、すべての入力について適用します。

RedPRL

theorem FunEq :
  (= (-> nat nat) (lam [x] ($ Plus x zero)) (lam [x] x))
by {
  auto;
  with x => `($ PlusZeroR x)
}.

redtt

def fun-eq : path (nat → nat) (λ x → plus x zero) (λ x → x) =
  funext nat (λ _ → nat) (λ x → plus x zero) (λ x → x) plus/zero/r

cooltt

def fun-eq : path {nat → nat} {x => plus x 0} {x => x} :=
  funext nat nat {x => plus x 0} {x => x} plus/zero/r

RedPRL は外延的なので、関数の等しさは各入力について確かめる形になります。
auto のあとに、各 x について PlusZeroR x を与えると通ります。

Extract は ax ── 自明な証拠だけです。redtt と cooltt は、funext という関数を prelude に持っています。各入力についての等しさの証明 plus/zero/r を渡すと、関数どうしのパスが得られます。

なお、Plus・plus と PlusZeroR・plus/zero/r の定義は、3 言語とも次のとおりです。

RedPRL

theorem Plus :
  (-> nat nat nat)
by {
  lam m n =>
  `(nat-rec [_] nat m n [_ r] (succ r))
}.

theorem PlusZeroR :
  (-> [n : nat] (= nat ($ Plus n zero) n))
by {
  lam n =>
  elim n;
  [ auto
  , with ih n' =>
    unfold Plus; reduce at left;
    rewrite ih;
    [ with z => `(= nat (succ z) (succ n'))
    , auto
    ];
    auto
  ]
}.

redtt

def plus (m n : nat) : nat =
  elim m [
  | zero → n
  | suc (m → plus/m/n) → suc plus/m/n
  ]

def plus/zero/r : (n : nat) → path nat (plus n zero) n =
  elim [
  | zero → refl
  | suc (n → ih) → λ i → suc (ih i)
  ]

cooltt

def plus : nat → nat → nat :=
  elim [
  | zero => n => n
  | suc {_ => ih} => n => suc {ih n}
  ]

def plus/zero/r : (n : nat) → path nat {plus n 0} n :=
  elim [
  | zero => _ => 0
  | suc {n => ih} => i => suc {ih i}
  ]

設例 2 ── n を法とする整数

型の定義
要素は nat のままです。新しい要素は作りません。

等しさの定義
2 つの自然数が等しいとは、n で割った余りが同じことです。
ここでは n = 3 とします。0 と 3 は等しく、4 と 7 も等しい。0 と 4 は等しくない。

これは、前編で Allen らの論文から引用した Z//En
── 型 Z の要素はそのままで、等しさを「n を法として合同」に取り替えた型 ── の実装です。

この設例は redtt でしか書くことができません。

要素を変えずに等しさだけを取り替える仕組みは、商型 と呼びますが、redtt は data/quotient.red にこの 商型 が定義されています。

それに対して、RedPRL と cooltt については、筆者が調べた限りでは、商型を作る構文が見当たりませんでした。

redtt

import prelude
import data.quotient
import data.nat

-- 3 で割った余りを 1 つ進める：0 → 1 → 2 → 0
def mod3/step : nat → nat =
  elim [
  | zero → suc zero
  | suc n →
    elim n [
    | zero → suc (suc zero)
    | suc _ → zero
    ]
  ]

-- 3 で割った余り
def mod3 : nat → nat =
  elim [
  | zero → zero
  | suc (_ → r) → mod3/step r
  ]

-- 「3 を法として合同」という関係
def R (a b : nat) : type =
  path nat (mod3 a) (mod3 b)

-- 3 を法とする整数。要素は nat のまま。等しさだけを R に取り替える
def Z/3 : type = quotient nat R

def three : nat = suc (suc (suc zero))
def four  : nat = suc three
def seven : nat = suc (suc (suc four))

-- 0 と 3 は 3 を法として合同
def r03 : R zero three = refl

-- 4 と 7 も合同
def r47 : R four seven = refl

-- Z/3 の中では、0 と 3 のあいだにパスがある
def p03 : path Z/3 (pt zero) (pt three) = λ i → gl zero three r03 i

-- 4 と 7 のあいだにも
def p47 : path Z/3 (pt four) (pt seven) = λ i → gl four seven r47 i

-- 8 以降をベタ打ちする必要はない。nat の要素は zero と suc で帰納的に作られ、
-- mod3 も elim で帰納的に定義されているので、どの自然数にも余りが計算できる。
-- たとえば、加算で 10 を作り、1 と合同であることを確かめる
def plus (m n : nat) : nat =
  elim m [
  | zero → n
  | suc (m → plus/m/n) → suc plus/m/n
  ]

def ten : nat = plus seven three

-- 1 と 10 は 3 を法として合同（余りはどちらも 1）
def r1-10 : R (suc zero) ten = refl

def p1-10 : path Z/3 (pt (suc zero)) (pt ten) = λ i → gl (suc zero) ten r1-10 i

筆者の環境で、すべての定義が型検査を通りました。

mod3 が、3 で割った余りを計算する関数です。
R a b は、mod3 a と mod3 b が nat として等しい、という関係です。
quotient nat R が、nat の要素をそのままに、等しさを R に取り替えた型です。

r03 : R zero three = refl は、0 と 3 の余りが等しいことを、計算だけで確かめています。mod3 zero を計算すると 0、mod3 three を計算すると 0 になるので、refl で通ります。

対照実験として、def r04 : R zero four = refl を書くと、redtt は 1 unsolved hole を報告します。mod3 four を計算すると 1 になり、0 と一致しないからです。

p03 は、Z/3 の中で 0 と 3 を結ぶパスです。
gl は商型の構成子で、関係 R の証明 r03 を受け取って、0 と 3 のあいだのパスを作ります。
nat の中では 0 と 3 は別の要素ですが、Z/3 の中では等しくなります。

three・four・seven は、読みやすさのために名前を付けただけです。
8以降をベタ打ちで定義する必要はありません。

nat のすべての要素は、zero と suc で帰納的に作られます。

mod3 も elim で帰納的に定義されているので、どの自然数に対しても余りを計算できます。
したがって、R と Z/3 は、名前を付けた数だけでなく、すべての自然数について定まっています。

上のコードでは、加算 plus で ten = plus seven three を作り、1 と 10 が 3 を法として合同であることを refl だけで確かめています。

mod3 ten を計算すると、plus seven three が 10 に、mod3 10 が 1 になり、mod3 (suc zero) の 1 と一致します。

なお、redtt の quotient は、要素のあいだにパスを足す higher inductive type として定義されています。Nuprl の商型 A//E は、等しさの取り決めを E に置き換えるもので、パスを足すものではありません。同じ「商型」という名前で、作り方が違います。この違いは後編で扱います。

設例 3 ── 円周

過去記事「Haskell の Int は『空間』でもある — プログラミング言語のデータ型が持つもうひとつの顔」では、円周について次のように解説しました。

円周というのは、丸の輪郭そのもの です。
中身の円盤は含みません。線だけです。
そして、S¹ の輪郭上に 1 点を選び、その点に名前をつけて base と呼ぶ ことにします。
日本語で「基点」と訳します。
「どこでもいいから 1 点、目印になる場所」と思ってください。
地図で言えば、旅の出発地点を「ここ」と決めるようなものです。

図の中で、輪郭上の黒丸が base です。
ここでは輪郭の一番上に選びましたが、右でも下でも、選ぶ場所はどこでも構いません。
base を 1 つ決めたら、次のような問いが立ちます。
base から出発して、円周に沿って歩き、base に戻ってくる道は何通りあるか？

  • 動かないでその場にいる ── これも 1 つの道（動かない道）
  • 1 周して戻る ── これは動かない道とは違う道
  • 2 周して戻る ── これもまた違う道
  • 逆向きに 1 周 ── これもまた違う道

こうして、base から base への道は、「何周したか」で無限に区別できます。
左回りをプラス、右回りをマイナスと数えると、道の種類は 整数全体 ℤ と 1 対 1 に対応 します。
これが、代数トポロジーで 19 世紀末から知られている 「円周の基本群は ℤ である」 という古典的な事実です。

出典：
https://qiita.com/etale_cohomology/items/e3eae170f14f134c8f13

過去記事で述べたのは、base から base へ戻るパスは、loop を巻いた回数ごとにすべて異なる、だから基本群が整数と同じになる、ということです。

本記事の例は、その同じ定理を、逆の側から見ています。

過去記事で述べたのは「巻き数が違えば、パスは異なる」という側面です。
本記事で述べるのは「巻き数が同じなら、パスは等しい」という側面です。

この 2 つが合わさって、base から base へ戻るパスの集まりが、整数と一対一に対応します。
巻き数が違えば異なり、同じなら等しい。だから、パスを整数で数えられます。

本記事の例で確かめるのは、後者の側面です。loop を 3 回巻いたパスと、2 回巻いて 1 回戻してさらに 2 回巻いたパスは、見た目は違いますが、計算すると巻き数が同じ 3 になるので、等しいと判断されます。

先に、使う関数の出どころを明記します。以下のコードに出てくる関数は、RedPRL と redtt に組み込まれたものではありません。

RedPRL の

  • S1LoopConcat（パスの連結）
  • S1LoopInv（パスの反転）
  • S1LoopToInt（パスから巻き数への変換）
  • IntToS1Loop（巻き数からパスへの変換）
  • Loop（1 回巻くパス）

は、RedPRL の example ディレクトリにある omega1s1.prl の中で theorem として定義されたものです。RedPRL の開発者が example として書いた、ユーザー定義の定理です。

RedPRL に組み込まれているのは、

  • S1
  • base
  • loop
  • S1-rec

と、cubical の操作 hcom・coe です。

パスの連結と反転は、hcom を使って omega1s1.prl の中で定義されています。

redtt の

  • loopn（巻き数からパスへ）
  • winding（パスから巻き数へ）
  • Ω1s1（base から base へのパスの型）

は、redtt の library ディレクトリにある paths/s1.red の中で def として定義されたものです。

  • trans（連結）
  • symm（反転）

は、prelude の定義です。

円周 s1 自体も、data/s1.red の中で data として定義されています。

redtt に組み込まれているのは、data と elim の構文、comp・coe、パスの記法です。

本記事の 設例3 は、これらの定義を再利用して、その上に Loop3・Loop2Inv1Loop2（RedPRL）と loop3・loop2-inv1-loop2（redtt）を筆者が定義したものです。

型の定義
円周は、base という点と、base から base へ戻る loop というパスの、2 つの構成子で定義されます。

等しさの定義
base から base へ戻る 2 つのパスが等しいとは、巻き数が同じことです。巻き数は、パスを整数に変換する関数 ── RedPRL では S1LoopToInt、redtt では winding ── で計算します。

この設例は RedPRL と redtt の 2 言語で書きます。 cooltt の test には、円周の定義と、loop を n 回巻く関数はありますが、パスから巻き数を整数として取り出す関数がありません。取り出すには、整数型と、univalence を使った円周の被覆空間の構成が要ります。cooltt で 1 から書くのは本記事の範囲を超えるため、cooltt は省きます。

RedPRL

// loop を 3 回巻く
theorem Loop3 :
  (path [_] S1 base base)
by {
  `($ S1LoopConcat Loop ($ S1LoopConcat Loop Loop))
}.

// loop を 2 回巻き、1 回戻し、さらに 2 回巻く
theorem Loop2Inv1Loop2 :
  (path [_] S1 base base)
by {
  `($ S1LoopConcat Loop
     ($ S1LoopConcat Loop
       ($ S1LoopConcat ($ S1LoopInv Loop)
         ($ S1LoopConcat Loop Loop))))
}.

// どちらも巻き数は 3
theorem Loop3Winding :
  (= int ($ S1LoopToInt Loop3) (int 3))
by {
  unfold Loop3 Loop; auto
}.

theorem Loop2Inv1Loop2Winding :
  (= int ($ S1LoopToInt Loop2Inv1Loop2) (int 3))
by {
  unfold Loop2Inv1Loop2 S1LoopInv Loop; auto
}.

redtt

import prelude
import data.s1
import data.int
import paths.s1

-- loop を 3 回巻く
def loop3 : Ω1s1 = loopn (pos (suc (suc (suc zero))))

-- loop を 2 回巻き、1 回戻し、さらに 2 回巻く
def loop2-inv1-loop2 : Ω1s1 =
  trans s1
    (loopn (pos (suc (suc zero))))
    (trans s1
      (symm s1 (loopn (pos (suc zero))))
      (loopn (pos (suc (suc zero)))))

-- どちらも巻き数は 3。winding で整数に変換して比べる
def loop3/winding : path int (winding loop3) (pos (suc (suc (suc zero)))) =
  refl

def loop2-inv1-loop2/winding : path int (winding loop2-inv1-loop2) (pos (suc (suc (suc zero)))) =
  refl

筆者の環境で、両言語ともすべての定義が型検査を通りました。

RedPRL では、S1LoopConcat がパスの連結、S1LoopInv がパスの反転です。S1LoopToInt がパスを整数に変換します。Loop3 と Loop2Inv1Loop2 は、連結と反転の組み合わせ方が違います。しかし、S1LoopToInt で整数に変換すると、どちらも (int 3) になります。証明は auto だけで通り、Extract は ax です。

redtt では、loopn が整数から巻き数分のパスを作り、winding がパスから整数を取り出します。trans がパスの連結、symm が反転です。winding loop3 と winding loop2-inv1-loop2 は、どちらも refl だけで pos 3 に等しいと示せます。計算するだけで、巻き数が 3 に到達するからです。

設例 3 は、巻き方の数（巻いて、戻して（逆向きに巻いて）を合計した結果、差し引きの巻回数）は無限個の整数がありえますから、設例 2 と同様に、帰納的に定義できます。

redtt の loopn は、整数を受け取ってパスを返す関数で、paths/s1.red に次のように定義されています。

def loopn : int → Ω1s1 =
  elim [
  | pos n →
    elim n [
    | zero → refl
    | suc (n → loopn) →
      λ i → comp 0 1 (loopn i) [ i=0 → refl | i=1 j → loop j ]
    ]
  | negsuc n →
    elim n [
    | zero →
      λ i → comp 1 0 base [ i=0 → refl | i=1 j → loop j ]
    | suc (n → loopn) →
      λ i → comp 1 0 (loopn i) [ i=0 → refl | i=1 j → loop j ]
    ]
  ]

正の整数 pos n については n について帰納的に、負の整数 negsuc n についても n について帰納的に、パスを組み立てています。したがって、loopn はどの整数に対しても定義されています。3 回巻くパスも、100 回巻くパスも、逆向きに 50 回巻くパスも、同じ定義から作られます。

RedPRL の IntToS1Loop も、omega1s1.prl の中で、整数について帰納的に定義されています。

見た目の違う 2 つのパスが、巻き数という計算の結果で等しいと判断される。これが、円周における「等しさの定義」です。

この 3 つの設例から分かること

設例 1 では、関数の等しさを「すべての入力で同じ出力」と定め、それを各入力について計算した結果で確かめました。

設例 2 では、nat の等しさを「3 で割った余りが同じ」に取り替え、余りを計算した結果で確かめました。

設例 3 では、円周のパスの等しさを「巻き数が同じ」と定め、巻き数を計算した結果で確かめました。

3 つとも、型が何であるかと、その型で何を等しいと見なすかが、ペアで定まっています。そして、等しいかどうかの判断は、計算の結果を比べることで行われています。

筆者の環境では、次のとおり実行できました。

設例 1 は、

  • RedPRL（funext-ex.prl）
  • redtt（funext-ex.red）
  • cooltt（funext-ex.cooltt）

の全定義が通過しました。

設例 2 は、 redtt（zmod3.red）の全定義が通過し、対照実験の r04 は 1 unsolved hole で止まりました。

設例 3 は、

  • RedPRL（s1winding.prl、omega1s1.prl の定義を再利用）
  • redtt（s1winding.red）

の全定義が通過しました。

タロウくん：
設例 2 で、要素は nat のままで、等しさだけを「3 で割った余りが同じ」に取り替えた型を見ました。Nuprl では、この仕組みをどう定義しているのですか？
これは、「型の中での等しさ」の境を動かすと型が変わる、という例にもなっていると思いました。
どの数字で割った余りを同じと定義するか、が変わるからです。

専任講師：
その認識であっています。そして、Nuprl では、商型（quotient type） と呼びます。

Nuprl の商型 は、まさに「何を等しいと見なすかを取り替える」仕組みです。
型 $A$ には、等しさの関係 =A が付いています。

$E$ が $A$ の上の同値関係である とき、A//E という 新しい型 を作ることができます。A//E の要素は $A$ の要素と同じですが、等しさが $E$ に置き換わります。

たとえば、En(x, y) を「$x$ と $y$ は $n$ を法として合同」とすれば、Z//En は $n$ を法とする整数になります。要素は整数のままです。等しさだけを取り替えると、別の型になります 。

📌 厳密性を担保した説明をすると……本文の一般例と、redtt の小さなコード例は同じ対象ではない

本文の一般例 Z//En は、整数の型 $Z$ を $n$ を法とする合同関係で割るイメージです。
一方、その直後の redtt のコードでは、入門用に自然数 nat を使い、「偶奇が等しい」という関係で商を作っています。

したがって quotient nat R は、整数全体の剰余類を厳密に実装した例ではありません。
自然数を偶奇で同一視する例です。

負の数を含むか、加法・乗法をどう定義するか、といった数学的構造まで同じになるわけではありません。

ただし両者は、「要素の候補を大きく変えずに、どの要素を同一視するかを変える」という商型の 直観を共有 します。

コードの目的は、整数論を完全に実装することではなく、この直観を小さく動かして確かめること です。

出典：
S. F. Allen, M. Bickford, R. L. Constable, R. Eaton, C. Kreitz, L. Lorigo, E. Moran, "Innovations in computational type theory using Nuprl", Journal of Applied Logic 4(4), 2006, pp. 428-469. https://www.sciencedirect.com/science/article/pii/S1570868305000704

これを、筆者の環境で動かしました。
動かしたのは、redtt という証明支援系です。

redtt は、Nuprl の系譜（学統）にあるカーネギーメロン大学のグループが 2018年に開発した定理証明支援系です。

import prelude
import data.quotient
import data.nat
import data.void
import data.unit
import data.bool

-- 偶奇を bool で返す
def parity : nat → bool =
  elim [
  | zero → tt
  | suc (n → p) → not p
  ]

-- 偶奇が等しい、という関係
def R (m n : nat) : type =
  path bool (parity m) (parity n)

-- 2 を法とする整数。
-- 要素は nat のまま。等しさだけを「偶奇が等しい」に取り替える。
def Z/2 : type = quotient nat R

def two : nat = suc (suc zero)

-- 0 と 2 は偶奇が等しい
def r02 : R zero two = refl

-- 商型 Z/2 の中では、0 と 2 のあいだにパスがある
def p02 : path Z/2 (pt zero) (pt two) = λ i → gl zero two r02 i

筆者の環境で、すべての定義が型検査を通りました。

📌 コラム：Nuprlの商型とredttのquotientは同じものではない

Nuprl の quotient type は、型 $A$ にもともと備わっている等しさを、同値関係 $E$ によって 置き換えるという computational type theory の商型です。

他方で、redtt の quotient は higher inductive type として構成されています。

どちらも「異なる代表元を等しいものとして扱う」という数学的目的を持ちますが、型理論上の実現方法は同じではありません。

本記事の redtt のコードは、Nuprl の商型をそのまま実装したものではなく、redtt における quotient の構成を使って同じ数学的 直観 を確認したものです。

対照実験として、最後の行を次のように変えます。

def p02/nat : path nat zero two = refl

nat の中で、0 と 2 のあいだにパスを作ろうとしています。
redtt は 1 unsolved hole を報告しました。作れない、ということです。

📌 厳密性を担保した説明をすると……unsolved hole は、その書き方で証明が完成しないことを示す

1 unsolved hole という表示が直接示しているのは、本文に書いた定義、すなわち refl を置く書き方では証明の穴が埋まらない、ということです。

nat における 0 と 2 のあいだにパスが存在しないこと自体は、型理論の意味論や正規形についての説明を使って、別に正当化する話になります。コンパイラのエラー表示だけが、その一般的な不可能性を数学的に証明しているわけではありません。

本文の対照実験で確かめているのは、Z/2 では与えた関係から 0 と 2 を結ぶパスを構成できるのに対し、nat では同じ形の定義を refl で通すことはできない、という違いです。

同じ 0 と 2 が、nat の中では別の要素で、Z/2 の中では等しい。
型を変えると、何を等しいと見なすかの境が変わります。

これが、境の取り替え です。

1 点、注意を要する点があります。

redtt の quotient は、Nuprl の商型 A//E をそのまま実装したものではありません。

Nuprl の商型は、型 $A$ に備わっている等しさを 同値関係 $E$ で置き換えます 。

redtt の quotient は、higher inductive type として構成されています。

どちらも「異なる要素を等しいものとして扱う」という目的を持ちますが、型理論上の実現方法は同じではありません。

上のコードは、redtt の quotient の構成を使って、同じ数学的な 直観 を確かめたものです。
2つの商型の違いは、後編の記事 で解説します。

pic_3.jpg

画像の弧に添えた gl 0 2 r02 は、コードの最後の行 gl zero two r02 i に対応しています。

gl は redtt の商型の構成子で、4 つの引数をとります。
1つ目と2つ目は、もとの型の要素です。

3つ目は、その 2つが関係 R で結ばれていることの証明です。

4つ目は、区間 𝕀 の点 i です。
i を 0 から 1 へ動かすと、1 つ目の要素から 2 つ目の要素へ至るパスになります。

画像では、0 と 2 の偶奇が等しいことの証明 r02 を 3 つ目の引数に渡し、0 と 2 を結ぶパスを作っています。

（画像：同じ 0 と 2 が、型を変えると等しくなる）

画像プロンプト（商型）

タロウくん：
等しいと見なす範囲は、定理証明支援系によって違うのですか？

専任講師：
違います。

Lean 4 や Rocq では、型検査のときに計算が走ります。
2 + 2 と 4 は、型検査器が計算して同じだと判断 します。

これを、定義的等価性（definitional equality） と呼びます。

Dedukti連載の2回目の記事で取り上げました。

ただし、Lean 4 や Rocq では、定義的等価性 と、命題としての等しさ（propositional equality） は、完全に別のもの です。

このため、等しいと都合よく証明できるものが限られます。

Rocq では 0 + n = n は 定義的等価性 に従いますが、n + 0 = n は 帰納法による証明 が必要になります。

Nuprl では、この 2 つが一致します。

「この2つの関数は、どの入力に対しても同じ値を返す」という等しさ ── 外延的な等しさ ── を、型の等しさとして認めるからです 。

📌 厳密性を担保した説明をすると……外延性・等式反映・関数外延性は別の言葉である

本文では、Nuprl 系の特徴として equality reflection（等式反映）を説明しています。これは、命題として証明された等しさを、判断上の等しさとしても使えるようにする規則です。

一方で「外延的」という語は、より広く使われます。代表例は関数外延性で、「すべての入力で同じ出力を返す 2 つの関数を等しいと見なす」という性質です。

どちらも「振る舞いにもとづいて同一視する」という印象を与えますが、同じ規則ではありません。外延的型理論が必ず equality reflection を採用するわけでも、関数外延性だけで equality reflection が得られるわけでもありません。

本文では、Nuprl 系と Lean 4・Rocq の違いを、型検査の決定可能性との関係から説明するため、equality reflection を中心に据えています。

出典：
T. Ringer, K. Palmskog, I. Sergey, M. Gligoric, Z. Tatlock, "QED at Large: A Survey of Engineering of Formally Verified Software", Foundations and Trends in Programming Languages, arXiv:2003.06458. https://arxiv.org/abs/2003.06458

この一致をもたらすのが、equality reflection（等式反映）という規則 です。

命題として等しいことが証明できれば、判断として等しいと扱ってよい、という規則 です。
Nuprl とその後継 ── RedPRL を含む ── が採用 しています。

出典：
J. Sterling, C. Angiuli, D. Gratzer, "Cubical Syntax for Reflection-Free Extensional Equality", arXiv:1904.08562. https://arxiv.org/abs/1904.08562

タロウくん：
一致すると、何が起きるのですか？

専任講師：
証明の検査が、決定不能になります。

命題としての等しさで、決定不能な問題を記述できるからです。

Lean 4 や Rocq の型検査器は、有限の手順で必ず 答えを出します。
Nuprl では、その保証がありません。

📌 厳密性を担保した説明をすると……決定不能なのは、証明支援系が何も確認できないという意味ではない

ここで「決定不能」と言っている対象は、equality reflection を含む一般の判断・型検査について、任意の入力に対して必ず有限時間で yes / no を返す完全な手続きがない、という性質 です。

これは、Nuprl や RedPRL で証明を確認できない、あるいは自動化がまったく使えない、という意味ではありません。簡約、タクティク、特定の形に限った決定手続きなどにより、多くの導出を実際に構築・確認できます。

また、型検査が決定可能な Lean 4 や Rocq でも、定理を発見したり、帰納法の方針を選んだりする作業まで自動化されるわけではありません。

本文でいう取引は、「何でも自動」対「何も自動でない」ではなく、型検査器にどこまでの等しさの判断を任せられるか、という違い です。

つまり、等しいと見なす範囲をどこまで広げるかは、こういう取引 です。

範囲を狭くすれば、2つの項が等しいかどうかを型検査器が自動で判定できる。その代わり、等しいと認められる項の組が少なく、人間が証明を書く場面が増える。

Lean 4 や Rocq は、こちらを選んでいます。

本記事では、範囲を狭くする選択を「線を手前に引く」と呼びます 。

他方で、範囲を広くすれば、数学者が等しいと考えるものを、そのまま等しいと記述できる。その代わり、2 つの項が等しいかどうかを型検査器が自動で判定できず、人間がタクティクを書いて証明を組み立てる必要がある。

Nuprl は、こちらを選んでいます。
本連載シリーズでは、範囲を広くする選択を「線を奥に引く」と呼びます 。

pic_4.jpg

タロウくん：
「2 つの項が等しいかどうかを型検査器が 自動で判定できない 」というのは、実際にはどう見えるのですか？

専任講師：
証明を組み立てるのが、型検査器ではなく、人間のタクティクになります。

同じ定理を、RedPRL と Lean 4 で証明してみます。「not (not b) = b」という、bool の定理です。

RedPRL の example/tutorial.prl にある証明です。

theorem NotNot :
  (->
   [b : bool]
   (= bool ($ Not ($ Not b)) b))
by {
  lam b =>
  unfold Not;
  if b
  then (reduce at left; refine bool/eq/tt)
  else (reduce at left; refine bool/eq/ff)
}.

unfold、reduce at left、refine bool/eq/tt。
人間がタクティクを並べて、証明を組み立てています。

Lean 4 での証明です。筆者が書きました。

theorem NotNot : ∀ b : Bool, Not' (Not' b) = b := by
  intro b; cases b <;> rfl

cases b で場合分けしたあと、rfl だけです。
型検査器が両辺を計算して、等しいと判定します。

「型検査が決定不能である」という性質そのものは、画面に映りません。

映るのは、証明を組み立てるのが人間のタクティクか、型検査器の自動判定かという違い です。

📌 厳密性を担保した説明をすると……タクティクと型検査器は、どちらか一方だけを使う道具ではない

本文の比較は、RedPRL と Lean 4 の一つの小さな定理で、導出の組み立て方がどう見えるかを示したものです。

Lean 4 や Rocq でもタクティクは広く使われます。
cases、simp、rw、帰納法などを使い、人間と自動化が協力して証明を作ります。

逆に RedPRL にも auto のような自動化があります。

違いは「一方は人間、他方は機械」という二分法ではありません。

equality reflection を採る系では、一般の型検査だけで等しさを決め切ることを期待せず、タクティクや部分的な決定手続きがより重要な位置を占めます。

本文のコード比較は、その傾向を一つの例で示したものです。

pic_5.jpg

なお、RedPRL の tutorial.prl には、「次の 4 行は auto で置き換えられる」というコメントがあります。

RedPRL にも自動化はあります。

ただし、それは部分的な決定手続きであり、型検査器の判定ではありません。

Sterling らの論文は、この流儀の証明支援系が型検査を支えるのではなく、タクティクと部分的な決定手続きによる導出の対話的な構築に大きく依存する、と述べています。

タロウくん：
等しいと見なす範囲を広くすると、証明の形はどう変わるのですか？

専任講師：
等しさの証明が、証明項から消えます。

もう 1 つ、同じ tutorial.prl の定理 を証明する例で比較してみましょう。

「family b の要素が与えられたら、family (not (not b)) の要素を作れ」という定理です。

RedPRLの証明項 です。

Thm:
  (->
   [family : (-> bool (U 0))]
   [b : bool]
   ($ family b)
   ($ family ($ Not ($ Not b))))

Extract:
  (lam [x0 x1 x2] x2)

Extract が、証明の計算的内容です。
第3引数 x2 を、そのまま返しています。

not (not b) = b という等しさの証明は、どこにも現れません。

Lean 4 で同じものを書きました。

def RespectEquality
    (family : Bool → Type) (b : Bool) (pf : family b) :
    family (Not' (Not' b)) := by
  rw [NotNot]; exact pf

#print で証明項を表示すると、こうなります。

fun (family : Bool → Type) (b : Bool) (pf : family b) =>
  @Eq.mpr.{1} (family (Not' (Not' b))) (family b)
    (RespectEquality._proof_1 family b) pf

Eq.mpr という書き換えが、証明項に残っています。

NotNot の証明を使って、型を書き換えてから pf を返す、という形 です。

RedPRL では、厳密な等しさの証明が実行時に現れないのに対して、Lean 4では、書き換えが証明項に残ります。

等しいと見なす範囲を広くした Nuprl や RedPRL では、厳密な等しさの証明は計算に痕跡を残しません。

それとは対照的に、範囲を狭くした Lean 4 や Rocq では、等しさの証明を証明項の中で明示的に使う必要があります。

pic_6.jpg

📌 厳密性を担保した説明をすると……表示された証明項と、実行時コストは同じではない

本文では、Lean 4 の #print に Eq.mpr が現れ、RedPRL の Extract には対応する transport が現れないことを比べました。

この比較は、「依存型の書き換えを証明項として明示するか」を見るには有用です。

ただし、証明項を表示したときに Eq.mpr が見えることと、その書き換えが実行時に必ずコストとして残ることは同じではありません。

Lean のコンパイル・proof の消去・最適化の状況や、プログラムが proof を実際に計算に使うかによって事情は変わります。

ここでの要点は性能比較ではありません。

Nuprl／RedPRL の厳密な等しさでは、proof-irrelevant な扱いにより、等しさの証拠が、取り出される計算内容に現れない構造を持つ、という点 です。

「厳密な等しさ」と限定したのには理由があります。

RedPRL には、等しさが2種類ある からです。

  • 厳密な等しさ（exact equality）
  • パス（path）

の2つです。

厳密な等しさの証明は計算的内容を持ちませんが、パスは計算的内容を持ちます。

ここで見ているのは、厳密な等しさについての話 です。

tutorial.prl のコメントも、実行時に transport が不要であることを述べています。

タロウくん：
等しさの証明が消える、というのは、具体的にはどういうことですか。

専任講師：
等しさの証明は、すべて等しい、ということです。

同じ tutorial.prl に、次の定理があります。

// In fact, all proofs of (not(not(b)) == b) are equal.
theorem EqualityIrrelevant :
  (=
    (-> [b : bool] (= bool ($ Not ($ Not b)) b))
    NotNot
    (lam [b] ax))
by {
  auto
}.

NotNot という証明と、lam [b] ax という証明が、等しいと判定されます。Extract は ax ── 自明な証拠 ── だけです。

等しさの証明はすべて等しく、計算的内容を持ちません。これを proof-irrelevant と呼びます。

これに対して proof-relevant という立場 があります。
2つの対象の間には、「両者が等しいという主張」の根拠が複数、存在する場合 があります。

このとき、ホモトピー型理論（HoTT） は、2 つの対象の間をつなぐ異なる 2 つの経路（path）が伸びていると表現します 。

（参考）

proof-relevant は、複数の経路を同じ 1 つのものとして混同せずに、異なる2つの経路があると区別して扱います。

RedPRL は、外延的で proof-irrelevant な「厳密な等しさ」と、高次元で proof-relevant な「パス」が共存する、二層の型理論を実装しています。

pic_7.jpg

📌 厳密性を担保した説明をすると……proof-irrelevant なのは、ここでいう「厳密な等しさ」である

本文の EqualityIrrelevant が示しているのは、厳密な等しさ（exact equality）の証明について、どの証明を選んでも区別しないという性質です。

これは「RedPRL では、あらゆる equality proof や path proof が計算的に無意味になる」という意味ではありません。RedPRL の path は proof-relevant であり、異なるパスを区別する高次元の情報を持ち得ます。

したがって、本文の「等しさの証明はすべて等しい」という説明は、直前に扱った厳密な等しさの範囲で読む必要があります。

RedPRL では、proof-irrelevant な厳密な等しさと、proof-relevant な path が役割を分けて共存しています。

出典：
C. Angiuli, E. Cavallo, K.-B. Hou (Favonia), R. Harper, J. Sterling, "The RedPRL Proof Assistant (Invited Paper)", LFMTP 2018, EPTCS 274, pp. 1-10. DOI: 10.4204/EPTCS.274.1 ／ arXiv:1807.01869. https://arxiv.org/abs/1807.01869

対話篇 ── 研究はいつ始まったのか。当初の動機と目的は何か

タロウくん：
computational type theory の研究は、いつ始まったのですか？
何を動機として、何を目的に始まったのですか？

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

年 出来事
1968 年 Robert L. Constable が Cornell の計算機科学科に着任
1971 年 Constable が、プログラミング言語としても機能する構成的数学の形式理論を設計し実装する、という構想を打ち出す
1979 年 PRL 研究グループが Joseph L. Bates と Constable によって設立される
1983 年 Constable が Nuprl の構築を開始
1984 年 Nuprl の版が動く。以後、証明開発システムの一族に取り組む
1985 年 書籍『Implementing Mathematics with the Nuprl Proof Development System』（Prentice-Hall）
2006 年 Allen ほか「Innovations in computational type theory using Nuprl」

出典：

pic_8.jpg

タロウくん：
設立の趣旨は、何だったのですか？

専任講師：
Cornell の公式サイトが、次のように述べています。

The PRL research group was founded in 1979 by Joseph L. Bates and Robert L. Constable. It began as a project to build a logic-based program development system in which programs are constructed by interactive refinement.

（筆者訳）PRL 研究グループは、1979 年に Joseph L. Bates と Robert L. Constable によって設立された。論理にもとづくプログラム開発システムを作る計画として始まった。そのシステムでは、プログラムは対話的な精密化によって組み立てられる。

出典：
https://nuprl-web.cs.cornell.edu/Intro/subintro.html

タロウくん：
動機を整理すると、どうなりますか。

専任講師：
3 点に整理できます。

1 点目。プログラムを、証明の副産物として得ること。

Constable は 1971 年に、構成的数学の形式理論をプログラミング言語としても使う構想を打ち出しました。Cornell の紹介ページは、この仕事が信頼できるソフトウェアの生産を自動化する新しい道につながった、と述べています。

2 点目。普遍的なプログラミング言語を、理論の一部として持つこと。

Allen ほかの 2006 年の論文は、computational type theory が、数学と計算の実務の両方において計算についての推論の基礎を与えるよう設計された、密接に関連する理論の一族である、と述べています。

あわせて、計算機科学者が普遍的なプログラミング言語を理論の不可欠な一部として持ちたいと願う気持ちに強く影響されている、とも述べています。

3 点目。Cornell の初期の仕事の継承。

この要請は、Cornell で PLC プログラムを論理のアルゴリズムとした PLCV という、プログラミング論理の初期の仕事にさかのぼります。

出典：
S. F. Allen ほか, "Innovations in computational type theory using Nuprl", Journal of Applied Logic 4(4), 2006. https://www.sciencedirect.com/science/article/pii/S1570868305000704

タロウくん：
Martin-Löf の型理論とは、どういう関係ですか？

専任講師：
Allen ほかの論文は、computational type theory が Martin-Löf の直観主義型理論と、Rocq に実装された Calculus of Inductive Constructions に密接に関連する、と述べています。

また、Martin-Löf による propositions-as-types 原理への革新は、命題 $P$ の証明そのものではなく、証明の計算的内容を使う点にあった、とも述べています。

Martin-Löf の meaning explanation
── 型の意味を、その型の要素がどう計算されるかによって説明する立場
── が、computational type theory の出発点です。

対話篇 ── 動機と目的は変わったのか

タロウくん：
1979 年の当初の動機と、2026 年 9 月現在の動機とで、変化はありますか？あるとすれば、なぜ、どう変わったのですか？

専任講師：
変化しています。

当初、1979 年から 2000 年代までの動機は、証明からプログラムを取り出すことでした。

計算についての推論の基礎を与えること。分散システムの正しい部品を合成すること。

Nuprl は現在も使われています。

Cornell の紹介ページによれば、正しさが構成によって保証される分散プロトコルの作成に使われています。

プロトコルの仕様を Nuprl で記述し、その仕様を満たすことの証明から、プロトコルを実行するプログラムを取り出す、という使い方です。1971 年の構想が、分散システム という対象に向けられています。

さらに、Nuprl の実装自体が、2000 年以降は 分散システム になっています。

Allen ほかの論文は、Nuprl が 分散システム として、また 抽象オブジェクト識別子の概念を用いた形式数学のトランザクションデータベース として構築されていることを述べています。

Nuprl で証明された定理に加えて、HOL・MetaPRL・PVS で証明された
定理の一部 も収めて、保管する場所として使われています

出典：

産業での利用事例について、筆者が確認できたのは以下の通りです。

Rahli・Guaspari・Bickford・Constable が 2015 年の国際ワークショップ AVoCS で発表した論文の要旨に、次のように書かれています。

We discuss here a methodology that has proven itself in building a state of the art implementation of Multi-Paxos and other distributed protocols used in a deployed database system.

（筆者訳）本稿では、Multi-Paxos やその他の分散プロトコルの最先端の実装を構築するうえで実績を示した手法を論じる。それらの実装は、配備されたデータベースシステムで使われている。

出典：
V. Rahli, D. Guaspari, M. Bickford, R. L. Constable, "Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML", AVoCS 2015, Electronic Communications of the EASST, Vol. 72, 2015. https://eceasst.org/index.php/eceasst/article/view/2195

EventML は、Nuprl を裏で使う分散プロトコルの仕様記述言語です。

この論文は、EventML で記述した Multi-Paxos の実装が、配備されたデータベースシステムで使われている、と述べています。

同じ論文の本文には、Multi-Paxos のような産業水準の耐障害分散プロトコル を実装するのにこの手法を使った、とも書かれています。

ただし、どのデータベースシステムかは、筆者が確認した範囲では書かれていません。研究は DARPA の CRASH プロジェクトの支援を受けています。

2010 年代以降、新しい動機が加わりました。homotopy type theory の univalence と higher inductive types に、計算的な内容を与えることです。

理由は、次のとおりです。

RedPRL の論文は、通常の型理論であれば閉じた項 $n$ はある数値を計算するアルゴリズムを表すが、homotopy type theory には 計算的意味論がない ため、Brunerie の証明がそうしたアルゴリズムを与えると期待する理由がない、と述べています。

複数の研究者が、型理論の構文と意味論を cubical な仕組みで拡張することにより、univalence と higher inductive types の構成性を確立しました。その 1 つが Cohen らの（De Morgan）cubical type theory であり、cubicaltt という型検査器に実装されました。RedPRL は別の道 ── Cartesian cubical computational type theory ── にもとづく対話的証明支援系です。

出典：C. Angiuli ほか, "The RedPRL Proof Assistant (Invited Paper)", LFMTP 2018. https://arxiv.org/abs/1807.01869

タロウくん：
なぜ、homotopy type theory には計算的意味論がないのですか。

2 つの対象の間が等しいとき、その等しさの根拠となるものが 2 つ以上あるとき、それぞれの等しさの根拠は、具体的に計算できる根拠であり、計算論的な意味を持つのではないのですか。

専任講師：
君の直観は正しいです。

等しさの根拠は、計算論的な意味を持つべき ものです。

問題 は、homotopy type theory の 最初の定式化では 、その意味を実際に計算する仕組みが備わっていなかった、という点 にあります。

順に述べます。

**homotopy type theory の最初の定式化は、Martin-Löf 型理論に univalence を公理として加えたものでした。**2013 年に公開された HoTT Book が、その定式化です。

univalence は、「型 A と型 B が同値であれば、A と B は等しい」という原理です。この原理を、HoTT Book は 公理として導入 しました。ua : (A ≃ B) → (A = B) という形で、同値から等しさの証明を作る関数を、証明なしに仮定した、ということです。

公理には、計算規則がありません。

Martin-Löf 型理論では、等しさの証明 p : a = b に沿って、$a$ についての性質を $b$ についての性質へ移す操作があります。transport と呼びます。

transport は、p が refl ── 自明な 等しさの証明 ── であるときに 計算規則を持ちます。 transport refl x は x に簡約されます。

ところが、ua e は refl ではありません。
公理から作られた証明項だから です。

transport (ua e) x を簡約しようとしても、ua に計算規則がないので、そこで止まります。
この状態を、項が stuck である、と言います。

その結果、閉じた項が数値に到達しません。

pic_add_1.jpg

Brunerie の証明は、π₄(S³) という群が ℤ/n の形をしていることを示し、その $n$ を定義しました。$n$ は、閉じた自然数の項です。

通常の型理論であれば、閉じた自然数の項は計算すれば数値になります。

しかし Brunerie の $n$ の定義は、univalence を経由しています。計算しようとすると ua で止まり、数値に到達しません。

RedPRL の論文が「homotopy type theory には計算的意味論がないため、Brunerie の証明がそうしたアルゴリズムを与えると期待する理由がない」と述べているのは、このことです。

出典：C. Angiuli, E. Cavallo, K.-B. Hou (Favonia), R. Harper, J. Sterling, "The RedPRL Proof Assistant (Invited Paper)", LFMTP 2018, EPTCS 274, §1. https://arxiv.org/abs/1807.01869

タロウくん：
では、等しさの根拠が計算論的な意味を持つようにするには、どうすればよいのですか？

専任講師：
univalence を公理ではなく、計算規則を持つ構成として与えることです。
それを実現したのが、cubical type theory です。

cubical type theory は、区間 $I$ という型を導入し、等しさの証明を「区間 I から型への関数」── パス ── として表します。

そして、パスに沿った transport を、coe や hcom といった操作の計算規則として定義 します。
この設定では、ua e に沿った transport が、e の中身に従って実際に計算されます 。

つまり、君が言う 「等しさの根拠は計算できるはずだ」という直観を、型理論の中で実現するために必要だったのが、cubical という仕組み です。

pic_9.jpg

HoTT Book の型理論では、その直観を書き表すことはできても、計算することはできませんでした。

Brunerie の証明は、2023 年に Ljungström と Mörtberg が Cubical Agda で形式化しました。
ただし、Brunerie の元の定義をそのまま計算したのではありません。

Brunerie が博士論文で概略しか示さなかった技術的結果を回避するよう証明を修正し、その過程で得られた、より単純な Brunerie 数のひとつを計算しました。

その数は −2 に正規化され、π₄(S³) ≅ ℤ/2ℤ の形式化された証明が完成しました。

Brunerie の元の定義が実際に計算できるかどうかは、2023 年 11 月の Mörtberg の投稿によれば、未解決のままです。

出典：
A. Ljungström, A. Mörtberg, "Formalizing π₄(S³) ≅ ℤ/2ℤ and
Computing a Brunerie Number in Cubical Agda", LICS 2023.
arXiv:2302.00151. https://arxiv.org/abs/2302.00151
Distinguished Paper Award（LICS 2023）

タロウくん：
研究の目的意識（動機）の変化を要約すると、どうなりますか？

専任講師：
こうなります。

当初  証明からプログラムを取り出す。分散システムを正しく合成する
      ↓
現在  homotopy type theory の univalence に計算的内容を与える
      ↓
共通  「計算の振る舞いを土台に置く」という方法論は変わっていない

pic_10.jpg

RedPRL の論文は、Nuprl で開拓された computational type theory の方法論を論じたうえで、その証明論的な実現を RedPRL で記述する、という構成を採っています。

方法論そのものは継承されているのです。

現在の実装を並べます。

  • Nuprl : Cornell。1984 年から。現在も分散プロトコルの合成に使用
  • MetaPRL : computational type theory のもう 1 つの実装
  • RedPRL : カーネギーメロン大学。2016〜2018 年。Cartesian cubical computational type theory
  • redtt : RedPRL の後継。2018 年
  • cooltt : さらに後継。2021 年

出典：
RedPRL 公式サイト. https://redprl.org/

ただし、redtt と cooltt が computational type theory の流儀を採用しているかどうかは、後編の記事 で確かめます。

答えを先に述べると、採用していません。
その理由も、後編記事 で解説します。

対話篇 ── 採用した言語と、採用しない言語とで何が違うのか

タロウくん：
computational type theory を採用した言語と、採用しない言語とで、何が違うのですか？

設計思想の違い、
言語としてできること・できないことの違い、
使いやすさの違い

を教えてください。

専任講師：
先に、ひとつ明確にしておきましょう。

ここでいう「言語」は、Nuprl・RedPRL・Rocq・Lean 4・Agda といった定理証明支援系です。

Haskell・Rust・Go のようなふつうのプログラミング言語は、computational type theory を採用していません。

ふつうのプログラミング言語との関係は、次の対話篇で扱います。

対比表にします。

computational type theory 系
Nuprl / RedPRL		 内包的型理論系
Rocq / Lean 4 / Agda
等しさの扱い 定義的等価性と命題的等価性が一致する（equality reflection） 完全に別のもの
型検査 決定不能 決定可能
証明の対象 型のない生の項（realizer） 型の付いた項
証明の進め方 タクティクと部分的な決定手続きによる対話的な導出の構築 型検査器が自動で判定
n + 0 = n 等しいものとして扱える 帰納法による証明が必要
商型 A//E として直接作れる setoid や quotient で迂回する必要がある
設計の優先順位 計算的な意味論による正当化 構造規則の許容性、型付けの決定可能性、複数のモデルでの解釈可能性
📌 厳密性を担保した説明をすると……商型の「ある／ない」は一語では比較できない

本文の表では、Nuprl 系と内包的型理論系で商型の扱いが異なることを示しました。

ただし、Rocq・Lean 4・Agda をまとめて「商型がない」と言うことはできません。たとえば Lean 4 には Quot があり、Rocq には setoid を使った開発や、ライブラリ・拡張による複数の方法があります。Agda でも、採用する公理や cubical な拡張によって選択肢が変わります。

ここで比べたいのは、商型を表現できるかどうかだけではありません。

Nuprl の A//E は、型に備わる等しさを別の同値関係へ取り替えるという CTT の考え方と直結しています。

各系の quotient は、同じ数学的目的を持つことがあっても、規則・計算の振る舞い・証明で使う際の制約が同一とは限りません。

pic_11.jpg

タロウくん：
最後の行の「設計の優先順位」について、もう少し説明してください。

専任講師：
Sterling らの論文が、この違いを述べています。

Nuprl 流の形式体系は、Martin-Löf の計算的な意味の説明に触発された、ただ1つの意図された意味論に対する「真理への窓」として働きます。

Nuprl の形式体系に新しい規則を加えるとき、考慮されるのは計算的な存在論における意味論的な正当化だけです。

対して、他の流儀では、構造規則の許容性・型付けの決定可能性・複数のモデルでの解釈可能性といった大域的な性質を決定的なものとして扱います。

つまり、こういう違いです。

computational type theory では、「この規則は計算の振る舞いとして正しいか」だけを問います。

内包的型理論では、「この規則を加えても型検査は決定可能なままか」「複数の意味論で解釈できるか」を問います。

📌 厳密性を担保した説明をすると……二つの流儀は、片方だけが意味論を重視するという対立ではない

本文では、computational type theory が計算的意味論による正当化を中心に置き、内包的型理論が型検査の決定可能性や複数モデルでの解釈可能性も重視する、と対比しました。

これは、両者の研究者が何を「重要な設計条件」として前面に出すかの違いです。内包的型理論も計算規則の意味を重視しますし、computational type theory の研究でもメタ理論的な性質をまったく考えないわけではありません。

したがって、これは「意味論を大切にする側」と「形式的な性質を大切にする側」の優劣や完全な分業ではありません。同じ型理論を、どの正当化の枠組みから設計・評価するかの重点の違いです。

出典：
J. Sterling, C. Angiuli, D. Gratzer, "Cubical Syntax for Reflection-Free Extensional Equality", arXiv:1904.08562, §1.2. https://arxiv.org/abs/1904.08562

タロウくん：
「証明の対象が型のない生の項」というのは、どういうことですか。

専任講師：
Nuprl 一族では、形式的なシーケントが、型の付いた項（証明）ではなく、型のない生の項 ── realizer と呼びます ── を対象とします。

その結果、証明の過程で、証明から realizer へ移る際に失われる情報を回復するために、型の関数性（functionality）に関する多数の部分目標を繰り返し立てる必要が生じます。

Sterling らの論文は、この点を Nuprl 一族の注目すべき特徴として挙げています。

タロウくん：
functionality という語は、関数（function）と関係がありそうです。
圏論の関手（functor）とは関係ないのですか。

専任講師：
関係ありません。別の概念です。

functionality は、function の性質を表す語で、日本語では関数性と訳します。

ここでは、「等しい値を代入したら、等しい結果になる」という性質を指します。

型 C[x] が x について functional であるとは、t₁ と t₂ が等しいなら C[t₁] と C[t₂] も等しい、ということです。

関数が入力の等しさを出力の等しさに移す、という意味で、関数性です。

圏論の関手（functor）の性質は functoriality と呼ばれ、別の概念です。

関手は、圏から圏への写像で、対象と射を保つものです。functionality とは、綴りも意味も違います。

Nuprl では、証明が型のない生の項 ── realizer ── を対象とするため、「この項は、等しい入力に対して等しい結果を返すか」を、証明の過程で何度も確かめる必要があります。それが、型の関数性に関する部分目標です。

出典：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

先ほどの RedPRL の証明項 (lam [x0 x1 x2] x2) は、型のない生の項です。Lean 4 の証明項 fun (family : Bool → Type) (b : Bool) (pf : family b) => ... には、型が付いています。

タロウくん：
使いやすさはどうですか？

専任講師：
両論があります。併記します。

**否定的な見方。**型検査が決定不能であるため、証明が正しく型付けされているかを型検査器が自動で判定できません。

**肯定的な見方。**Sanders の論文が、次のように述べています。内包的な数学の利点は型検査の決定可能性にあり、欠点は、どんなに自明な等式でも個別に証明しなければならない点にある。

ただし Nuprl の実務は、式が正しく型付けされているかを人手で確かめることが実際には通常たやすい、つまり決定可能な型検査は数学を形式化するうえで必須条件ではない、ということを示唆している。

出典：
S. Sanders, "To be or not to be constructive, that is not the question", arXiv:1704.00462. https://arxiv.org/abs/1704.00462

「決定不能だから使えない」という単純な結論には、帰着しません。

対話篇 ── ふつうのプログラミング言語にも出てくるのか

タロウくん：
何を等しいと見なすかを設計者が決める、という話は、ふつうのプログラミング言語にも出てくるのですか？

専任講師：
出てきます。ただし、型検査が決定不能になるところまでは行きません。

まず、2 つの型を同じ型として扱うかどうかを、どう決めるか、という話です。

Haskell や Rust では、型の同一性は名前で決まります。
data Foo = Foo Int と data Bar = Bar Int は、中身が同じでも別の型 です。これを nominal typing と呼びます。

Go のインタフェースは、名前を要求しません。

あるインタフェースが要求するメソッドをすべて持っていれば、その型は自動的にそのインタフェースを満たします。

TypeScript の型も、名前ではなく形で決まります。
同じフィールドを同じ型で持つ 2 つのオブジェクト型は、名前が違っても互いに代入できます。これを structural typing と呼びます。

次に、Haskell の型クラスと Rust のトレイトは、型の同一性を決める仕組みではありません。

型が満たすべき操作 ── == や show など ── を記述し、その操作を持つ型に制約をかける仕組みです。

Haskell や Rust の型そのものは nominal ですが、型クラスとトレイトは、インタフェースや制約の仕組みとして理解するのが適切です。

📌 厳密性を担保した説明をすると……nominal / structural は型システム全体を単純に二分する言葉ではない

nominal typing と structural typing は、型の同一性や適合性を説明するための重要な対比です。ただし、実際の言語は一方だけでできているとは限りません。

たとえば Go では、名前付き型そのものは区別されますが、インタフェースへの適合は必要なメソッド集合で判断されます。TypeScript にも、構造にもとづく代入可能性に加えて、private / protected メンバーなど名前や宣言上の由来が関わる場面があります。Haskell や Rust にも、型シノニム・newtype・トレイト／型クラスなど、単純な一語では説明し切れない仕組みがあります。

本文では、「名前より構造を重視して適合性を決める場面がある」という直観を伝えるために、この対比を使っています。

タロウくん：
それは、computational type theory が「何を等しいと見なすか」を決めているのと、同じことですか？

専任講師：
似ています。しかし、同じではありません。

computational type theory の外延性は、「計算の振る舞いが同じなら等しい」です。

それに対して、structural typing は、「型の構造が同じなら代入可能」です。

  • 前者は等しさの話で、後者は代入可能性の話です。
  • 前者は計算の実行結果を見ますが、後者はフィールドやメソッドの並びを見ます。

似ているのは、「名前ではなく振る舞いで同じかどうかを決める」という問いの立て方です。答えの中身は違います。

ここを混同して、同一視してしまうと、タロウくんが大学院に進学したあと、誤りの指摘を受けるはずです。

本稿は、両者が別の話であることを明示したうえで、問いの立て方の類似だけを指摘します。

タロウくん：
つまり、何を同じと見なすかを設計者が決める、という問いは、定理証明支援系だけの話ではない、ということですね？

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

ただし、その問いへの答え方は、定理証明支援系とふつうのプログラミング言語とで、異なります。

前者は等しさを問い、後者は代入可能性を問います。

ここまでのまとめ

前編では、5 つの問いに答えました。

（問1）

計算の振る舞い方のどこを境に、同じ型と別の型を分けるか。
境は 2 つあります。

型の中での等しさと、型そのものの等しさです。

型の中での等しさを取り替える仕組みが商型で、redtt で Z/2 を定義して確かめました。等しいと見なす範囲は定理証明支援系ごとに違い、範囲を狭くすれば型検査器が自動で判定でき、範囲を広くすれば数学者が等しいと考えるものを等しいと記述できます。

RedPRL と Lean 4 の証明項を比べ、RedPRL では等しさの証明が計算に痕跡を残さないことを確かめました。

（問2）
研究は 1971 年の Constable の構想に始まり、1979 年に PRL 研究グループが設立され、1984 年に Nuprl が動きました。

動機は、証明からプログラムを取り出すこと、普遍的なプログラミング言語を理論の一部として持つことでした。

**問い 3。**動機は変化しています。2010 年代以降、homotopy type theory の univalence に計算的内容を与えることが加わりました。ただし、計算の振る舞いを土台に置くという方法論は変わっていません。

（問4）
採用した言語と採用しない言語は、等しさの扱い・型検査の決定可能性・証明の対象・設計の優先順位で違います。

使いやすさについては両論があります。

（問5）
何を等しいと見なすかという問いは、ふつうのプログラミング言語にも出てきます。

ただし、computational type theory が問う「2 つの値は等しいか」と、structural typing が問う「2 つの型のあいだで値を代入できるか」は、同じものではありません。

次回記事へ

後編の記事『なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜』 では、次の4つの問い に答えます。

  • 問6： computational type theory を実際に動かせるプログラムは、どれだけあるのか。Dedukti の翻訳器は用意されているのか
  • 問7 : 論理体系と型理論は、一対一の対応ではないのか
  • 問8 : De Morgan cubical type theory で computational type theory を採用した言語はあるのか。無いのは偶然か、理論的な理由があるのか
  • 問9 : De Morgan で computational type theory の言語を作れたら、言語設計理論と数学研究の両方に新しい貢献になるか
    `
    筆者の環境でビルドした RedPRL・redtt・cooltt・cubicaltt の 4 つを、系統ごとに並べます。

📌 用語のミニ解説

📌 本文に登場した用語の、初心者向けミニ解説

computational type theory

型を、あらかじめ決まった集まりとしてではなく、計算の振る舞いが満たす条件として定義する型理論です。Constable らが Nuprl で採った立場に由来します。日本語の定まった訳語は、筆者が調べた範囲では確認できませんでした。

Nuprl（ニュープル）

Cornell の PRL 研究グループが 1984 年から作ってきた証明支援系です。名前は ν（nu、new）＋ PRL（Proof Refinement Logic）です。computational type theory の原型を実装しています。

RedPRL（レッドピーアールエル）

カーネギーメロン大学の Angiuli・Cavallo・Hou (Favonia)・Harper・Sterling が 2016 年から 2018 年にかけて開発した証明支援系です。名前は the People's Refinement Logic です。Cartesian cubical computational type theory を実装しています。

redtt・cooltt

RedPRL の後継です。redtt は 2018 年、cooltt は 2021 年に始まりました。いずれも Cartesian cubical type theory を実装していますが、computational type theory の流儀は採っていません。理由は後編で扱います。

equality reflection（等式反映）

命題として等しいことが証明できれば、判断として等しいと扱ってよい、という規則です。Nuprl と RedPRL が採用しています。型検査が決定不能になる原因です。

この規則を持つ型理論を、外延的型理論と呼ぶことが多いです。ただし、外延的（extensional）という語は、equality reflection よりも広い概念です。関数外延性 ── どの入力にも同じ値を返す 2 つの関数を等しいと見なすこと ── のように、「振る舞いによって対象を同一視する」性質を指す場合もあります。本記事では、Nuprl 系を説明するうえで equality reflection を中心に据えています。

定義的等価性（definitional equality）と命題的等価性（propositional equality）

定義的等価性は、型検査器が計算して判定する等しさです。2 + 2 と 4 が等しい、など。命題的等価性は、証明によって示す等しさです。n + 0 = n を帰納法で証明する、など。内包的型理論では両者は別物で、外延的型理論では一致します。

商型（quotient type）

型 A の要素はそのままで、等しさだけを同値関係 E に取り替えた型 A//E です。Nuprl が持っています。redtt にも quotient がありますが、higher inductive type として定義されており、Nuprl の商型とは仕組みが違います。この違いは後編で扱います。

realizer

Nuprl 一族で、証明の計算的内容にあたる、型のない生の項です。

proof-irrelevant と proof-relevant

proof-irrelevant は、ある命題の証明がすべて等しいと見なされることです。proof-relevant は、証明どうしを区別することです。RedPRL は、proof-irrelevant な厳密な等しさと、proof-relevant なパスが共存する二層の型理論です。

nominal typing と structural typing

nominal typing は、型の同一性を名前で決めます。Haskell や Rust の型がそうです。structural typing は、構造（フィールドやメソッドの並び）で決めます。Go のインタフェース、TypeScript のオブジェクト型がそうです。

Haskell の型クラスや Rust のトレイトは、型の同一性を決める仕組みではなく、型が満たすべき操作を記述する仕組みです。nominal typing の例として挙げるのは不正確です。

📌 コラム：nominal typing と type class / trait は別の概念

nominal typing は、型の同一性や適合性を型名・宣言された型関係にもとづいて扱う考え方です。

Haskell の型クラスや Rust のトレイトは、型そのものの nominal / structural な分類とは別に、型が満たす操作や性質を記述する仕組みです。

したがって「Haskell の型クラス、Rust のトレイト＝nominal typing」と整理するのは不正確です。

Haskell や Rust の型は基本的に nominal ですが、type class / trait はインタフェース・制約の仕組みとして説明するほうが適切です。

実機検証について

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

検証環境

構成要素 版 入手経路
OS Ubuntu 24.04 ─
MLton 20210117 apt
SML/NJ 110.79 apt
OCaml 5.1.1 opam（switch を作成）
RedPRL master（最終コミット 2019 年 11 月） GitHub RedPRL/sml-redprl をソースビルド
redtt master（最終コミット 2022 年 3 月） GitHub RedPRL/redtt をソースビルド
Lean 4 4.22.0-rc4 elan

検証できたこと

  • RedPRL を MLton でビルドし、example/README.prl と example/tutorial.prl の全証明が通った。
  • tutorial.prl の NotNot・RespectEquality・EqualityIrrelevant の証明項を取得した。
  • Lean 4.22.0-rc4 で NotNot と RespectEquality を証明し、#print で証明項を取得した。
  • redtt を OCaml 5.1.1 でビルドし、library/prelude.red の全定義が通った（univalence を含む）。
  • redtt で zmod2.red を書き、Z/2 を商型として定義し、型検査を通した。対照実験として nat の中で 0 と 2 のあいだにパスを作ろうとすると 1 unsolved hole になることを確かめた。

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

  • Nuprl は既定でクラウドで動き、公開サーバーのアカウント申請が必要なため、筆者の環境では実行していない。
  • MetaPRL は OCaml 4.02.3 または 4.05.0 を要求し、筆者の環境の OCaml ではビルドできなかった。
  • redtt のビルドには、次の変更が必要だった。menhir のフラグ --interpret-show-cst を外すこと。Grammar.mly のレコード更新式 9 箇所に ML. の修飾を付けること（OCaml 5.1 でレコードフィールドの曖昧性解消が厳格化されたため）。警告をエラー扱いにしない --profile release でビルドすること。
  • redtt の依存パッケージ astring・rresult は、配布元のサーバーから取得できず、GitHub のミラーに pin した。

cooltt と cubicaltt の環境構築は、後編で記します。

訂正一覧

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

関連記事

本記事の接続先

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

📚 Arend 連載（全 8 本）

出典一覧

0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?