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)

なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜

0
Last updated at Posted at 2026-09-12

thumbnail_picture.jpg

この連載について

本記事は、computational type theory を扱う 全２回（前編・後編）連載記事 の 後編記事 です。

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

前編の記事 は以下です。

この記事について

前編では、computational type theory が、``「先に計算の振る舞いがあり、あとから型が決まる」** という考え方をに立脚する 型理論 であることを紹介しました。

さらに、等しいと見なす範囲 を 広く すると、数学者が等しいと考えるものをそのまま記述できるメリットが得られる反面、型検査器が自動で判定できなくなるという代償を払うことを述べました。

（このトレードオフの関係を、本連載記事の独自の言葉として、「取引」 と呼ぶことにしました）

後編 となる この記事で は、computational type theory を実装した定理証明支援系にはどのような種類があり、手元で実際に動してみたときの挙動を、コードを具体的に見ながら論じていきます。

本記事執筆者は、RedPRL・redtt・cooltt・cubicaltt という 4 つの定理証明支援系を、自分の環境でビルドして動かしました。

なお、Nuprl と MetaPRL は、環境構築に至りませんでした。

📌 中上級者向けコラム ── cubicaltt は定理証明支援系か、型検査器か

本文では、RedPRL・redtt・cooltt・cubicaltt の 4 つを定理証明支援系と呼びました。このうち cubicaltt だけ、1 点注意があります。

cubicaltt の README は、「Cubical Type Theory の実験的な実装」 と名乗り、Cohen らの論文でも type checker と呼ばれています。タクティクや対話的な証明構築の機能は持ちません。

定理を書いて型検査させることはできるので、広い意味では定理証明支援系に含められますが、厳密には型検査器 です。

RedPRL と redtt は、公式に proof assistant と名乗っています。
cooltt は、公式サイトで「the red family of proof assistants」の一員として* 扱われています。

出典：

  • mortberg/cubicaltt（GitHub）. https://github.com/mortberg/cubicaltt
  • C. Cohen, T. Coquand, S. Huber, A. Mörtberg, "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom", TYPES 2015, LIPIcs 69, 2018. DOI: 10.4230/LIPIcs.TYPES.2015.5
  • The RedPRL Development Team, "The red* family of proof assistants". https://redprl.org/

本稿では、1つの事実に光を当てます 。

ホモトピー型理論（HoTT）の区間 $I$ を扱うことができる言語には、Cartesian cubical type theory を採用した言語 と、De Morgan cubical type theory を採用した言語 があります。

Cartesian cubical type theory を採用した言語 には、computational type theory を採用した言語 が 1つある のに対して、De Morgan cubical type theory を採用した言語 には computational type theory を採用した言語 が ひとつも見当たらない のです。

（あくまで2026年9月11日に本記事執筆者が調べた限りの結果です）

pic_1.jpg

本記事は、この事実について、理論的な考察を試みる ものです。
この考察を展開するにあたり、ある一次資料が手がかり となりました。

Sterling・Angiuli・Gratzer が 2019 年に arXiv に投稿した論文です。

この論文は、RedPRL の後継である redtt を作った当事者が、なぜ RedPRL の流儀
── computational type theory の流儀 ── を離れたのかを、自ら述べたものです。

出典：

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

同論文は、FSCD 2019（4th International Conference on Formal Structures for Computation and Deduction）で発表されました。LIPIcs Vol. 131, pp. 31:1-31:25. DOI: 10.4230/LIPIcs.FSCD.2019.31

論文の §1.2 に、次の記述があります。

  • cubical な型理論の高次元の構造は、Nuprl流の型なし推論の適用範囲を大きく狭める。
     
  • cubical でない型理論では β 規則のすべてと η 規則の多くを型なしの書き換えとして扱えるが、higher inductive types と univalence の cubical な扱い において、そのやり方は健全ではない。
     
  • その結果、RedPRL では 多くの β・η 書き換えが、補助的な証明義務を出さなければならない。
     
  • こうした経験と課題 を総合した結果として、redtt が作られた。

この記述が、本記事の考察の出発点 です。

pic_2.jpg

Cartesian の系統で computational type theory を採用した唯一の言語 RedPRL の開発者自身が、cubical では computational type theory の流儀が困難であることを報告しています。

この困難は、区間の演算の違いとは別の、cubical であること自体に由来します。
このことから、De Morgan の系統にも同じ困難があるのではないかと推定されます。

もう 1 つ、この考察を支える一次資料 があります。

出典：
C. Angiuli, R. Harper, T. Wilson, "Computational higher-dimensional type theory", POPL 2017, pp. 680-693. https://dl.acm.org/doi/10.1145/3009837.3009861

この論文は、Cartesian の系統が computational type theory の流儀を採ることを宣言したもの です。

型理論を作る流儀 には、大きく分けて、2つ あります。

1つ は、先に推論規則を書く流儀 です。

推論規則 とは、「$A$ が成り立ち、$B$ が成り立つなら、$A$ かつ $B$ が成り立つ」のように、何から何を導いてよいかを定めた決まりです。

この決まりを紙の上に並べ、その集まりとして型理論を定義 します。

これを、formal type theory の 流儀 と呼びます。
Rocq・Lean 4・Agda は、この流儀で作られています。

もう1つ は、先にプログラミング言語とその計算の仕方を定め、型はプログラムの振る舞いとしてあとから意味づける流儀 です。

前編記事 で扱った 「計算が先、型が後」という順序 です。

これを、computational type theory の 流儀 と呼びます。
Nuprl が、この流儀の 原型 です。
Martin-Löf が型の意味を計算によって説明した meaning explanation を、Nuprl の意味論として実装したものです。

Angiuli・Harper・Wilson の論文は、自分たちの体系が前者ではなく後者である、と述べています。

pic_3.jpg

しかし、De Morgan の系統の原論文 ── Cohen・Coquand・Huber・Mörtberg ── には、「自分たちの体系は computational type theory である」という宣言に相当する記述がありません。

筆者が論文の全文を確認したところ、computational type theory という言葉も、formal type theory という言葉も、本文中には見当たりませんでした。

同論文は、De Morgan cubical type theory という型理論の体系を、推論規則によって定式化し（第 2 節から第 7 節）、その型理論の意味論を cubical set のモデルによって与えています（第 8 節）。

これは formal type theory の作り方 です。

さらに、第 10 節で「De Morgan cubical type theory の正規化と、型検査の決定可能性の証明」を今後の課題として挙げています。

型検査の決定可能性を型理論の設計目標に置くのは、Sterling らが述べた formal type theory の流儀の特徴 です。

pic_4.jpg

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

  • Cartesian の論文は、computational type theory を採用すると明示的に宣言 しています。
     
  • De Morgan の論文は、どちらの流儀を採るかを宣言していませんが、作り方と設計目標は formal type theory の流儀のもの です。

なお、同じ第 10 節に、興味深い記述があります。

この論文の 意味論 の大部分が、Mark Bickford によって Nuprl で形式的に検証された、と述べています。

意味論 とは、型理論の記号や規則が何を表しているかを、数学的な対象に対応づけて説明したもの です。

この論文では、cubical set という数学的な対象を使って、De Morgan cubical type theory の型や項が何を表すかを説明 しています。その説明が正しく組み立てられていることを、Nuprl の中で証明として確かめた、ということです。

De Morgan の系統の意味論が、computational type theory の実装である Nuprl の中で確かめられている、ということです。2つの系統は、この点で交わっています。

出典：C. Cohen, T. Coquand, S. Huber, A. Mörtberg, "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom", TYPES 2015, LIPIcs 69, 2018, 5:1-5:34, §10. DOI: 10.4230/LIPIcs.TYPES.2015.5
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.5

なお、Dagstuhl の URL が 公式の出版元 です。
arXiv 版は 2016 年 11 月投稿で、LIPIcs 版より先に公開されています。

本記事の考察の詳細部分は、対話篇の形式を採用 しました。

なお、本記事は前編を読んでいなくてもお読みいただけるように心がけました。
前編で定義した語は、初出時に説明し直します。

📌 中上級者向けコラム ── 意味論のモデル cubical set とは何か

本記事では、De Morgan cubical type theory の意味論が cubical set のモデルによって与えられている、と述べます。

cubical set とは何かを、Cohen・Coquand・Huber・Mörtberg の論文の第 8.1 節に沿って説明します。

立方体の圏

まず、立方体の圏 $\mathcal{C}$ を定めます。
対象は、名前の有限集合 $I, J, K, \ldots$ です。

名前とは、区間の次元を表す記号 $i, j, k, \ldots$ のことです。
名前が $n$ 個ある集合 $I$ は、$n$ 次元の立方体 $[0,1]^I$ を表します。
名前が 0 個なら点、1 個なら線分、2 個なら正方形、3 個なら立方体です。

射 $\mathrm{Hom}(J, I)$ は、$I$ から $\mathrm{dM}(J)$ への写像です。
ここで $\mathrm{dM}(J)$ は、$J$ の名前から自由に生成された De Morgan 代数です。

つまり、$I$ の各名前に、$J$ の名前を $0$・$1$・反転・最小・最大で組み合わせた式を割り当てます。たとえば、名前 $i$ に $0$ を割り当てれば「$i = 0$ の面をとる」、$1 - j$ を割り当てれば「$j$ の向きを反転する」、$j \wedge k$ を割り当てれば「connection をとる」という操作になります。

cubical set

cubical set とは、この圏 $\mathcal{C}$ 上のプレシーフです。

具体的には、各 $I$ に集合 $\Gamma(I)$ を割り当て、各射 $f : J \to I$ に対して制限写像 $\Gamma(I) \to \Gamma(J)$ を割り当てたものです。

$\Gamma(I)$ の要素は「$I$ 次元の立方体の形をした要素」と読めます。制限写像は、立方体の面をとったり、次元を入れ替えたり、反転したりする操作に対応します。

具体例

位相空間 $X$ から作られる特異 cubical set $S(X)$ が、典型的な例です。

$S(X)(I)$ を、$[0,1]^I$ から $X$ への連続写像の集合と定めます。

$I$ が空なら $X$ の点、名前が 1 個なら $X$ の中の道、2 個なら $X$ の中の正方形、というように、$X$ の中の立方体を集めたものになります。

型理論との対応

De Morgan cubical type theory の型 $A$ は、cubical set の上の族として解釈 されます。

文脈 $\Gamma$ に名前が $n$ 個あるとき、その文脈での型は $n$ 次元の立方体の形をしています。

パス型 $\mathrm{Path}\ A\ a\ b$ は、名前を 1 つ増やした文脈での $A$ の要素で、両端が $a$ と $b$ であるものとして解釈されます。

Cartesian との違い

Cartesian cubical type theory の意味論も cubical set で与えられますが、立方体の圏が違います。

Cartesian の立方体の圏では、射に反転・最小・最大の演算を含めません。

face（面をとる）・degeneracy（次元を増やす）・symmetry（次元を入れ替える）・diagonal（対角線をとる）だけです。

この違いが、区間に認める演算の違いとして、型理論の側に現れます。

出典：

  • C. Cohen, T. Coquand, S. Huber, A. Mörtberg, "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom", TYPES 2015, LIPIcs 69, 2018, 5:1-5:34, §8.1. DOI: 10.4230/LIPIcs.TYPES.2015.5. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.5
  • C. Angiuli, G. Brunerie, T. Coquand, Favonia, R. Harper, D. R. Licata, "Syntax and Models of Cartesian Cubical Type Theory", Mathematical Structures in Computer Science 31(4), 2021. DOI: 10.1017/S0960129521000347

本記事の流れ

対話篇 ── computational type theory を動かせるプログラムは、どれだけあるのか

タロウくん：
先生、Qiitaの記事「ホモトピー型理論（HoTT）の区間 I に、どの数学的代数構造を入れるか ── De Morgan と Cartesian、2 つの立方体型理論から実装言語の地図まで」 を、いま開いています。

  • Cartesian cubical type theory を発案した Harper・Hou (Favonia)・Angiuli・Licata が、いずれもカーネギーメロン大学の研究者か、そこで学位を取った研究者であること。
     
  • カーネギーメロン大学の型理論グループに、Nuprl を軸とする伝統があること。
     
  • そして、Nuprl の型理論の考え方 ── 先に計算の振る舞いを決めておき、あとから「こういう動き方をするものを、この型に住むと呼ぶ」と型を規定する、という計算による意味付けが Harper に受け継がれ、Cartesian cubical type theory につながっていること。

この記事には、そう書かれています。

出典：
ホモトピー型理論（HoTT）の区間 I に、どの数学的代数構造を入れるか ── De Morgan と Cartesian、2 つの立方体型理論から実装言語の地図まで
https://qiita.com/etale_cohomology/items/75aa5395b5f8c03e1bf2

この伝統の中で、computational type theory を実際に動かせるプログラムには、どのようなものがあるのですか？

専任講師：
ここでは、「computational type theory を土台にして作られた、歴史的に重要な実装」を 5 つ挙げます。

ただし、後継の redtt と cooltt は、RedPRL から続く開発系譜に属しますが、RedPRL と同じ意味で computational type theory を採用しているわけではありません。

この違いは後半の記事の中の対話で説明します。

  • Nuprl
    Cornell の PRL プロジェクトが 1984 年から作ってきた証明支援系です。computational type theory の原型を実装しています。
     
  • MetaPRL
    Jason Hickey が博士研究として設計し、実装しました。Nuprl の型理論を実装したうえで、複数の論理を関係づける logical framework の性格を加えています。OCaml で記述されています。
     
  • RedPRL
    カーネギーメロン大学の Angiuli・Cavallo・Hou (Favonia)・Harper・Sterling が 2016 年から 2018 年にかけて開発しました。Standard ML で記述されています。
     
  • redtt
    RedPRL の後継です。2018 年から 2022 年まで開発されました。OCaml で記述されています。
     
  • cooltt
    redtt のさらに後継です。2021 年から 2023 年まで開発されました。OCaml で記述されています。

タロウくん：
5つを並べて比べたいです。

専任講師：
それはいいですね。
表にしますね。

名称 フルスペル 型理論 論理体系 Dedukti の翻訳器
Nuprl ν + PRL（PRL は Proof Refinement Logic） Computational Type Theory。外延的で、equality reflection を持つ 直観主義。述語的（predicative）。宇宙の階層を持つ 確認できず
MetaPRL Meta + PRL Nuprl の Computational Type Theory を実装したうえで、複数の論理を関係づける logical framework の性格を加えたもの 上に載せる対象論理を差し替えられる。Isabelle や Twelf と同系統の枠組み 確認できず
RedPRL the People's Refinement Logic Cartesian cubical computational type theory 直観主義。高次元。外延的で証明無関係な厳密な等しさと、証明関連的なパスが共存する二層の型理論 確認できず
redtt 公式のフルスペルは確認できず（red + tt と読める） Cartesian cubical type theory with extension types 直観主義。高次元。累積的で univalent な宇宙の述語的な階層を持つ。パス型を、より一般的な拡張型（extension type）で定義する 確認できず
cooltt 公式のフルスペルは確認できず（cool + tt と読める） Cartesian cubical type theory 直観主義。高次元。正規化を evaluation で行う（normalization by evaluation） 確認できず

pic_5.jpg

（画像について補足）

画像では MetaPRL を Nuprl から分岐した位置に描いています。

MetaPRL は、Cornell の PRL グループで、Constable の指導のもと Jason Hickey が博士研究として設計し、実装したものです。

Hickey は 2001 年に Cornell で博士号を取り、その後 Caltech に移りました。2003 年の時点では、複数の大学が参加する共同プロジェクトになっています。

画像の下部の Cornell という機関名は、Nuprl と MetaPRL の両方に当てはまります。

ただし、画像では MetaPRL を Nuprl の右上に分岐させて描いているため、Cornell という機関名が MetaPRL にも当てはまることは、画像だけからは読み取りにくくなっています。この補足で補います。

本文で述べたとおり、Jason Hickey が博士研究として設計し、実装したものです。

表に登場する専門用語は、解説が必要そうですね。
説明しますね。

  • 外延的（extensional） とは、2 つの関数がどの入力に対しても同じ値を返すなら等しいと見なす、という立場です。前編記事で述べた「等しいと見なす範囲を広くする」選択にあたります。
     
  • equality reflection（等式反映） とは、命題として等しいことが証明できれば、判断としても等しいと扱ってよい、という規則です。
    この規則を一般に認める体系では、型検査器が常に有限時間で答えを返すとは限らなくなります。
    ここでは、「型検査が決定可能でない」と短く呼びます。分かりやすく言えば、型検査が決定不能になります。

pic_6.jpg

 

  • **述語的（predicative）**とは、ある集まりを定義するときに、その集まり自身を含む全体を参照しない、という制約です。
     
  • 高次元 とは、2つの要素のあいだの等しさそのものを、パス（道）として扱い、パスとパスのあいだの等しさも扱える、ということです。ホモトピー型理論（HoTT）の特徴 です。
     
  • Deduktiとは、筆者の別の連載で扱った、論理体系そのものを記述するための言語です。
     
  • さまざまな定理証明支援系の証明を Dedukti の形式に翻訳し、Dedukti の小さな証明検査器で再検査する、という研究があります。その翻訳を行うプログラムを、翻訳器と呼びます。

タロウくん：
いちばん右の列が、すべて「確認できず」になっています。

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

Dedukti連載の4回目の記事 で、翻訳器の一覧を掲げました。

そこに載っているのは、Rocq・Isabelle・Agda・Lean 4・HOL Light・Matita・PVS の 7 つです。

EuroProofNet が公開している Tools 一覧と、Inria の Deducteam 年次報告 2024 を典拠にしています。

出典：
【Dedukti入門 ④】Dedukti に、産業実績はあるのか
https://qiita.com/etale_cohomology/items/184400900114ca3e4a39

いま表に並べた 5 つは、どれもその一覧に含まれていません。
Dedukti 連載の 4 回目で Idris 2 と Arend について「確認できず」と書いたのと、同じ扱いになります。

タロウくん：
なぜ翻訳器がないのですか？

専任講師：
その理由が記載されている資料は、見つけることができませんでした。

ただ、私自身の推測は、私個人の見解としてお伝えすることはできます。

Dedukti の符号化は、型検査が決定可能な体系を前提 としています。

ところが、Nuprl の系統は 型検査が決定不能 です。

そうすると、証明項をそのまま検査するという Dedukti の仕組みと、噛み合いません。

ただし、これは私個人の見方です。
裏づけを取っていません。

タロウくん：
先生、なぜ、Nuprl の系統は型検査が決定不能なのですか？

少し前に「equality reflection（等式反映）とは、命題として等しいことが証明できれば、判断として等しいと扱ってよい、という規則です。

この規則を持つ型理論では、型検査が決定不能になります」とおっしゃいましたが、命題として等しいことが証明できれば、判断として等しいと扱ってよい、という規則を持つ型理論は、なぜ決定不能になるのかが、腑に落ちません。

専任講師：
順を追って説明します。
3段階に分けて説明しますね。

（第１段階）型検査とは、何を判定することか。

型検査とは、「項 $M$ は型 $A$ を持つか」を判定することです。

判定の途中で、型検査器は「2 つの型 $A$ と $B$ は等しいか」を何度も問います。

たとえば、関数 f の型が A → C で、引数 $x$ の型が B であるとき、f x が型を持つためには、$A$ と $B$ が等しくなければなりません。

型検査器は、$A$ と $B$ が等しいかを判定する必要があります。

（第2段階） 内包的型理論では、その判定が有限の手順で終わる。

Lean 4 や Rocq では、「$A$ と $B$ は等しいか」を判定するとき、型検査器は $A$ と $B$ をそれぞれ計算して、正規形 ── これ以上計算できない形 ── に簡約します。

そして、2つの正規形が同じ形かどうかを、記号の列として比べます。

この手順は、必ず終わります。

Lean 4 や Rocq の型理論は、どんな項も有限回の計算で正規形に到達する、という性質 ── 強正規化性 ── を持つからです。

正規形に到達したら、あとは記号の列を比べるだけです。

これが、定義的等価性（definitional equality） です。
「計算して比べる」だけで判定できる等しさ です。

pic_8.jpg

（第3段階） equality reflection があると、その判定が有限の手順で終わらなくなる。

equality reflection は、「$a$ = $b$ という命題の証明 $p$ があるなら、$a$ と $b$ を判断として等しいと扱ってよい」という規則です。

ここで、鍵となる論点 があります。

規則を適用したあと、証明 $p$ は項の中に残りません。

判断として 等しいと扱う 、というのは、$a$ と $b$ を 「計算して比べる」等しさと同じ扱いにする、ということ です。

証明 $p$ は、規則を適用する根拠として使われ、そのあと捨てられてしまいます。

pic_9.jpg

補足すると、型検査器から見ると、ここで仕事が増えてしまいます。

ふつうは、$A$ と $B$ が等しいかを調べるとき、両方を計算して、最後に同じ形になるかを比べればよい のに対して、 equality reflection があると、計算しただけでは同じ形にならない $A$ と $B$ についても、「$A=B$ である証明がどこかにあれば、同じものとして扱ってよい」 ことになります。

そのため型検査器は、単に計算結果を比べるだけでは済みません。

$A=B$ を示す証明があるかもしれない、という可能性まで考えなければなりません。

pic_11.jpg

すると、型検査器が「$A$ と $B$ は等しいか」を判定しようとしたとき、こういう状況になります。

  • $A$ と $B$ を計算して比べても、正規形が違う。
  • しかし、$A$ と $B$ が 等しいという命題の証明 が、どこかに存在するかもしれない。
  • その証明が存在するなら、equality reflection によって $A$ と $B$ は判断として等しい。

つまり、型検査器は「$A$ = $B$ という命題の証明が存在するか」を、自分で判定しなければなりません。 証明が項の中に残っていないから です。

pic_10.jpg

タロウくん：
証明が存在するかを判定するのが、なぜ終わらないのですか？

専任講師：
証明は、いくらでも長くなりうるから です。

たとえば、2 つの関数 $f$ と $g$ が等しいという命題を考えます。

外延的な等しさ では、「すべての入力 $x$ に対して f $x$ = g $x$」が成り立てば、$f$ と $g$ は等しい。

この命題を証明する ためには、帰納法を使うか、何らかの数学的な議論を組み立てる必要があります。その議論の長さに、上限がないのです。

結果として、型検査器が「$f = g$ の証明が存在するか」を判定しようとすると、あらゆる長さの証明を順に試すことになってしまいます。

pic_12.jpg

証明が存在するなら、いつかは見つかります。

しかし、証明が存在しないとき、型検査器は「存在しない」と結論するために、無限に長い証明まで試さなければなりません。

つまり、終わりません。

これが、決定不能ということの中身です。

  • 証明が存在するときは有限時間で「はい」と答えられる。
  • 証明が存在しないときは、いつまでも答えられない。

pic_7.jpg

QED at Large という論文は、この点を次のように述べています。
外延的型理論では定義的等価性と命題的等価性が一致するが、その結果、証明検査は本質的に決定不能になる。
命題的等価性を使えば、決定不能な問題を記述できるからである、と。

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

タロウくん：
内包的型理論でも、n + 0 = n を証明するときは帰納法を使いますよね。
それは決定不能ではないのですか？

専任講師：
良い問いです。
区別すべき点が、ここにあります。

内包的型理論 では、n + 0 = n の証明を人間が書きます。
帰納法を使って、証明項を組み立てます。

型検査器は、その証明項を受け取って、「この証明項は、本当に n + 0 = n の証明になっているか」を判定します。

この判定は、証明項を計算して型を確かめるだけなので、有限の手順で終わります。

つまり、内包的型理論 では、証明を探すのは人間、証明を検査するのは型検査器、という分担です。

探すのは決定不能でも、検査するのは決定可能です。

pic_13.jpg

ところが、外延的型理論 では、equality reflection によって 証明が項から消えるので、型検査器が証明を探す側に回ることになります。

そして、探すのは決定不能なのです。

pic_14.jpg

こうした状況を鑑みて、と思われるのですが、Nuprl の系統では、型検査器が自動で判定するのではなく、人間がタクティクを書いて証明を組み立てる、という作り になっています。

前編の記事 で見た RedPRL の refine bool/eq/tt というタクティクは、その現れです。

pic_15.jpg

タロウくん：
つまり、証明を項に残すか、捨てるか、の違いなのですね。

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

内包的型理論は、証明を項に残します。

だから型検査器は証明を検査するだけで済み、決定可能です。

その代わり、n + 0 = n のような等しさを使うたびに、証明項の中に書き換えの操作が残ります。
前編で見た Lean 4 の Eq.mpr が、それです。

外延的型理論は、証明を捨てます。

だから証明項は簡潔になり、等しさの証明は計算に痕跡を残しません。
その代わり、型検査器は証明を探さなければならず、決定不能です。

証明を残すか捨てるか。
この 1 つの選択が、型検査の決定可能性と、証明項の簡潔さを、同時に決めています。

pic_16.jpg

対話篇 ── 論理体系と型理論は、一対一の対応ではないのか

タロウくん：
ここまでの話で、ひとつ分かってきたことがあります。

論理体系と型理論は、一対一の対応ではないのですね。

たとえば、古典論理を採る言語は複数あって、それぞれ違う型理論を採用している。
直観主義論理を採る言語も複数あって、それぞれ違う型理論を採用している。
時相論理を採る言語も複数あって、それぞれ違う型理論を採用している。

逆の方向もありそうです。
ある型理論を採用した言語が複数あって、それぞれ違う論理体系を扱っている。

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

一対一ではありません。

ただ、方向によって事情が違います。
順に述べます。

まず、型理論から論理への方向です。

型理論をひとつ決めると、対応する論理がひとつ決まります。

Curry-Howard 対応が、その決まり方を与えます。
命題を型に、証明を項に対応させる見方です。
Dedukti 連載の 3 回目で扱いました。

この方向は、比較的はっきりしています。

次に、論理から型理論への方向です。

こちらは決まりません。
同じ論理を持つ型理論が、いくつもあります。

pic_17.jpg

タロウくん：
直観主義論理の例を挙げてもらえますか？

専任講師：
直観主義論理を持つ型理論だけで、これだけあります。

型理論 主な実装 特徴
単純型付きラムダ計算 ── 直観主義命題論理に対応する
Edinburgh LF（λΠ計算） Twelf 依存型。推論規則を記述するための枠組み
Martin-Löf 型理論 Agda 依存型。帰納族。公理が少ない
Calculus of Inductive Constructions Rocq・Lean 4 依存型。帰納型。宇宙の階層
Computational Type Theory Nuprl・MetaPRL 外延的。equality reflection を持つ
Cartesian cubical type theory RedPRL・redtt・cooltt 高次元。区間に反転と最小・最大を入れない
De Morgan cubical type theory cubicaltt・Agda の --cubical 高次元。区間に De Morgan 代数の構造を持たせる

どれも直観主義論理です。
しかし、型理論はすべて違います。

タロウくん：
古典論理のほうはどうですか？

専任講師：
古典論理も、複数の型理論に分かれます。

型理論 主な実装 特徴
高階論理（Church の単純型理論） HOL Light・HOL4 単純型。検査の核が小さい
高階論理＋型クラス Isabelle/HOL 単純型に型クラスを加えた
高階論理＋述語による部分型 PVS 述語で絞り込んだ部分型を作れる。型検査が決定不能になる
λμ計算 ── 古典論理に対応する型理論として Parigot が提案した

Isabelle/HOL と HOL Light は、どちらも古典的な高階論理を扱います。
しかし、型の仕組みが違います。
Dedukti 連載の 1 回目で、この違いを表にしました。

タロウくん：
時相論理はどうですか。時相論理を型として持つ言語は、あるのですか？

専任講師：
あります。
ただし、事情が少し違います。

時相論理そのものを土台に据えた言語というよりは、時相論理の演算子にあたるものを型として導入した、という形が主です。

中野浩が 2000 年の国際会議 LICS で提案した later modality が、その出発点です。
関数の出力が入力に直ちには依存しないことを型で表す仕組みで、不動点を計算しても安全であることを保証します。
この考え方は guarded recursion と呼ばれます。

出典：
H. Nakano, "A Modality for Recursion", LICS 2000, pp. 255-266. DOI: 10.1109/LICS.2000.855774

later modality は ▷A と書かれます。
▷A は、1 つの時間の刻みのあとに型 $A$ になる項の型、と読みます。

出典：H. B. Grathwohl, "Guarded Recursive Type Theory"（博士論文、オーフス大学）. https://cs.au.dk/~birke/phd-students/GrathwohlHB-thesis.pdf

pic_18.jpg

タロウくん：
それは、時相論理の「次の時点で」にあたるものですか？

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

さらに、線形時相論理（LTL）を Curry-Howard 対応によって反応的プログラミングの言語として使う、という提案もあります。
停止性、活性、公平性といった性質を型として表すことを狙ったものです。

ただし、この 2 つの考え方のあいだには衝突があることも報告されています。
guarded な不動点演算子が、停止性を保証するはずの帰納型に非停止性を持ち込んでしまう、という衝突です。

タロウくん：
実装はあるのですか？

専任講師：
guarded recursion を型理論に組み込んだ体系は複数あります。

Birkedal・Bizjak・Clouston・Grathwohl・Spitters・Vezzosi による Guarded cubical type theory、Sterling と Harper による Guarded Computational Type Theory などです。

出典：J. Sterling, R. Harper, "Guarded Computational Type Theory", LICS 2018, pp. 879-888. DOI: 10.1145/3209108.3209153 ／ arXiv:1804.09098

最後に挙げた Guarded Computational Type Theory は、本記事の主題である computational type theory に、guarded recursion を加えたものです。

タロウくん：
逆の方向も聞かせてください。
同じ型理論の上で、違う論理体系を扱う、という例です。

専任講師：
2通りあります。

1つ目は、公理を足す方法です。

Rocq と Lean 4 は、どちらも Calculus of Inductive Constructions を土台にしています。

この型理論そのものは直観主義です。

しかし、排中律を公理として読み込めば、 その上で古典論理の証明を記述できます。

型理論は変えずに、論理だけを変えたことになります。

pic_19.jpg

2つ目は、logical framework の方法です。

Dedukti連載の3回目 で扱いました。

λΠ計算というひとつの型理論を土台に置き、その土台を用いて一階述語論理・高階論理・様相論理といった論理体系を記述します。

土台の型理論はひとつのまま、記述する論理体系を差し替えます。

Isabelle も同じ作りです。
Isabelle/Pure というメタ論理を土台として、HOL・ZF・FOL を定義します。

pic_20.jpg

タロウくん：
整理すると、こうなりますか？

  • 型理論を決めれば論理は決まる。
  • しかし論理を決めても型理論は決まらない。
  • そのうえ、同じ型理論を土台として違う論理を記述することもできる。

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

そして、その非対称を正面から扱う仕組みが logical framework です。

ひとつの型理論を土台として固定し、その土台を用いて複数の論理体系を記述する。
Dedukti が属している系譜です。

pic_21.jpg

対話篇 ── なぜ De Morgan cubical type theory には computational type theory の実装がないのか

タロウくん：
先生、最初の表に戻らせてください。

表の中で、Cartesian cubical ではない言語があります。

Cartesian ではないほうは、De Morgan cubical computational type theory なのですか？

専任講師：
違います。

表の 5 つのうち、Cartesian ではないのは Nuprl と MetaPRL です。
この 2 つは、そもそも cubical ではありません。

cubical ではない      Nuprl・MetaPRL
Cartesian cubical    RedPRL・redtt・cooltt

Nuprl と MetaPRL は、1984 年から 2000 年代にかけての体系です。

cubical な仕組みは 2010 年代に入ってから、ホモトピー型理論の univalence に計算的な内容を与えるために導入されました。

Nuprl が作られた時代には、まだ存在しません。

タロウくん：
では、De Morgan cubical というのは、どこに出てくるのですか？

専任講師：
別の系統です。

Cohen・Coquand・Huber・Mörtberg による cubical type theory が、その系統にあたります。

cubicaltt という型検査器に実装されました。
Agda の --cubical も、この系統です。

Cartesian と De Morgan の違いのひとつは、区間（interval）に何の演算を認めるかです。

  • De Morgan の系統は、区間に反転と最小・最大を入れ、De Morgan 代数の構造を持たせます。
  • Cartesian の系統は、それらを入れません。

詳細は、以下の記事で取り上げています。

出典：
C. Angiuli, G. Brunerie, T. Coquand, Favonia, R. Harper, D. R. Licata, "Syntax and Models of Cartesian Cubical Type Theory", Mathematical Structures in Computer Science 31(4), 2021. DOI: 10.1017/S0960129521000347
要旨に「based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal)」とあり、De Morgan の系統が持つ connection と reversal を持たないことが明記されています。

整理すると、3つの系統があります。

  • そもそも cubical でない： Nuprl・MetaPRL
  • Cartesian cubical ： RedPRL・redtt・cooltt
  • De Morgan cubical ： cubicaltt・Agda の --cubical

pic_22.jpg

タロウくん：
先生、もう一度、表に戻らせてください。

De Morgan cubical の区間を採用し、さらに computational type theory を採用した言語は、あるのですか？

専任講師：
筆者が調べた公開資料の範囲では、確認できませんでした。

nLab の NuPRL の項が、computational type theory の実装として 4 つを挙げています。
Nuprl、MetaPRL、RedPRL、そして CompLF です。

RedPRL については、computational type theory の cubical な変種のための試験的な証明支援系、と説明されています。RedPRL は Cartesian です。De Morgan の系統の実装は、この一覧に含まれていません。

出典：
nLab, "NuPRL". https://ncatlab.org/nlab/show/NuPRL

タロウくん：
Cartesian と De Morgan の違いは、区間に認める演算の違いだけではないのですか？

専任講師：
違います。

型理論の作り方そのものが違います。

Angiuli・Harper・Wilson が 2017 年の国際会議 POPL で発表した論文が、自分たちの体系を次のように位置づけています。

規則によって定義される formal type theory ではなく、
Martin-Löf の meaning explanation と Nuprl の意味論の意味での computational type theory である、と。

出典：C.
Angiuli, R. Harper, T. Wilson, "Computational higher-dimensional type theory", POPL 2017, pp. 680-693. https://dl.acm.org/doi/10.1145/3009837.3009861

RedPRL の論文は、この違いをさらに明確に述べています。

RedPRL and Nuprl are based on a computation-first methodology in which the judgments of type theory range over programs from a programming language whose syntax and dynamics have already been defined.

（筆者訳）RedPRL と Nuprl は、計算を先に置く方法論にもとづいている。型理論の判断は、構文と動作がすでに定義されたプログラミング言語のプログラムを対象とする。

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

同じ箇所で、対照的な方法についても述べています。

証明項を帰納的に定義し、あとから 簡約の意味論や realizability モデルを備え付ける方法です。

整理します。

ホモトピー型理論で定義される区間 $I$ を扱える言語には、De Morgan cubical type theory を採用した言語と、Cartesian cubical type theory を採用した言語があります。

両者の大きな違いのひとつは、次の点です。

  • De Morgan cubical type theory を採用 した言語は、まず先に型の定義があり、その後に計算がある言語 です。
     
  • Cartesian cubical type theory を採用 した言語のうち computational type theory を採用した言語 は、まず先に計算があり、計算したときの振る舞い方がある条件を満たすかどうかで、ある型の要素かどうかを決める 言語です。

pic_23.jpg

タロウくん：
言い換えると、こうなりますか？

前編で学んできた computational type theory を採用した言語には、ホモトピー型理論を扱える言語と、扱えない言語がある。

そして、computational type theory を採用した言語のうち、ホモトピー型理論を扱える言語は、Cartesian cubical type theory を採用した言語である。

De Morgan cubical type theory を採用した言語には、computational type theory を採用した言語はない。

専任講師：
そのとおりです。
ただし、1点だけ補足が必要です。

Cartesian cubical type theory を採用した言語のすべてが、computational type theory を採用しているわけではありません。

RedPRL の公式サイトは、RedPRL を「computational Cartesian cubical type theory のための Nuprl 流の証明支援系」と説明しています。

一方、後継の redtt については「Cartesian cubical type theory のための証明支援系」とだけ説明しています。

computational という語が外れています。

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

つまり、Cartesian の系統でも、computational type theory を採用しているのは RedPRL だけです。

redtt と cooltt は、Cartesian ではありますが、computational type theory の流儀を離れています。

pic_24.jpg

タロウくん：
なぜ後継が流儀を離れたのですか？

専任講師：
Sterling・Angiuli・Gratzer の論文が、その理由を述べています。

whose higher-dimensional structure significantly reduces the applicability of Nuprl-style untyped reasoning. In particular, whereas it is possible to treat all β-rules and many η-rules in non-cubical type theory as untyped rewrites, such an approach is unsound for the cubical account of higher inductive types and univalence; consequently, in RedPRL many β/η rewrites must emit auxiliary proof obligations.

（筆者訳）その高次元の構造は、Nuprl 流の型なし推論の適用範囲を大きく狭める。特に、cubical でない型理論では β 規則のすべてと η 規則の多くを型なしの書き換えとして扱えるのに対し、higher inductive types と univalence の cubical な扱いにおいて、そのやり方は健全でない。その結果、RedPRL では多くの β・η 書き換えが、補助的な証明義務を出さなければならない。

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

同じ論文は、こうした経験と課題を総合した結果として、Cartesian cubical type theory のための redtt が作られた、と続けています。

タロウくん：
引用の中に「Nuprl 流の型なし推論」「型なしの書き換え」という言葉が出てきました。

型なしの書き換え とは、何ですか？

専任講師：
項の型を確かめずに、項の形だけを見て、書き換え規則を適用することです。

具体的に述べます。
ラムダ計算には、 $β$ 規則 という 書き換え規則 があります。

(λx. M) N  ↦  M[N/x]

関数 λx. M に引数 N を渡した式は、$M$ の中の $x$ を N で置き換えた式に書き換えられる、という規則です。

この規則を適用するとき、λx. M の型が何であるか、N の型が何であるかを、確かめる必要はありません。

式の形が (λx. M) N になっていれば、型を見ずに書き換えられます。

これが、型なしの書き換え です。

$η$ 規則の多くも同様 です。

関数については λx. f $x$ ↦ f、対については (π₁ p, π₂ p) ↦ p という書き換えがあります。

cubical でない型理論では、$β$ 規則のすべてと $η$ 規則の多くを、型を見ずに適用できます。
Sterling らの論文は all β-rules and many η-rules と述べています。

すべての $η$ 規則ではありません。

pic_25.jpg

タロウくん：
なぜ Nuprl は、型を見ずに書き換えるのですか？

専任講師：
先に計算があり、あとから型が決まる、という順序だから です。

RedPRL の論文が述べているとおり、Nuprl と RedPRL では、型理論の判断 が対象とするのは、構文と動作がすでに定義されたプログラミング言語のプログラム です。

プログラムの動作 ── どう計算が進むか ── は、型が決まる前に定義されています。
$β$ 規則や $η$ 規則は、その動作の一部です。

したがって、Nuprl では、項の型を確かめる前に、項を計算することができるのです。

pic_26.jpg

具体例を挙げます。
(λx. $x$ + 1) 2 という項が 自然数の型に属するか を確かめたいとします。

Lean 4 や Rocq では、

  • まず λx. $x$ + 1 が Nat → Nat という型を持つこと
  • 2 が Nat を持つこと を確かめてから、
  • 関数適用の規則から (λx. $x$ + 1) 2 が Nat を持つと導きます。

型の情報を組み合わせて、結論を出します。

Nuprl では、

  • まず (λx. $x$ + 1) 2 を計算します。
  • $β$ 規則で 2 + 1 になり、さらに計算して 3 になります。
  • 3 は自然数です。
  • だから、もとの項は 自然数の型に属します。

型の情報を組み合わせるのではなく、計算の結果を見て結論を出します。

Sterling らの論文は、Nuprl がこの 「計算して結果を見る」推論に大きく依存している、と述べています。

この推論の正確な仕組みと、その代償については、中上級者向けのコラムで扱います。

タロウくん：
つまり、Nuprl は 「計算して結果を見る」を、型を確かめる代わりに使っている、ということ ですね。

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

これに対して、Lean 4 や Rocq では、項は 最初から型が付いた状態で構成 されます。
書き換えも、型の付いた項に対して行われます。

📌 中上級者向けコラム ── pointwise functionality と dependent cut

本文で「計算して結果を見る推論」と述べたものの正確な名前は、pointwise functionality を経由した型なしの計算的推論です。Sterling らの論文の記述を引用します。

To mitigate the corresponding blow-up in proof size, Nuprl relies heavily on untyped computational reasoning via pointwise functionality, a non-standard semantics for dependently typed sequents which has some surprising consequences, such as refuting the principle of dependent cut [42].

（筆者訳）それに伴う証明の大きさの膨張を抑えるために、Nuprl は pointwise functionality を経由した型なしの計算的推論に大きく依存している。pointwise functionality は依存型のシーケントに対する非標準的な意味論であり、dependent cut の原理を反証するといった、驚くべき帰結を持つ。

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

この一文には、3 つの語が含まれています。順に扱います。

1. 型なしの計算的推論

項を実際に計算して、その結果の振る舞いから性質を導く推論です。本文で (λx. x + 1) 2 の例を挙げました。

2. pointwise functionality

Nuprl のシーケント x₁ : H₁; x₂ : H₂[x₁]; …; xₙ : Hₙ[x₁; …; xₙ₋₁] ⊢ C[x₁; …; xₙ] が「真である」とはどういうことか、を定める方式のひとつです。Kopylov の博士論文の §2.2 に、原典の記述があります。

Roughly speaking the sequent (2.1) is true when C[x₁; …; xₙ] is true (i.e. nonempty) for all xᵢ's from Hᵢ[x₁; …; xᵢ₋₁]. The formal definition of the truth of the sequent deals with functionality. Basically, we say that a type C[x] is functional over x : T if t₁ = t₂ ∈ T implies C[t₁] = C[t₂].

（筆者訳）おおまかに言えば、シーケント (2.1) が真であるとは、Hᵢ[x₁; …; xᵢ₋₁] に属するすべての xᵢ について C[x₁; …; xₙ] が真である（すなわち空でない）ことである。シーケントの真理の形式的な定義は、functionality を扱う。基本的には、型 C[x] が x : T について functional であるとは、t₁ = t₂ ∈ T ならば C[t₁] = C[t₂] であることをいう。

functionality とは、等しい値を代入したら等しい結果になる、という性質です。ここまでは、どの型理論でも共通です。違いは、この性質をどの範囲で要求するかにあります。

There are different nonequivalent approaches to define what it means for a sequent to be true. Originally Martin-Löf required that any hypothesis Hᵢ must be functional over previous hypotheses and the conclusion must be functional over all hypotheses.

The type theory implemented in NuPRL uses a weaker requirement that allows one to formulate stronger rules (for example a rule for induction over natural numbers). This approach is called pointwise functionality and was discovered by Stuart Allen in [3].

Another version of functionality was used in [31]. Aleksey Nogin later independently rediscovered it and called it pairwise functionality.

（筆者訳）シーケントが真であることの意味を定めるには、互いに同値でない複数の方式がある。もともと Martin-Löf は、どの仮説 Hᵢ も前の仮説について functional であり、結論がすべての仮説について functional であることを要求した。

NuPRL に実装された型理論は、より弱い要求を用いる。この弱い要求によって、より強い規則（たとえば自然数の帰納法の規則）を定式化できる。この方式は pointwise functionality と呼ばれ、Stuart Allen が [3] で発見した。

functionality の別の版が [31] で用いられた。Aleksey Nogin が後に独立にそれを再発見し、pairwise functionality と名づけた。

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

Kopylov の論文は、2 つの方式の形式的な定義を与えています。Γ を仮説の列、t⃗ を代入する項の列とすると、次のとおりです。

pointwise functionality（§2.2.1）：

∀t⃗. ( t⃗ ∈ Γ[t⃗] ∧ ∀t⃗'. (t⃗ = t⃗' ∈ Γ[t⃗] ⇒ Γ[t⃗] = Γ[t⃗']) )
     ⇒ ∀t⃗'. (t⃗ = t⃗' ∈ Γ[t⃗] ⇒ C[t⃗] ∧ C[t⃗] = C[t⃗'])

pairwise functionality（§2.2.2）：

∀t⃗. ∀t⃗'. ( Γ[t⃗] = Γ[t⃗'] ∧ t⃗ = t⃗' ∈ Γ[t⃗] ) ⇒ ( C[t⃗] ∧ C[t⃗] = C[t⃗'] )

2 つの定義の違いは、量化の順序と、前提の置き方にあります。pairwise は、任意の 2 つの代入 t⃗ と t⃗' の対について、仮説が等しく代入が等しければ結論が等しい、と一度に要求します。pointwise は、まず 1 つの代入 t⃗ を固定し、その t⃗ で仮説が正しく型付けされ、かつ t⃗ と等しい任意の t⃗' について仮説が等しいことを前提としたうえで、その t⃗' について結論が等しい、と要求します。「1 点ずつ」（pointwise）とは、この「t⃗ を 1 つ固定してから」という構造を指しています。

pointwise の前提のほうが強い（仮説の functionality を、固定した t⃗ について先に仮定できる）ので、結論を導く際の負担が軽くなります。これが「より弱い要求」であり、「より強い規則を定式化できる」理由です。

3. dependent cut

Sterling らが dependent cut と呼ぶ規則は、Kopylov の論文では Let 規則と呼ばれています。cut 規則の一形態です。

The most important rule that holds only in pairwise functionality is the Let rule (a form of the Cut rule):

Γ; x : A; Δ[x] ⊢ C[x]        Γ ⊢ a ∈ A
─────────────────────────────────────  (Let x = a ∈ A)
           Γ; Δ[a] ⊢ C[a]

In pointwise functionality this rule is invalid, only a weaker form of this rule (when Δ does not depend on x) is valid:

Γ; x : A; Δ ⊢ C[x]        Γ ⊢ a ∈ A
───────────────────────────────────
           Γ; Δ ⊢ C[a]

（筆者訳）pairwise functionality でのみ成り立つ最も重要な規則は、Let 規則（cut 規則の一形態）である。pointwise functionality ではこの規則は成り立たず、より弱い形（Δ が x に依存しない場合）だけが成り立つ。

出典：同上、§2.2.3

cut 規則とは、「A が成り立つ」という証明と「A を仮定すれば B が成り立つ」という証明を組み合わせて「B が成り立つ」を導く規則です。Let 規則は、依存型の設定でこれを行います。「a は A の要素である」という証明と、「x が A の要素だと仮定すれば、Δ[x] のもとで C[x] が成り立つ」という証明から、x に a を代入して「Δ[a] のもとで C[a] が成り立つ」を導きます。

pointwise では、Δ が x に依存しない場合に限って成り立ちます。x に a を代入したあとの仮説 Δ が、x を含んでいてはならない、ということです。

Kopylov の論文は、この規則が pointwise で成り立たないことを述べていますが、その理由を説明していません。筆者も、定義から理由を再構成することは控えます。

4. 逆に pointwise でしか成り立たない規則

Kopylov の論文は、pointwise で成り立ち pairwise で成り立たない規則も挙げています。

On the other hand, the following rule is true in pointwise, but not in pairwise:

Γ₁; t : T; Γ₂[t]; x : A[t]; Δ[x; t] ⊢ t = t' ∈ T
Γ₁; t : T; Γ₂[t]; x : A[t']; Δ[x; t] ⊢ C[t; x]
────────────────────────────────────────────────  (PointwiseSubstitute)
Γ₁; t : T; Γ₂[t]; x : A[t]; Δ[x; t] ⊢ C[t; x]

This rule states that we can replace a variable declared as t : T by a term t' if we know that t = t' ∈ T.

（筆者訳）一方、次の規則は pointwise では成り立つが pairwise では成り立たない。この規則は、t = t' ∈ T が分かっているなら、t : T と宣言された変数を項 t' で置き換えられる、と述べている。

出典：同上、§2.2.3

つまり、pointwise と pairwise は、どちらかが他方より優れているのではなく、成り立つ規則の集合が違います。Nuprl は、自然数の帰納法のような強い規則を使えるようにするために pointwise を選び、その代わりに Let 規則の一般形を手放しました。

5. なぜこれが cubical で問題になるか

Sterling らの論文は、Nuprl 流の型なし推論の適用範囲が、cubical な型理論の高次元の構造によって大きく狭められる、と述べています。その具体的な現れが、本文で扱う「型なしの書き換えが健全でなくなる」という事態です。pointwise functionality を経由した型なしの計算的推論は、cubical でない設定では証明の膨張を抑える有効な手段でしたが、cubical では higher inductive types と univalence の扱いにおいて、その手段が使えなくなります。

タロウくん：
では、「型なしの書き換えが健全でなくなる」 とは、どういうことですか？

専任講師：
書き換えの前後で、項の意味が保たれなくなる、ということ です。

健全性（soundness） とは、規則を適用した結果が、意味論的に正しいこと です。

書き換え規則の場合、書き換える前の項と、書き換えたあとの項が、同じ意味 ── 同じ振る舞い ── を持つなら、その書き換えは健全です。

pic_28.jpg

cubical でない型理論 では、$β$ 規則のすべてと $η$ 規則の多くの書き換えは、項の型によらず意味を保ちます。

だから、型を見ずに書き換えても健全です。

cubical な型理論では、事情が変わります。

higher inductive types と univalence を扱うとき、項の意味が、その項がどの型に属するかに依存する部分が出てきます。

pic_29.jpg

タロウくん：
型に依存する、というのは、たとえばどういう場面ですか？

専任講師：
univalence の場面を挙げます。

筆者の理解にもとづく説明です。

univalence では、型 $A$ と型 $B$ が同値であれば、$A$ と $B$ のあいだにパス ── 道 ── があると扱います。

そして、そのパスに沿って、$A$ の要素を $B$ の要素に変換する操作があります。
Cartesian cubical type theory では、この操作を coe と呼びます。

この変換の中身は、$A$ と $B$ のあいだの 同値の中身によって決まります。

  • 同値が「$A$ の要素を 2 倍する」というものなら、変換は 2 倍する操作になります。
  • 同値が「$A$ の要素を反転する」というものなら、変換は反転する操作になります。

補足します。

この記事の執筆者がホモトピー型理論HoTTについて解説した複数の記事で述べたように、2つの対象Aと$B$のあいだには、両者が等しいことの理由、根拠が複数ある場合、異なる"等しさの理由、根拠"を互いに混同せずに区別して取り扱える数学理論と解説しました。

そのため、どの"等しさの理由、根拠"をつかって計算するのかによって、計算結果が変わることが、HoTTでは出てくる のです。

つまり、coe を含む項をどう書き換えるかは、その項がどの型に属し、どの同値を使っているかに依存します。

型を見ずに書き換えると、どの同値を使うべきかが分かりません。

その結果、書き換えの結果が、意味論的に正しくならないことがあります。

pic_30.jpg

Sterling らの論文は、この状況を 「higher inductive types と univalence の cubical な扱いにおいて、そのやり方は健全でない」 と述べています。

同じ論文の別の箇所に、この困難 を具体的に述べた記述があります。

関数型 のあいだの 等式 $q$ に沿った coercion を簡約するには、$q$ を 「引数の型の等式」と「戻り値の型の等式」の2つに分解する必要 があります。

しかし、$q$ が 変数として与えられている とき、その2つの等式の証明を何もないところから思いつくか、あるいは存在しないと判定するかしなければならず、それは不可能な仕事である、と論文は述べています。

coercion を簡約するには、等式の中身 ── 型の構造 ── を見る必要がある、ということです。

pic_31.jpg

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

タロウくん：
それで、RedPRL は何をしたのですか？

専任講師：
書き換えのたびに、「この書き換えは、この型において正しいか」を確かめる証明義務を出すようにしました。

Sterling らの論文が「RedPRL では 多くの β・η 書き換えが、補助的な証明義務を出さなければならない 」と述べているのは、このことです。

型なしで書き換える という Nuprl 流の利点が、cubical では使えなくなり、代わりに型を確かめる手間 が加わりました。

その手間を抱えたまま RedPRL は作られ、その経験を踏まえて、後継の redtt は型なしの書き換えという流儀そのものを離れました。

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

pic_27.jpg

タロウくん：
De Morgan cubical type theory を採用した言語に、computational type theory を採用した言語がないのは、偶然ですか。それとも、理論的な理由があるのですか？

専任講師：
理論的な理由があります。

ただし、「De Morgan では不可能である」と述べた資料は見つけていません。

分かっているのは、次のことです。

Sterling らの論文が述べているとおり、cubical な型理論の高次元の構造は、Nuprl流の型なし推論 を 大きく制約 します。

higher inductive types と univalence を cubical に扱うとき、型なしの書き換えは健全でなくなります。

この制約 は、Cartesian と De Morgan のどちらにも共通 します。
区間の演算の違いとは別の、cubical であること自体に由来する制約 です。

pic_32.jpg

Cartesianの系統 の RedPRL は、この制約を抱えながら computational type theory の流儀で作られました。

pic_33.jpg

タロウくん：
どうやって、健全でなくなるという制約を抱えながら、RedPRL は computational type theory の流儀に従うことができたのですか？

専任講師：
書き換えの健全性を、書き換え規則の側ではなく、証明義務の側で確保する、という方法を取り入れたからです。

Sterling らの論文の記述に戻ります。

consequently, in RedPRL many β/η rewrites must emit auxiliary proof obligations.

（筆者訳）その結果、RedPRL では多くの β・η 書き換えが、補助的な証明義務を出さなければならない。

cubicalでないNuprl では、$β$ 規則や $η$ 規則の書き換えは、どの型に属する項に対しても意味を保ちます 。だから、型を見ずに書き換えてよい。書き換え規則そのものが健全性を保証 しています。

ところが、cubicalなRedPRL では、この保証が成り立ちません。
同じ書き換えでも、項がどの型に属するかによって、意味が保たれる場合と保たれない場合があります。

そこで RedPRL は、書き換えを行うたびに、「この書き換えは、この型において意味を保つか」という問いを、証明義務として別に立てます。

書き換え自体は型を見ずに行う。

しかし、その書き換えが健全であることの証明を、利用者が ── あるいは自動化されたタクティクが ── 別途与える。

健全性の保証を、規則から証明義務へ移した、ということです。

pic_34.jpg

ただし、いま述べた「書き換え自体は型を見ずに行い、健全性の証明を別途与える」という説明は、Sterling らの「補助的な証明義務を出す」という記述を、筆者が読み解いたもの です。

RedPRL の実装が正確にそのとおりに動いているかは、ソースコードで確かめたわけではありません。
論文の記述から筆者が理解した範囲での説明です。

タロウくん：
それで computational type theory の流儀は保たれているのですか？

専任講師：
保たれています。

computational type theory の流儀とは、先に型なしのプログラムとその計算の仕方があり、型はプログラムの振る舞いとしてあとから意味づける、という順序です。

RedPRL の論文は、型を「型なしプログラムの評価の振る舞いを指定する部分同値関係」として捉える、と述べています。

この順序は変わっていません。

変わったのは、書き換えの扱い です。

Nuprl では「型なしで書き換える。健全性は規則が保証する」でした。

RedPRL では 「型なしで書き換える。健全性は証明義務で確認する」 になりました。
前半は同じで、後半が違います。

ただし、この方法には代償があります。

書き換えのたびに証明義務が出るので、証明が膨らみます。

Sterling らの論文が「経験と課題を総合した結果として redtt が作られた」と述べているのは、この代償が大きかったから だと考えられます。

redtt は、型なしの書き換えという前半も手放して 、最初から型の付いた項を扱う流儀に移りました。

出典：

  • J. Sterling, C. Angiuli, D. Gratzer, "Cubical Syntax for Reflection-Free Extensional Equality", arXiv:1904.08562, §1.2. https://arxiv.org/abs/1904.08562
  • 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

pic_36.jpg

そして、その経験 を踏まえて、後継の redtt は computational type theory の流儀から離れました。

De Morgan の系統は、最初から formal type theory の流儀で作られています。
Cohen・Coquand・Huber・Mörtberg の論文は、規則によって型理論を定義 し、cubicaltt に実装しました。

出典：
C. Cohen, T. Coquand, S. Huber, A. Mörtberg, "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom", TYPES 2015, LIPIcs 69, 2018, 5:1-5:34. DOI: 10.4230/LIPIcs.TYPES.2015.5

したがって、筆者の整理はこうなります。

De Morgan の系統に computational type theory の実装がないのは、偶然ではありません。

cubical な型理論ではNuprl流の型なし推論が困難であることが、Cartesian の系統の経験で報告されています。

De Morgan の系統でその困難に挑んだ例は、筆者が調べた範囲では確認できませんでした。

タロウくん：
そういういきさつ（経緯）があったのですね。勉強になりました。

Cartesian cubical type theory の場合、「型なしで書き換える。健全性は証明義務で確認する」 という設計方針を貫こうとした結果、証明の規模が膨れ上がってしまったということですが、もし仮に、将来だれかが、De Morgan cubical type theory で、この設計方針を貫こうとチャレンジした場合は、Cartesian cubical type theory の場合（RedPRL の場合）よりも、直面するであろう困難はもっと大きくなってしまうと予想されているのでしょうか？

たとえば、De Morgan の区間 $I$ は、Cartesian の区間 $I$ よりも、豊かで複雑な代数構造を備えていることを、過去の対話（過去の記事）で先生との対話で学んだことを念頭においています。

専任講師：
その予想を述べた資料を、筆者は見つけていません。
ですから、答えは筆者の見当になります。

あくまでも私個人の見立てとしては、困難が大きくなる面と、小さくなる面の、両方がありえます。
一概には言えません。

（困難が大きくなると予想される理由）

De Morgan の区間は、反転・最小・最大の演算を持ちます。
Cartesian の区間は持ちません。

その結果、型なしの書き換えで健全性を保つべき箇所は、区間の演算の種類に応じて増えるであろうと考えられます。

  • 反転を含む項の書き換え
  • 最小や最大を含む項の書き換え

それぞれについて「この型で意味を保つか」を確認する必要が出ます。

証明義務の種類が増える ので、RedPRL より困難が大きくなると考えられます。

（困難が小さくなると予想される理由）

De Morgan の演算は、構成を簡単にする側面も持っています。

Cohen らの論文は、connection ── 最小と最大による演算 ── があるおかげで、composition から Kan filling を定義できる、と述べています。

Cartesian では、connection がないので、filling を別に用意する必要があります。

つまり、De Morgan では、Cartesian で複雑になる構成の一部が、区間の演算によって簡潔に書けます。構成が簡潔なら、それに伴う証明義務も減る可能性があります。

出典：
C. Cohen, T. Coquand, S. Huber, A. Mörtberg, "Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom", TYPES 2015, LIPIcs 69, 2018, §4.4. DOI: 10.4230/LIPIcs.TYPES.2015.5

（総合すると・・・）

区間の演算が増えることは、証明義務の種類を増やす方向にも、構成を簡潔にして証明義務を減らす方向にも働きます。

どちらが勝るかは、実際に試みた例がないので分かりません。

本記事の末尾の対話で、この方向の研究が貢献になりうるかどうかを扱います。

いま述べた「どちらが勝つか」が、その貢献の中身のひとつになります。試みてみなければ分からない、というのが、いまの正確な答えです。

タロウくん：
わかりました。まだまだ未解明の部分があるということですね！
ここは、研究テーマとして興味深い領域です。

ところで、ここまで、formal type theory の流儀 ── 先に推論規則を書き、その規則で型理論を定義する ── と、computational type theory の流儀 ── 先にプログラムがあり、型はプログラムの振る舞いとしてあとから意味づける ── の違いを学びました。

前編で、商型 ── 型の要素はそのままに、等しさの取り決めだけを取り替えて作る型 ── を redtt で動かしました。redtt は Cartesian ですが、computational type theory の流儀を離れた言語です。

そうすると、redtt の商型は、formal type theory の流儀で作られた商型で、Nuprl の商型は、computational type theory の流儀で作られた商型、ということになります。この 2 つの商型は、作り方が違うのですか？

専任講師：
そのとおりです。作り方が違います。

Nuprl の商型 A//E は、要素は $A$ のまま、等しさを $E$ に取り替えます。
等しさの証明は計算的内容を持ちません。

この先の議論をする前に、まず最初に、前編の商型の議論を振り返っておきましょう。

商型 とは、型の要素はそのままに、等しさの取り決めだけを別の同値関係に取り替えて作る型 でした。

前編の記事では、自然数の型の等しさを「3 で割った余りが同じ」に取り替えて、3 を法とする整数の型を redtt で作り、0 と 3 が等しくなることを確かめました。

以上が、前編の記事で論じたことのおさらいでした。

議論に戻るとすると、redtt の商型と、Nuprl の商型は、作り方が違います。

Nuprl の商型 A//E は、要素は $A$ のまま、等しさを $E$ に取り替えます。等しさの証明は計算的内容を持ちません、と先ほどお伝えしました。

redtt の商型は、higher inductive type として定義されています。
redtt の data/quotient.red は次のとおりです。

data (A : type) (R : A → A → type) ⊢ quotient where
| pt (a : A)
| gl (a b : A) (p : R a b) (i : 𝕀) [
  | i=0 → pt a
  | i=1 → pt b
  ]

構成子 gl が、関係 $R$ の証明を受け取って、区間 $I$ の上のパスを作ります。

これは「等しさを取り替える」というより「パスを足す」操作です。
パスは計算的内容を持ちます。

同じ商型という名前ですが、

  • Nuprl は等しさを取り替える
  • redtt はパスを足す

この違い が、computational type theory の流儀と formal type theory の流儀の違いの、具体的な現れ です。

pic_35.jpg

タロウくん：
ここまでの議論を整理したいと思います。

言語を3つのグループに分けて、一覧表にしていただけますか？

  • ホモトピー型理論で定義される区間 $I$ を扱えない言語
  • Cartesian cubical type theory で区間 $I$ を扱える言語
  • De Morgan cubical type theory で区間 $I$ を扱える言語

の3類型です。

各言語が computational type theory を採用しているか、していないかも入れてください。

専任講師：
表にします。
ひとつも該当する言語がない欄は「該当なし」と書きます。

グループ computational type theory を採用 computational type theory を採用しない
区間 $I$ を扱えない Nuprl（Lisp 系）
MetaPRL（OCaml）		 Rocq（OCaml。CIC）
Lean 4（C++ と Lean。CIC の変種）
Agda（Haskell。Martin-Löf 型理論）
Twelf（Standard ML。Edinburgh LF）
Cartesian cubical type theory で区間 $I$ を扱える RedPRL（Standard ML） redtt（OCaml）
cooltt（OCaml）
yacctt（Haskell）
De Morgan cubical type theory で区間 $I$ を扱える 該当なし cubicaltt（Haskell）
Agda の --cubical（Haskell）

**筆者の環境で実行したもの。**RedPRL・redtt・cooltt・cubicaltt の 4 つは、筆者の環境でビルドし、実行しました。詳細は記事末尾の「実機検証について」に記します。

**yacctt について。**Yet Another Cartesian Cubical Type Theory の略で、cubicaltt を Cartesian に作り直したものです。筆者の環境では実行していません。

**CompLF について。**nLab が computational type theory の実装として挙げていますが、試験的な設計とされており、詳細を確認できていません。表には含めていません。

**Isabelle/HOL について。**型理論ではなく高階論理を土台とするため、表には含めていません。

対話篇 ── De Morgan で computational type theory の言語を作れたら、新しい貢献になるか

タロウくん：
ここまでの議論を整理すると、まだ研究の余地が残されている未踏の領野が見えてきたように思います。

もし僕が将来、De Morgan cubical type theory を実装し、ホモトピー型理論の区間 $I$ を計算できて、さらに computational type theory も採用した言語を設計し、実装できたとしたら、プログラミング言語設計理論の研究と、数学研究の両方に、今までなかった新しい貢献ができそうでしょうか？

専任講師：
もしそれができたとしたら、貢献になりえると思いますよ。

ただし、貢献の中身は「作れた」という事実だけでは足りません。
何を示せたかが問われます。

順に述べます。

まず、何が困難かは、すでに分かっています。

Sterling らの論文が報告したとおり、cubical な型理論では、higher inductive types と univalence に対して、Nuprl 流の型なしの書き換えが健全でなくなります。
RedPRL は、多くの書き換えに補助的な証明義務を付けることで、この困難を抱えたまま作られました。
後継の redtt は、流儀そのものを離れました。

De Morgan の系統で computational type theory を採用した言語を作るなら、同じ困難に正面から当たります。
De Morgan の区間は、Cartesian の区間に加えて、反転と最小・最大の演算を持ちます。
演算が増えるぶん、型なしの書き換えで健全性を保つべき箇所も増えます。

したがって、貢献の核心はここになります。

その困難を、De Morgan の設定でどう克服したか。
RedPRL が証明義務で補ったところを、別の設計で解消できたのか。
あるいは解消できず、別の代償を払ったのか。
それを示せれば、貢献です。

そして、もし解消できたなら、その設計は「なぜ Cartesian の系統の後継が流儀を離れなければならなかったのか」への答えにもなります。
Cartesian の系統で解けなかった問題が De Morgan の系統で解けたのか、それとも解けなかったことに共通の理由があるのか。
どちらの結果であっても、cubical な型理論の理解を一歩進めます。

数学研究への貢献は、意味論にあります。

De Morgan の区間は、Cartesian より多くの定義的等式を持ちます。
反転と最小・最大の演算が加わるからです。

その等式を、規則として記述するのではなく、型なしプログラムの評価の振る舞いから導けることを示せれば、cubical な型理論の意味論の研究になります。

Angiuli らが Cartesian で行った仕事の、De Morgan 版にあたります。

Angiuli らの仕事とは、次のものです。

Angiuli・Harper・Wilson は、2017 年の国際会議 POPL で、Cartesian cubical の設定で computational type theory の意味論を構築しました。

型なしプログラムに決定的な操作的意味論 ── Kan 条件を実現する操作を含む ── を与え、型をそのプログラムの評価の振る舞いを指定する部分同値関係として定義しました。

主な成果は、 canonicity 定理です。
bool 型の閉じた項は、必ず true か false に評価される、という定理です。

この定理によって、高次元の依存型理論に計算的な解釈を与えた最初の仕事になりました。

翌年、Angiuli・Hou (Favonia)・Harper は、この意味論をパスと厳密な等しさの両方を持つ体系に拡張し、RedPRL の基礎としました。

De Morgan の区間で同じことを行うなら、反転・最小・最大を含む項に操作的意味論を与え、それらの演算が満たすべき等式が評価の振る舞いから導かれることを示し、canonicity を証明することになります。

出典：

  • C. Angiuli, R. Harper, T. Wilson, "Computational higher-dimensional type theory", POPL 2017, pp. 680-693. https://dl.acm.org/doi/10.1145/3009837.3009861
  • C. Angiuli, K.-B. Hou (Favonia), R. Harper, "Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities", CSL 2018, LIPIcs 119, pp. 6:1-6:17. DOI: 10.4230/LIPIcs.CSL.2018.6

プログラミング言語設計への貢献は、方法論にあります。

RedPRL の論文は、計算を先に置く方法論の利点として、例外や非停止性といった計算機科学の機能を組み込みやすいことを挙げています。理論がプログラミング言語から直接立ち上がるからです。

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

その利点を、De Morgan cubical の設定で実際に示せれば、言語設計の研究になります。
たとえば、ホモトピー型理論を扱いながら例外を持つ言語が作れるのか。
それは formal type theory の流儀では作りにくいのか。
そうした問いに、実装で答えることになります。

ひとつ、注意しておきます。

筆者は、この方向の研究がすでに誰かによって着手されているかどうかを、確認できていません。
本記事の執筆時点で公開資料に見当たらない、というだけです。
着手するなら、最初に先行研究を洗い直すことが要ります。

タロウくん：
つまり、作れるかどうかより、なぜ今まで無かったのかを解き明かせるかどうか、ということですね。

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

ここまでのまとめ

後編では、4 つの問いに答えました。

（問6）
computational type theory を実際に動かせるプログラムは、Nuprl・MetaPRL・RedPRL・redtt・cooltt の 5 つです。いずれも Dedukti の翻訳器は確認できませんでした。

（問7）
論理体系と型理論は、一対一の対応ではありません。型理論を決めれば論理は決まりますが、論理を決めても型理論は決まりません。直観主義論理を持つ型理論は 7 つ以上あり、古典論理を持つ型理論は 4 つ以上あります。時相論理は、later modality という形で型に導入されています。同じ型理論を土台として違う論理を記述する方法として、公理を足す方法と logical framework の方法があります。

（問8）
De Morgan cubical type theory で computational type theory を採用した言語は、筆者が調べた範囲では確認できませんでした。Cartesian と De Morgan の違いは、区間の演算だけでなく、型理論の作り方そのものにあります。Cartesian の系統でも computational type theory を採用しているのは RedPRL だけで、後継の redtt と cooltt は流儀を離れました。理由は、cubical な型理論では Nuprl 流の型なし推論が健全でなくなるからです。De Morgan の系統に実装がないのは、偶然ではなく、cubical であること自体に由来する制約によるものです。

（問9）
De Morgan で computational type theory の言語を作れたら、貢献になりえます。ただし、作れた事実だけでは足りず、cubical の困難をどう克服したかを示すことが核心です。

前編・後編を通して述べた中心の主張に戻ります。
型は、言語があらかじめ用意した、変えられない枠ではありません。
何を等しいと見なすかを、言語の設計者が決めています。
そして、その決め方には、得るものと失うものの取引があります。
Nuprl から RedPRL・cooltt への系譜は、その取引の記録です。

📌 用語のミニ解説

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

Cartesian cubical type theory と De Morgan cubical type theory

どちらも、ホモトピー型理論の univalence に計算的内容を与えるために作られた型理論です。区間 I に何の演算を認めるかが違います。De Morgan は反転と最小・最大を入れ、Cartesian は入れません。加えて、型理論の作り方も違います。Cartesian の RedPRL は計算を先に置く流儀、De Morgan の cubicaltt は規則を先に置く流儀です。

区間 I（interval）

ホモトピー型理論で、2 つの要素のあいだのパス（道）を表すために使う型です。0 と 1 という 2 つの端点を持ち、パスは区間 I から型への関数として表されます。

higher inductive types

要素だけでなく、要素のあいだのパスも構成子として持つ帰納型です。円周や商型などを定義できます。

univalence

2 つの型が同値であることと、2 つの型が等しいことを、同一視する原理です。ホモトピー型理論の中心にあります。

formal type theory と computational type theory

formal type theory は、推論規則を先に書き、その規則で型理論を定義する流儀です。Rocq・Lean 4・Agda・cubicaltt がこの流儀です。computational type theory は、先にプログラミング言語があり、その言語のプログラムの振る舞いから型を定める流儀です。Nuprl・RedPRL がこの流儀です。

later modality（▷）

中野浩が 2000 年に提案した型の演算子です。▷A は、1 つの時間の刻みのあとに型 A になる項の型です。時相論理の「次の時点で」に対応します。guarded recursion の基礎です。

guarded recursion

再帰的な定義が無限に展開されないよう、later modality で守った再帰です。無限のデータ構造を安全に扱うために使います。

logical framework

論理体系そのものを記述するための言語です。ひとつの型理論を土台に固定し、その土台を用いて複数の論理体系を記述します。Edinburgh LF、Twelf、Isabelle/Pure、Dedukti が属します。

cubicaltt

Cohen・Coquand・Huber・Mörtberg による De Morgan cubical type theory の型検査器です。Haskell で記述されています。

yacctt

Yet Another Cartesian Cubical Type Theory の略です。cubicaltt を Cartesian に作り直したものです。Haskell で記述されています。

実機検証について

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

検証環境

構成要素 版
MLton 20210117
SML/NJ 110.79
OCaml 5.1.1
GHC 9.4.7
cabal 3.8.1.0
BNFC 2.9.5
RedPRL master（最終コミット 2019 年 11 月。GitHub RedPRL/sml-redprl をソースビルド）
redtt master（最終コミット 2022 年 3 月。GitHub RedPRL/redtt をソースビルド）
cooltt master（最終コミット 2023 年 10 月。GitHub RedPRL/cooltt をソースビルド）
cubicaltt master（最終コミット 2023 年 9 月。GitHub mortberg/cubicaltt をソースビルド）

検証できたこと

  • RedPRL を MLton でビルドし、example/README.prl と example/tutorial.prl の全証明が通った。
     
  • redtt を OCaml 5.1.1 でビルドし、library/prelude.red の全定義が通った。univalence の定義を含む。
     
  • cooltt を OCaml 5.1.1 でビルドし、test/ の 32 本のうち 30 本が通った。test/circle.cooltt で loopn 100 の正規形が計算された。
     
  • cubicaltt を GHC 9.4.7 でビルドし、examples/univalence.ctt が型検査を通った。

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

  • Nuprl は既定でクラウドで動き、公開サーバーのアカウント申請が必要なため、実行していない。
     
  • MetaPRL は OCaml 4.02.3 または 4.05.0 を要求するため、ビルドできなかった。libmojave と camlp5 は導入できたが、OCaml の版の壁で止まった。
     
  • yacctt は実行していない。
     
  • Agda の --cubical は実行していない。

環境構築で越えた壁

cooltt・redtt・cubicaltt のビルドには、次の対処が必要でした。記録として記します。

  • cooltt
    OCaml 5.0 以上が必要なため、5.1.1 を用意した。
    依存パッケージのうち topkg・fmt・cmdliner・uutf・uucp・uuseg・jsonm の 7 つは、GitHub の dbuenzli ミラーから取得した。
    fmt v0.9.0 と cmdliner 2.1.1 が非互換だったため、cmdliner を v1.3.0 に固定した。
    menhir が OCaml 5.1 でビルドできなかっ
    たため、menhirLib だけを dune-universe のミラーからビルドし、dune-project の version を 20231231 に合わせて、menhir が生成するコードと版番号を一致させた。
     
  • redtt
    依存パッケージ astring・rresult は、GitHub のミラーから取得した。
    menhir のフラグ --interpret-show-cst が .ml を生成しないため、--explain だけに変更した。
    OCaml 5.1 でレコードフィールドの曖昧性解消が厳格化されたため、Grammar.mly の {rest with con = …} 9 箇所を ML.{rest with con = …} に変更した。
    警告がエラー扱いになるため、--profile release でビルドした。
     
  • cubicaltt
    libghc-quickcheck2-dev・bnfc・happy・alex を導入した。
    BNFC で Exp.cf からパーサを生成し、ghc --make で直接ビルドした。

訂正一覧

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

関連記事

本記事の接続先

関連連載記事

出典一覧

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?