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)

【Arend 連載⑤】帰納型に条件を付けるだけで、円周が書ける ── Arend の高次帰納型

0
Last updated at Posted at 2026-09-04

thumbnail_picture.jpg

本記事は、連載記事の第５回です

Arend という定理証明支援系について、全７回にわたってお伝えしています。

これまでの流れ

回 何を扱ったか
第１回 なぜ Arend が生まれたのか
第２回 区間を型の中に置き、仕様を単純に保った。代償は計算しきる力
第３回 等しさを型として扱うと、何ができるようになるか
第４回 代数構造の階層を、どこで支えるか（まとめる仕組み）
第５回 data で図形を作る（作る仕組み）

本記事の主題

本記事のテーマは、「data に１行コードを足すと、図形を定義できる」ということです。

Haskell の data は、値の作り方を並べるものでした。

そこに、２つの対象を互いに等しいものとみなす（数学者は同一視する、と表現します）１行を足す。それだけで、円周という図形を定義できます。

その１行が何であるかを、先に見ておきます。

まず、Haskell で分数を書いてみます

＜Haskell のコード＞

data Frac = Frac Int Int

half :: Frac
half = Frac 1 2

twoQuarters :: Frac
twoQuarters = Frac 2 4

Frac 1 2 が $1/2$、Frac 2 4 が $2/4$ を表します。

この２つは、別の値です。 構成子 Frac に渡した数が違うからです。

タロウくん：
・・・分数としては、同じ数ですが。

専任講師：
そこで、Haskell では等しさの判定を自分で書くことになります。

＜Haskell のコード＞

instance Eq Frac where
  Frac a b == Frac c d = a * d == c * b

main :: IO ()
main = print (half == twoQuarters)

タロウくん：
・・・a * d == c * b というのは。

専任講師：
中学生のときに習ったはずの数式を、コードにしたものです。

$2$ つの分数が等号で結ばれているとき、互いの分母と分子をたすきがけして掛け算すると、等しくなります。

$$\frac{a}{b} = \frac{c}{d} \quad \Longleftrightarrow \quad a \times d = c \times b$$

タロウくん：
・・・分母を払う、というやつですね。

専任講師：
$1/2$ と $2/4$ で確かめてみます。

$$1 \times 4 = 4, \qquad 2 \times 2 = 4$$

どちらも $4$ になります。

タロウくん：
・・・だから、等しいと判定される。

専任講師：
コードでは Frac a b の $a$ と $b$、Frac c d の $c$ と $d$ を、そのまま使っています。

コード 数式
Frac a b $\dfrac{a}{b}$
Frac c d $\dfrac{c}{d}$
a * d == c * b $a \times d = c \times b$

＜Haskell の実行結果＞

$ runghc H4.hs

True

True が返ります。

タロウくん：
・・・等しいと判定されました。

専任講師：
しかし、値そのものが同じになったわけではありません。

half と twoQuarters は、依然として別の値です。「等しいと判定する関数を、別に用意した」だけです。

タロウくん：
・・・第３回目の記事で扱った話ですね。== は True を返して終わる。

Arend では、型の定義に書き込みます

＜Arend のコード＞

\data Frac
  | frac Nat Nat

まず、Haskell と同じ形です。 frac 1 2 と frac 2 4 は、別の値です。

ここに、１行を足します。

＜Arend のコード＞

\data Q
  | q Nat Nat
  | same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

２行目の same が、その１行です。

部分 意味
same (a b k : Nat) ３つの自然数 a、b、k を受け取る
q a b = q (a * k) (b * k) q a b と q (a*k) (b*k) を同一視する

分子と分母に同じ数 k を掛けたものは、元と同じである。

そう書き込んでいます。

タロウくん：
・・・約分の関係を、型の定義に入れている。

専任講師：
確かめてみます。

＜Arend のコード＞

\func q1 : Q => q 1 2
\func q2 : Q => q 2 4
\func eq : q1 = q2 => same 1 2 2

＜Arend の型検査結果＞

$ java -jar Arend.jar ADD1.ard

--- Typechecking \default ---
[ ] src.ADD1
--- Done (140ms) ---

タロウくん：
・・・same 1 2 2 が、等しさの根拠ですね。

専任講師：
$a = 1$、$b = 2$、$k = 2$ を渡しています。

$1/2$ の分子と分母に $2$ を掛けると $2/4$ になる。その関係が、根拠になります。

このコードには、誤りが潜んでいます

専任講師：
・・・ところで、このコードには誤りが潜んでいます。いまから修正しますね。

タロウくん：
え？　どこに問題があるんですか？

専任講師：
suc k にしないと、$0$ が入る場合があります。

$0$ が入ると、Q はすべての値がひとつに潰れた型になってしまいます。

タロウくん：
・・・潰れる、といいますと。

専任講師：
same の k に 0 を渡してみます。

＜Arend のコード＞

\func collapse1 : q 1 2 = q 0 0 => same 1 2 0
\func collapse2 : q 3 5 = q 0 0 => same 3 5 0

$a \times 0 = 0$、$b \times 0 = 0$ ですから、どの分数も q 0 0 と等しくなります。

タロウくん：
・・・全部が q 0 0 を経由してつながってしまう。

専任講師：
そうなると、たとえば q 1 2 と q 3 5 が等しくなります。

$$\frac{1}{2} = \frac{3}{5}$$

になってしまうのです。

＜Arend のコード＞

\func bad : q 1 2 = q 3 5 => collapse1 *> inv collapse2

＜Arend の型検査結果＞

$ java -jar Arend.jar K0.ard

--- Typechecking \default ---
[ ] src.K0
--- Done (265ms) ---

型検査を通ってしまいます。

タロウくん：
・・・$1/2$ と $3/5$ が等しい、と示せてしまった。

専任講師：
修正版はこれです。

＜Arend のコード＞

\data Q
  | q Nat Nat
  | same (a b k : Nat) : q a b = q (a Nat.* (suc k)) (b Nat.* (suc k))

＜Arend の型検査結果＞

$ java -jar Arend.jar QFIX.ard

--- Typechecking \default ---
[ ] src.QFIX
--- Done (123ms) ---

suc k にすれば、掛ける数が必ず１以上になります。

タロウくん：
・・・k = 0 を渡しても、掛ける数は suc 0、つまり $1$ になる。

専任講師：
$1$ を掛けても分数は変わりません。潰れなくなります。

なお、本記事の以降のコードでは、説明を簡潔にするため same (a b k : Nat) の形を使います。

実際に有理数を定義する場合には、この修正が必要です。 分母が $0$ でないことも、別に指定する必要があります。

なお、厳密に有理数を定義する場合に必要なものについては、本稿末尾のコラム欄（厳密に有理数を定義するなら、何を追加するのか）をご参照ください。

このような型を、商型と呼びます

タロウくん：
・・・この Q には、名前があるのですか。

専任講師：
商型と呼びます。

「同一視したいもの」を、型の定義に書き込んだ型です。

タロウくん：
・・・「商」というのは。

専任講師：
割り算の商と、同じ言葉です。

$12$ を $4$ で割ると $3$ になります。$12$ 個のものを、$4$ 個ずつのまとまりに分けると、$3$ つのまとまりができます。

タロウくん：
・・・まとめて、数を減らす。

専任講師：
商型も同じです。

$1/2$、$2/4$、$3/6$、$4/8$。これらを、ひとつのまとまりにします。

もとの値 まとめた後
q 1 2, q 2 4, q 3 6, ... ひとつの値（$1/2$ という数）
q 1 3, q 2 6, q 3 9, ... ひとつの値（$1/3$ という数）

タロウくん：
・・・無限にあった値が、まとまりごとに１つになる。

専任講師：
そのまとまりを、数学では同値類と呼びます。

そして、同値類を集めたものが商型です。

タロウくん：
・・・分数は、そうやって作られていたのですね。

専任講師：
数学で有理数を定義するときも、同じ方法を使います。

整数の組 $(a, b)$ を集め、$ad = bc$ のとき $(a,b)$ と $(c,d)$ を同一視する。その結果が、有理数全体です。

同じ１行を、Cubical Agda で書くと

＜Cubical Agda のコード＞

{-# OPTIONS --cubical #-}
data Q : Set where
  q : Nat → Nat → Q
  same : (a b k : Nat) → q a b ≡ q (a * k) (b * k)

＜Agda の型検査結果＞

$ agda QC.agda

Checking QC (/tmp/ag/QC.agda).

４行目が、Arend の same にあたります。

そして、表している数式も同じです。

$$\frac{a}{b} = \frac{a \times k}{b \times k}$$

タロウくん：
・・・記号が違うだけですね。

専任講師：
違いを並べます。

Arend Cubical Agda
等しさの記号 = ≡
構成子の型 q Nat Nat q : Nat → Nat → Q
モードの指定 不要 --cubical が必要

Agda では = を定義に使うため、等しさには ≡ を使います。

Haskell では、この１行を記述できません

＜Haskell のコード＞

{-# LANGUAGE GADTs, DataKinds #-}
data Q where
  Q    :: Int -> Int -> Q
  Same :: (Q 1 2 :~: Q 2 4) -> Q

＜Haskell のエラー＞

$ runghc HQ6.hs

HQ6.hs:6:12: error:
    * Expected kind `GHC.Num.Natural.Natural
                     -> GHC.Num.Natural.Natural -> k0',
        but `Q' has kind `*'
    * In the first argument of `(:~:)', namely `Q 1 2'

タロウくん：
・・・「Q は種 * を持つ」。

専任講師：
Q 1 2 と書いたため、コンパイラは「Q は自然数を２つ受け取るもの」だと解釈しました。

しかし Q は、値を受け取れません。

$$\frac{1}{2} = \frac{2}{4}$$

この数式を、型として記述する手段が、標準の Haskell にはないのです。

Haskell との違い

Haskell Arend Cubical Agda
同一視の１行 記述する手段がない | same ... : q a b = q (a*k) (b*k) same : ... → q a b ≡ q (a*k) (b*k)
１行の置き場所 型の外（instance Eq） 型の定義のなか 型の定義のなか
何を作るか 等しさを判定する関数 等しさの根拠そのもの 等しさの根拠そのもの
値どうしの関係 別の値のまま 同一視される 同一視される

タロウくん：
・・・data の中に記述できるかどうか、が違う。

専任講師：
そして、この同じ１行の仕組みで、円周という図形が定義できます。

本記事は、その仕組みを扱います。

なお、「同型な２つの群を等しいとみなす」という話とは別のものです。 そちらは型と型の関係であり、第１回目の記事で扱いました。

第１回目の記事に、次の記述があります。

２つの群が 同型 であるとは、名前を付け替えただけで、中身の構造がそっくり重なる ということです。

要素どうしを過不足なく対応させられて、しかも演算の結果まで一致する。そういう関係を指します。

同型なら、区別せずに扱う。 数学者は、そうしてきました。

しかし従来の集合論では、この慣行を正当化できませんでした。 同型な２つの群も、集合としては違うものだから です。

ホモトピー型理論 は、これを 構造同一原理 として支えます。

出典：【Arend Theorem Prover 連載（初回）】「同型なものは等しい」を機械に検査させる ── 定理証明支援系 Arend がHoTTを公理としなかった理由

実際に、Arend で書いてみます

専任講師：
同型な２つの群を、実際に定義してみましょう。

＜Arend のコード＞

\data Bool | true | false
\data Bit | one | zero

\func notB (b : Bool) : Bool \elim b
  | true => false
  | false => true

\func xorB (x y : Bool) : Bool \elim x
  | true => notB y
  | false => y

\func notI (x : Bit) : Bit \elim x
  | one => zero
  | zero => one

\func xorI (x y : Bit) : Bit \elim x
  | one => notI y
  | zero => y

\record Group (E : \Set0)
  | unit : E
  | op : E -> E -> E
  | inv : E -> E

\func G1 : Group \cowith
  | E => Bool
  | unit => false
  | op => xorB
  | inv => \lam x => x

\func G2 : Group \cowith
  | E => Bit
  | unit => zero
  | op => xorI
  | inv => \lam x => x

タロウくん：
・・・Bool の群と、Bit の群ですね。

専任講師：
名前が違うだけで、中身は同じです。

Bool の側 Bit の側
false（単位元） zero（単位元）
true one
xorB xorI

タロウくん：
・・・true を one に、false を zero に読み替えただけ。

専任講師：
それが「名前を付け替えただけで、中身の構造がそっくり重なる」ということです。

このコードにも、誤りが潜んでいます

専任講師：
・・・ところで、このコードにも誤りが潜んでいます。いまから修正しますね。

タロウくん：
え？　どこに問題があるんですか？

専任講師：
Group に、群の法則がありません。

\record Group (E : \Set0)
  | unit : E
  | op : E -> E -> E
  | inv : E -> E

単位元、演算、逆元。この３つを並べただけです。

タロウくん：
・・・本連載シリーズの第４回目の記事で、法則を書き込めると伺いました。

専任講師：
そのとおりです。Arend では、レコードの定義のなかに法則を書き込めます。

しかし、いま書いた Group には、それがありません。

タロウくん：
・・・法則を満たさないものも、Group として作れてしまう。

専任講師：
そうなります。修正版はこれです。

＜Arend のコード＞

\record Group (E : \Set0)
  | unit : E
  | op : E -> E -> E
  | inv : E -> E
  | assoc (x y z : E) : op (op x y) z = op x (op y z)
  | unitLeft (x : E) : op unit x = x
  | invLeft (x : E) : op (inv x) x = unit

下の３行が、群の法則です。

法則 意味
assoc どこから計算しても、結果は同じ
unitLeft 単位元を左から演算しても、相手は変わらない
invLeft 逆元を左から演算すると、単位元になる

タロウくん：
・・・すると、G1 を作るときに証明も渡すことになりますね。

専任講師：
そうです。実際に渡してみます。

＜Arend のコード＞

\func G1 : Group \cowith
  | E => Bool
  | unit => false
  | op => xorB
  | inv => \lam x => x
  | assoc => assocB
  | unitLeft => unitLeftB
  | invLeft => invLeftB
  \where {
    \func assocB (x y z : Bool) : xorB (xorB x y) z = xorB x (xorB y z) \elim x, y, z
      | true, true, true => idp
      | true, true, false => idp
      | true, false, true => idp
      | true, false, false => idp
      | false, true, true => idp
      | false, true, false => idp
      | false, false, true => idp
      | false, false, false => idp
    \func unitLeftB (x : Bool) : xorB false x = x => idp
    \func invLeftB (x : Bool) : xorB x x = false \elim x
      | true => idp
      | false => idp
  }

＜Arend の型検査結果＞

$ java -jar Arend.jar GRPLAW.ard

--- Typechecking \default ---
[ ] src.GRPLAW
--- Done (436ms) ---

タロウくん：
・・・assocB が長いですね。

専任講師：
Bool の値は true と false の２つです。３つの引数について場合分けすると、$2^3 = 8$ 通りになります。

そして、どの場合も idp で通ります。 計算すれば同じ形になるからです。

タロウくん：
・・・法則を書き込むと、証明を渡す手間が増える。

専任講師：
その代わり、法則を満たさないものは作れなくなります。

本連載シリーズの第４回目の記事で扱ったとおりです。

なお、本記事では説明を簡潔にするため、以降も法則を省いた Group を使います。

なお、本記事の Group が群の公理を省略している点については、本稿末尾のコラム欄（ここでの Group は、なぜ群の公理を省略しているのか）をご参照ください。

演算が働く対象の型を、等しいと示します

専任講師：
Bool と Bit が等しいことを、Arend で示せます。

＜Arend のコード＞

\func f (b : Bool) : Bit \elim b
  | true => one
  | false => zero

\func g (x : Bit) : Bool \elim x
  | one => true
  | zero => false

\func gf (b : Bool) : g (f b) = b \elim b
  | true => idp
  | false => idp

\func fg (x : Bit) : f (g x) = x \elim x
  | one => idp
  | zero => idp

\func EqType : Bool = Bit => path (iso f g gf fg)

＜Arend の型検査結果＞

$ java -jar Arend.jar ISO2.ard

--- Typechecking \default ---
[ ] src.ISO2
--- Done (232ms) ---

タロウくん：
・・・Bool = Bit が示せました。

専任講師：
iso に４つのものを渡しています。

渡すもの 意味
f Bool から Bit への対応
g Bit から Bool への対応
gf f のあとに g を適用すると、元に戻る
fg g のあとに f を適用すると、元に戻る

タロウくん：
・・・行って戻ってこられる、ということですね。

専任講師：
その４つが揃えば、２つの型は等しいと示せます。

これが一価性です。本連載シリーズの第３回目の記事で、iso を使った移送を扱いました。

なお、同型から型の等しさが出る仕組みについては、本稿末尾のコラム欄（同型から型の等しさが出るのは、なぜか）をご参照ください。

本記事で扱うものとの違い

タロウくん：
・・・本記事の same とは、何が違うのですか。

専任講師：
扱っている階層が違います。

何と何を等しいとするか 使う仕組み
本記事の same q 1 2 と q 2 4（同じ型のなかの値どうし） 高次帰納型
iso Bool と Bit（型と型） 一価性

タロウくん：
・・・値どうしか、型どうしか。

専任講師：
Q という型のなかで、q 1 2 と q 2 4 を同一視する。それが本記事で扱う仕組みです。

Bool という型と Bit という型を等しいとする。そちらは一価性の話です。

タロウくん：
・・・混同しやすいですね。

専任講師：
どちらも「同じとみなす」という言葉で語られるためです。

なお、本記事だけでも読めるように書きました。 第１回目から第４回目までの記事で扱った概念も、必要な範囲で改めて解説します。

本記事のExecutive Summary

本記事を読むと、何が分かるのか

Haskell で data を書いたことがあるでしょうか。

data Nat = Zero | Succ Nat

Zero と Succ。並んでいるのは、値をどう作るかだけです。

この data に、もう１行足すことができたら、何が起きるでしょうか。

２つの値を同一視するという指定を、値の作り方と同じ場所に並べる。

その１行が、これです。

| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

この行は、次の数式を表しています。

$$\frac{a}{b} = \frac{a \times k}{b \times k}$$

分子と分母に同じ数 $k$ を掛けても、分数としては同じ。そう書き込んでいます。

$1/2$ を表す値と、$2/4$ を表す値。その２つを同一視します。

それだけで、円周という図形を型として定義できます。

高次帰納型とは何か

本記事の中心にある概念を、先に定義しておきます。

高次帰納型（higher inductive type、HIT）とは、値を作る構成子に加えて、値どうしの等しさを与える構成子を持てるようにしたデータ型です。

データ型の種類 data に並べられるもの 例
帰納型 値の作り方だけ | q Nat Nat
高次帰納型 値の作り方＋２つの値を同一視するという指定 | same (a b k : Nat) : q a b = q (a*k) (b*k)

一次資料でも、同じように説明されています。

（原文引用）

A higher inductive type may, in addition, have constructors for identifications between elements of the type.

（筆者による日本語訳）

高次帰納型は、それに加えて、その型の要素間の同一視のための構成子を持ちうる。

出典：Taichi Uemura, "Higher inductive types in $(\infty,1)$-categories", arXiv:2410.17615, 2024年10月23日

同じ論文は、通常の帰納型についても述べています。 帰納型とは、その型の要素を作る構成子の集まりによって自由に生成される型である、と。そして例として、構成子が zero と後続子である自然数の型が挙げられています。

そして高次帰納型の例として、円周、命題切断、集合切断の３つが挙げられています。

例 構成子
円周 基点と、その上のループ
命題切断 任意の２つの要素が、構成子によって強制的に同一視される
集合切断 任意の２つの平行な同一視が、構成子によって強制的に同一視される

なお、命題切断と集合切断については、本稿末尾のコラム欄（命題切断と集合切断とは何か）をご参照ください。

なお、この論文の著者である上村太一氏は、本記事が訳語の典拠としている『ホモトピー型理論』の著者と同一人物です。

本記事の結論

この記事の論旨展開と結論を先に要約してお伝えします。

第１に、型理論では、ほとんどすべての型が data で作られています。

自然数も、リストも、そして「等しさ」を表す型も。Lean の公式ドキュメントは「宇宙と依存関数型を除けば、すべてが帰納型である」と述べています。

第２に、しかし data では作れないものがあります。

$1/2$ と $2/4$ を、同じものとして扱いたい。値の作り方を並べるだけでは、この要求に応えられません。

第３に、等式の構成子を並べると、その要求に応えられます。

| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

この１行が表しているのは、$\dfrac{a}{b} = \dfrac{a \times k}{b \times k}$ です。

$1/2$ を表す値と $2/4$ を表す値を同一視する。そう data の中に書く。それが高次帰納型です。

第４に、同じ仕組みで、図形を記述することができます。

点をひとつ置き、その点から自分自身への道をひとつ置く。それだけで、円周を表す型になります。

第５に、Arend では、区間を使ってこの定義を記述します。

第２回目の記事で扱った区間 I が、ここで使われます。

第６に、その書き方を可能にしたのは、第２回目の記事で述べた設計判断でした。

Arend は区間を普通の型として置き、仕様を単純に保ちました。その代わりに、計算しきる力を手放しました。

そして、その単純さが、高次帰納型の定義の単純さを生んでいます。

本記事には、Arend 以外の言語も登場します

本記事の主題は Arend です。

しかし、Arend の設計判断を理解するには、他の言語がどうしているかを見る必要があります。

言語・処理系 本記事で登場する理由 実機検証
Arend 本記事の主題。data の中に道の構成子を並べられる 1.10
Haskell 出発点。data から始める。２つの対象を等しいと宣言する１行を、記述する手段がない GHC 9.4.7
Cubical Agda **対比の中心。**分数の商型も円周も、Arend と同じ形で記述できる Agda 2.6.3
標準の Agda 対比。--cubical を付けないと、円周を定義できない Agda 2.6.3
Lean 4 **対比。**高次帰納型を中核で支えていない 4.33.1
Rocq／Coq **対比。**回避策で高次帰納型を扱う 未検証

Rocq／Coq を除き、本記事に掲載したコードはすべて実機で検証しました。

本記事の議論の流れ

青い枠が、出発点です。

Haskell の data から始めます。読者が毎日使っている道具です。

赤い枠が、行き詰まりです。

$1/2$ と $2/4$ を同じものとして扱いたい。しかし、値の作り方を並べるだけでは足りません。

金色の枠が、本記事の中心です。

等式の構成子を足すと、何が起きるか。そして、同じ仕組みで図形を記述できること。

緑の枠が、到達点です。

第２回目の記事で仕様を単純に保ったことが、ここで見返りを生みます。

本記事の読み方

本記事は長いため、関心に応じた入口を示しておきます。

関心 どこから読むか
２つの対象を等しいと宣言するために追記するコードが、Haskell・Arend・Cubical Agda でそれぞれどうなるかを知りたい 冒頭「本記事の主題」
Haskell の data から読みたい 第１部から順に
分数の $1/2$ と $2/4$ を、なぜ同じ値として扱えないのかを知りたい 第３部
円周がどう定義されるかを知りたい 第５部
他の言語で円周を定義できるかを知りたい 第５部の直後
円周を、区間を使って定義する Arend にしかない書き方を知りたい 第６部・第７部

第１部 ── Haskell の data は、値の作り方だけを並べる

pic_1.jpg

構成子とは何か

皆様は、Haskell で data を書いたことがおありでしょうか。

＜Haskell のコード＞

data Nat = Zero | Succ Nat

Zero と Succ。
この２つを、構成子（constructor）と呼びます。

構成子とは、その型の値を作るための道具です。

Zero は、それだけで値になります。
Succ は、Nat の値をひとつ受け取って、新しい Nat の値を返します。

タロウくん：
・・・部品の型番と、組み立て方の説明書のようなものですね。

専任講師：
Zero から始めて、Succ を繰り返し適用する。
それが Nat の値の作り方のすべてです。

式 表す数
Zero $0$
Succ Zero $1$
Succ (Succ Zero) $2$

帰納型とは何か

data で定義した型を、型理論では帰納型（inductive type）と呼びます。

帰納型とは、構成子を並べることで定義される型です。

そして、その型の値は、並べた構成子を有限回組み合わせて作れるものに限られます。

タロウくん：
・・・「限られる」というのは？

専任講師：
Nat に、Zero でも Succ でもない値が紛れ込むことはありません。

構成子で作れるものが、すべてです。

タロウくん：
書いていないものは、存在しない。

専任講師：
この性質があるおかげで、Nat についての主張を証明できます。

Zero の場合を示し、Succ n の場合を示す。
それで、すべての自然数について示したことになります。

タロウくん：
・・・数学的帰納法ですね。

専任講師：
「帰納型」という名前は、そこから来ています。

なお、帰納型の厳密な定義については、本稿末尾のコラム欄（帰納型の厳密な定義について）をご参照ください。

Arend でも、同じように定義できます。

＜Arend のコード＞

\data MyNat
  | myZero
  | mySuc MyNat

＜Arend の型検査結果＞

$ java -jar Arend.jar T5A.ard

--- Typechecking \default ---
[ ] src.T5A
--- Done (127ms) ---

Haskell の | が、Arend でも同じ役割を果たします。

再帰的な定義

Succ Nat という行に、注目してください。

Nat を定義している途中で、Nat 自身が現れています。

このような定義を、再帰的な定義と呼びます。

タロウくん：
・・・自分を使って自分を定義している。

専任講師：
循環しているように見えますが、しません。

Succ が受け取る Nat は、すでに作られた値です。そこから、新しい値をひとつ作ります。

タロウくん：
・・・小さいものから積み上げていく。

専任講師：
Zero という出発点があるので、循環になりません。

リストも、同じ形です。

＜Arend のコード＞

\data MyList (A : \Type)
  | nil
  | cons A (MyList A)

nil が空のリスト、cons が「先頭に要素をひとつ足す」操作です。

タロウくん：
・・・どちらも、値の作り方を並べているだけですね。

専任講師：
そこが、本記事の出発点になります。

第２部 ── 型理論では、ほとんどすべてが data で作られる

記号の読み方

本記事では、Arend のコードを何度も示します。

先に、記号の読み方をまとめておきます。

Arend 意味 Haskell でいえば Cubical Agda では
\data データ型を定義する data data ... : Set where
\func 関数や値を定義する 関数定義 関数定義
\record レコードを定義する data のレコード構文 record
=> 定義の本体を書き始める = =
\elim x 引数 x について場合分けする case x of パターンマッチ
\with { ... } 条件を書く ── ──
| 構成子や選択肢を区切る | 改行して並べる
\Type 型が置かれる場所 * Set
\Set0 等しさの根拠が高々１本の型を集めた場所 ── ──
\Prop 要素が高々１つしかない型を集めた場所 ── ──
\Pi (x : A) -> ... 依存関数の型 ── (x : A) → ...
-> 関数の型を作る -> →
: 「〜の型を持つ」 :: :
{A : \Type} 暗黙の引数 型変数 a {A : Set}
a = b a と b が等しいことを表す型 ── a ≡ b
idp 両辺が計算して同じ形になる証拠 ── refl
I 区間。left と right を端点に持つ ── I（i0 と i1 を端点に持つ）
left / right 区間の端点 ── i0 / i1
Nat.* 自然数の掛け算 * *
Nat.+ 自然数の足し算 + +
{?} まだ埋めていない箇所 ── ?

なお、\Set0 と \Prop の「高々１つ」が何を数えているのかについては、本稿末尾のコラム欄（\Set0 と \Prop の「高々１つ」は何を数えているのか）をご参照ください。

Cubical Agda の列は、本記事で対比のために使う記号だけを挙げています。

Agda では = を定義に使うため、等しさには ≡ を使います。そして、関数の矢印には → を使います。

太字にした３つが、本記事で新しく出る記号です。

なお、\ はキーワードの目印です。 Haskell のラムダ式とは異なります。

Haskell の \x -> ... にあたるものは、Arend では \lam x => ... と記述します。

Arend の公式マニュアルは、次のページにあります。

なお、本記事に掲載したコードの検証環境については、本稿末尾のコラム欄（本記事のコードの検証環境について）をご参照ください。

また、訳語の選定については、本稿末尾のコラム欄（訳語について）をご参照ください。

パターンマッチと除去規則

構成子は、値を作るための道具でした。

では、作った値を使う側はどうなるでしょうか。

＜Haskell のコード＞

data Nat = Zero | Succ Nat

toInt :: Nat -> Int
toInt Zero     = 0
toInt (Succ n) = 1 + toInt n

main :: IO ()
main = print (toInt (Succ (Succ Zero)))

＜Haskell の実行結果＞

$ runghc H3.hs

2

Zero の場合と Succ n の場合を、それぞれ書いています。

これがパターンマッチです。

Arend では、\elim を使います。

＜Arend のコード＞

\func toNat (n : MyNat) : Nat \elim n
  | myZero => 0
  | mySuc m => suc (toNat m)

\func c : toNat (mySuc (mySuc myZero)) = 2 => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar T5C.ard

--- Typechecking \default ---
[ ] src.T5C
--- Done (130ms) ---

mySuc (mySuc myZero) が 2 になることを、idp で確かめています。

タロウくん：
・・・構成子の数だけ、行を書くのですね。

専任講師：
すべての構成子について書かなければ、型検査を通りません。

この仕組みを、型理論では除去規則と呼びます。

何をするか
構成子 その型の値を作る
除去規則 その型の値を使う

構成子を並べると、除去規則は自動的に決まります。

タロウくん：
・・・作り方を決めれば、使い方も決まる。

専任講師：
第４部で高次帰納型を扱うとき、この対応が効いてきます。

依存関数型

Haskell の関数の型は、こう書きます。

＜Haskell のコード＞

f :: Int -> Bool

Int を受け取って Bool を返す。返す型は、いつも Bool です。

依存型を持つ言語では、返す型が引数の値によって変わる関数を記述することができます。

＜Arend のコード＞

\data Vec (A : \Type) (n : Nat) \elim n
  | 0 => vnil
  | suc m => vcons A (Vec A m)

\func mk (n : Nat) : Vec Nat n \elim n
  | 0 => vnil
  | suc m => vcons 0 (mk m)

＜Arend の型検査結果＞

$ java -jar Arend.jar VEC.ard

--- Typechecking \default ---
[ ] src.VEC
--- Done (174ms) ---

Vec A n は「長さ $n$ の A のベクトル」です。

m と n の関係

タロウくん：
先生、待ってください。

vcons を適用すると、要素が１つ増えますよね。それなら、m を渡すと m+1 個の要素を持つベクトルが返るのではありませんか。

専任講師：
返ります。そして、それで正しいのです。

タロウくん：
・・・宣言では Vec Nat n を返すと書いてあります。

専任講師：
その枝で受け取っている n は、m ではありません。suc m です。

＜Arend のコード＞

\func mk (n : Nat) : Vec Nat n \elim n
  | 0 => vnil
  | suc m => vcons 0 (mk m)

２行目の suc m は、n が suc m という形をしている場合を表しています。

タロウくん：
・・・つまり n = m + 1 である場合。

専任講師：
その枝で返すべき型は Vec Nat (suc m)、つまり長さ m+1 のベクトルです。

そして mk m が長さ m のベクトルを返し、vcons がそこに要素を１つ足します。

式 型
mk m Vec Nat m
vcons 0 (mk m) Vec Nat (suc m)

タロウくん：
・・・要素が１つ増えた結果が、ちょうど求められている長さになる。

vcons 0 の 0 は、何を表すのか

タロウくん：
もうひとつ、確かめさせてください。

vcons 0 (mk m) の 0 ですが、これは長さを表しているのではありませんか。それなら $n = m + 0$ になってしまいます。

専任講師：
その 0 は、長さではありません。先頭に置く要素の値です。

タロウくん：
・・・値、ですか。

専任講師：
vcons が受け取るものを、定義で確かめます。

＜Arend のコード＞

| suc m => vcons A (Vec A m)
引数 何を渡すか
第１引数（A） 要素の値
第２引数（Vec A m） 残りのベクトル

タロウくん：
・・・第１引数が値で、第２引数がベクトル。

専任講師：
vcons 0 (mk m) は、「mk m というベクトルの先頭に、0 という数を置く」という意味です。

タロウくん：
別の数でも構わないのですか。

専任講師：
構いません。

＜Arend のコード＞

\func v1 : Vec Nat 1 => vcons 7 vnil
\func v3 : Vec Nat 3 => vcons 5 (vcons 6 (vcons 7 vnil))

＜Arend の型検査結果＞

$ java -jar Arend.jar VEC3.ard

--- Typechecking \default ---
[ ] src.VEC3
--- Done (157ms) ---

v3 は、$5, 6, 7$ という３つの数が並んだベクトルです。

タロウくん：
・・・では、mk が 0 を使っているのは。

専任講師：
mk は「指定した長さの、中身がすべて 0 のベクトル」を作る関数だからです。

0 は、たまたま選んだ値にすぎません。7 に変えれば、7 が並びます。

タロウくん：
・・・長さは、どこで決まるのですか。

専任講師：
vcons を何回使ったかで決まります。

式 長さ
vnil 0
vcons 0 vnil 1
vcons 0 (vcons 0 vnil) 2
vcons 0 (vcons 0 (vcons 0 vnil)) 3

vcons を１回使うごとに、長さが１増えます。

タロウくん：
・・・引数の値ではなく、適用の回数。

専任講師：
m は、残りのベクトルの長さです。そこに vcons で要素を１つ足すので、全体の長さは m + 1 になります。

そして、その枝で受け取っている n は suc m、つまり m + 1 です。

タロウくん：
・・・一致しますね。

実際に確かめる

専任講師：
実際に確かめてみます。

＜Arend のコード＞

\func check2 : Vec Nat 0 => vnil
\func check3 : Vec Nat 1 => vcons 7 vnil
\func check4 : Vec Nat 2 => vcons 7 (vcons 8 vnil)

vcons を１回使えば長さ１、２回使えば長さ２になります。

タロウくん：
・・・長さが合わないと、どうなりますか。

専任講師：
型検査で弾かれます。

＜Arend のコード＞

\func bad : Vec Nat 2 => vcons 7 vnil

＜Arend の型検査結果＞

$ java -jar Arend.jar VEC2.ard

[ERROR] src.VEC2:6:34: Type mismatch
  Expected type: Vec Nat 1
    Actual type: Vec Nat 0
  In: vnil

要素１個のベクトルを Vec Nat 2 として宣言したため、長さが合わないと指摘されています。

タロウくん：
・・・長さが型に入っているから、検査できる。

専任講師：
mk 3 を呼べば Vec Nat 3 が返り、mk 5 を呼べば Vec Nat 5 が返ります。

返す型が、渡した値によって変わるのです。

このような関数の型を、依存関数型と呼びます。

数学では $\Pi$ という記号を使うため、$\Pi$ 型とも呼ばれます。

Arend では、次のように記述します。

\Pi (n : Nat) -> Vec Nat n

タロウくん：
Haskell では記述できない型ですね。

専任講師：
標準の Haskell には、この仕組みがありません。

なお、依存関数型と対になる依存和型については、本稿末尾のコラム欄（依存関数型と依存和型）をご参照ください。

型理論では、ほとんどすべてが帰納型である

タロウくん：
先生、帰納型は型理論のなかで、どういう位置にあるのですか。

専任講師：
中心的な位置にあります。

Lean の公式ドキュメントが、次のように述べています。

（原文引用）

in Lean's library, every concrete type other than the universes and every type constructor other than Pi is an instance of a general family of type constructions known as inductive types.

（筆者による日本語訳）

Lean のライブラリにおいて、宇宙以外のすべての具体的な型と、依存関数型以外のすべての型構成子は、帰納型と呼ばれる型構成の一般的な族の実例である。

出典：Theorem Proving in Lean, Inductive Types

タロウくん：
・・・宇宙と依存関数型を除けば、すべて。

専任講師：
自然数も、リストも、真偽値も。

そして、等しさを表す型も帰納型です。

タロウくん：
・・・a = b も。

専任講師：
第３回目の記事で扱った同一視型です。過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

x = y と書くと、それは「$x$ と $y$ が等しい」という主張を表す型になります。その型の値が、等しさの根拠にあたります。

その型も、構成子を並べて定義されています。

タロウくん：
・・・idp が、その構成子ですね。

専任講師：
同じドキュメントに、続きがあります。

（原文引用）

It is remarkable that it is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, Pi types, and inductive types.

（筆者による日本語訳）

型宇宙、依存関数型、そして帰納型のみに基づいて、数学の実質的な体系を構築できることは、注目に値する。

出典：同上

タロウくん：
・・・３つだけで、数学が組み立てられる。

専任講師：
data は、思っていたより中心的な道具でした。

なお、この記述がどこまで一般的な言い方かについては、本稿末尾のコラム欄（「ほとんどすべてが帰納型」は、どこまで一般的な言い方か）をご参照ください。

タロウくん：
では、data があれば何でも作れるのですか。

専任講師：
そこに、限界があります。

次の部で、その限界を見ましょう。

第３部 ── しかし、data では作れないものがある

pic_2.jpg

商型と Quot の振り返り

過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

何が困るのか

分数を、データ型として表してみます。

分子と分母の組として持つのが、素直な方法です。

＜Arend のコード＞

\data Frac
  | frac Nat Nat

frac 1 2 が $1/2$、frac 2 4 が $2/4$ を表します。

タロウくん：
・・・$1/2$ と $2/4$ は、同じ数ですね。

専任講師：
数としては同じです。しかし、この定義では別の値になります。

タロウくん：
確かめてみたいのですが。

専任講師：
等しいと主張してみましょう。

＜Arend のコード＞

\func bad : frac 1 2 = frac 2 4 => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar QREV2.ard

[ERROR] src.QREV2:4:36: Expressions are not equal
  Left:  frac 1 2
  Right: frac 2 4
  In: idp

弾かれます。

タロウくん：
・・・「式が等しくない」。

専任講師：
frac 1 2 と frac 2 4 は、別の値です。構成子の適用の仕方が違うからです。

タロウくん：
・・・約分が反映されていない。

商型を使うと、どうなるか

専任講師：
本連載シリーズの第３回目の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

Arend では、data の中に q 1 2 と q 2 4 を同一視する、という指定を記述することができます。

＜Arend のコード＞

\data Q
  | q Nat Nat
  | same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

same の行が、その指定です。

**「分子と分母に同じ数 k を掛けたものは、元と同じである」**という意味です。

タロウくん：
・・・約分の関係を、型の定義に書き込んでいる。

専任講師：
確かめてみます。

＜Arend のコード＞

\func half : Q => q 1 2
\func twoQuarters : Q => q 2 4
\func eq : half = twoQuarters => same 1 2 2

＜Arend の型検査結果＞

$ java -jar Arend.jar QREV.ard

--- Typechecking \default ---
[ ] src.QREV
--- Done (114ms) ---

通ります。

タロウくん：
・・・same 1 2 2 が、等しさの根拠ですね。

専任講師：
$a = 1$、$b = 2$、$k = 2$ を渡しています。

same の行を、数式に直します。

$$\frac{a}{b} = \frac{a \times k}{b \times k}$$

タロウくん：
・・・約分すれば、左辺に戻りますね。

専任講師：
$1/2$ に $k = 2$ を掛けると $2/4$。そして $2/4$ を $2$ で約分すると $1/2$ に戻ります。

$$\frac{1 \times 2}{2 \times 2} = \frac{2}{4}, \qquad \frac{2 \div 2}{4 \div 2} = \frac{1}{2}$$

その関係を、型の定義に書き込んでいます。

このような型を、商型と呼びます。

「同じとみなしたいもの」を、型の定義に書き込んだ型です。

同じ１行を、Cubical Agda で書くと

冒頭で見たとおりです。

＜Cubical Agda のコード＞

  same : (a b k : Nat) → q a b ≡ q (a * k) (b * k)

表している数式は、Arend と同じです。

$$\frac{a}{b} = \frac{a \times k}{b \times k}$$

タロウくん：
・・・等しさの記号が ≡ になっているだけですね。

専任講師：
Agda では = を定義に使うため、等しさには ≡ を使います。

Haskell では、この１行を記述できません

冒頭で見たとおりです。

＜Haskell のコード＞

Same :: (Q 1 2 :~: Q 2 4) -> Q

Q は値を受け取れないため、この行は型検査で弾かれます。

タロウくん：
・・・だから instance Eq を型の外に書くことになる。

専任講師：
そして、型の外に書いた判定は、値そのものを同一視しません。

Lean 4 の Quot

タロウくん：
他の言語では、どうなっていますか。

専任講師：
本連載シリーズの第４回目の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

Lean 4 には、Quot という組み込みの仕組みがあります。

＜Lean 4 のコード＞

-- 型と、その上の同値関係を渡すと、商型が返る
Quot : {α : Sort u} → (α → α → Prop) → Sort u

-- 元の値を、商型の値へ写す
Quot.mk : (r : α → α → Prop) → α → Quot r

-- 同値な2つの値は、商型では等しくなる
Quot.sound : r a b → Quot.mk r a = Quot.mk r b

＜Lean 4 の型検査結果＞

$ lean Q1.lean

@Quot : {α : Sort u_1} → (α → α → Prop) → Sort u_1
@Quot.mk : {α : Sort u_1} → (r : α → α → Prop) → α → Quot r
@Quot.sound : ∀ {α : Sort u_1} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b

「型」と「その上の同値関係」を渡すと、商型を返してくれます。

タロウくん：
・・・Arend とは、書き方が違いますね。

専任講師：
方式が違います。

方式 商型の作り方
Lean 4 Quot という専用の仕組みに、型と同値関係を渡す
Arend data の定義のなかに、等しさを直接書き込む

タロウくん：
・・・どちらでも、商型は得られる。

専任講師：
そこは、本連載シリーズの第４回目の記事で扱いました。

そして本記事で扱うのは、そのどちらも持たない言語です。

商型を持たない言語では、どうするのか

pic_3.jpg

タロウくん：
・・・商型を持たない言語があるのですか？

専任講師：
Rocq／Coq には、商型がありません。

タロウくん：
では、分数をどう扱うのですか。

専任講師：
setoid という方式を使います。

なぜ、setoid 方式を取り上げるのか

本連載シリーズの第３回目の記事で、商型を扱いました。
さらに、第４回目の記事では、Lean 4 の Quot との違いを扱いました。

しかし、どちらの記事でも触れていない論点があります。

商型そのものを持たない言語では、実際にどうしているのか。

その答えが、setoid 方式です。

この方式を知ると、高次帰納型が何を解決したのかが見えてきます。

q 1 2 と q 2 4 を同一視する、と型の定義に書き込めない世界で、関数型プログラミング言語と定理証明支援系を開発してきた先駆者たちはどのような工夫をしたのでしょうか？

次の１行を記述する手段がない場合の対処法を巡る試行錯誤に思いを馳せてみましょう。

| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

先駆者たちの労苦に思いをめぐらすことで、same の一行が持つ意味が分かるのではないでしょうか。

setoid とは何か

setoid（セトイド）とは、型と、その型の上の同値関係を組にしたものです。

タロウくん：
・・・型に、関係を添える。

専任講師：
たとえば、自然数と「２で割った余りが同じ」という関係を組にします。

すると、$0$ と $2$ と $4$ は同じものとして扱われます。

タロウくん：
・・・商型と、似ていますね。

専任講師：
目的は同じです。しかし、やり方が違います。

商型 setoid
同じとみなす仕組み 型の定義に書き込む 型とは別に、関係を持ち歩く
等しさ 言語の = をそのまま使う 関係のほうを使う
関数を作るとき 型検査器が条件を確かめる 関係を保つことを、別に証明する

タロウくん：
・・・持ち歩く。

専任講師：
第４回目の記事で「証明を持ち回る」という話が出てきました。あれと同じ構図です。

Rocq／Coq では、setoid が標準の方式です

（原文引用）

Because the Coq type theory lacks quotient types (as it would make type checking undecidable), one usually bases abstract structures on a setoid ('Bishop set'): a type equipped with an equivalence relation.

（筆者による日本語訳）

Coq の型理論は商型を持たない（それを入れると型検査が決定不能になるため）。そのため、抽象構造は通常、setoid（「ビショップ集合」）── 同値関係を備えた型 ── の上に据えられる。

出典：Bas Spitters, Eelis van der Weegen, "Type Classes for Mathematics in Type Theory", arXiv:1102.1323

タロウくん：
・・・「型検査が決定不能になるため」。

専任講師：
商型を入れないのには、理由があるということです。

そして、Rocq でこの方式が標準であることも記されています。

（原文引用）

Thus, in Rocq, using setoids in place of quotients is the norm.

（筆者による日本語訳）

したがって Rocq では、商型の代わりに setoid を使うのが常道である。

出典：Talia Ringer 他, "Proof Repair across Quotient Type Equivalences", arXiv:2310.06959

setoid 方式の負担

タロウくん：
・・・その方式で、困ることはないのですか。

専任講師：
負担があります。論文の記述を引きます。

（原文引用）

Every type that we talk about needs to come with a relation and a proof that this relation is an equivalence relation. Every function that we use needs to come with a proof that it sends equivalent elements to equivalent elements.

（筆者による日本語訳）

扱うすべての型に、関係と、その関係が同値関係であることの証明を添える必要がある。使うすべての関数に、同値な要素を同値な要素へ写すことの証明を添える必要がある。

出典：Jason Gross, Adam Chlipala, David I. Spivak, "Experience Implementing a Performant Category-Theory Library in Coq", arXiv:1401.7694

タロウくん：
・・・すべての型と、すべての関数に。

専任講師：
そして、等しさが２種類になります。

（原文引用）

users of setoids need to juggle multiple notions of equality, unlike with native quotient types where the same equality is used universally

（筆者による日本語訳）

setoid の利用者は、複数の等しさの概念をやりくりする必要がある。組み込みの商型では、同じ等しさが一様に使われるのとは違う。

出典：Talia Ringer 他, "Proof Repair across Quotient Type Equivalences"（同上）

タロウくん：
・・・言語の = と、自分で定義した関係の２つ。

専任講師：
どちらを使うべきかを、そのつど判断することになります。

「setoid 地獄」という言葉

専任講師：
この負担には、名前が付いています。

（原文引用）

But setoids are impractical, to the extent that the proof assistant community coined the term "Setoid Hell" to refer to their use.

（筆者による日本語訳）

しかし setoid は実用的でない。定理証明支援系のコミュニティが、その使用を指して「setoid 地獄」という語を作ったほどである。

出典："Constructive Analysis in the Agda Proof Assistant", arXiv:2205.08354

タロウくん：
・・・地獄、ですか。

専任講師：
それだけ負担が大きいということです。

タロウくん：
・・・だから、高次帰納型が求められた。

専任講師：
same という一行を書けば、その負担がなくなります。

| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

$\dfrac{a}{b} = \dfrac{a \times k}{b \times k}$ という主張を、型の定義に書き込む。

そうすれば、あとは型検査器が守ってくれるからです。

タロウくん：
・・・setoid 方式は、使われなくなったのですか。

専任講師：
いまも広く使われています。Rocq／Coq の大きなライブラリは、この方式で書かれています。

実用的な方式です。ただし、負担が大きい。

なお、setoid と商型の圏論的な関係については、本稿末尾のコラム欄（setoid と商型の関係を、厳密にいうと）をご参照ください。

また、Coq が商型を持たない理由については、本稿末尾のコラム欄（Coq が商型を持たない理由）をご参照ください。

では、なぜ通常の data では足りないのか

タロウくん：
先生、根本のところを確かめさせてください。

なぜ、通常の data では「q 1 2 と q 2 4 を同一視する」と記述できないのですか。

つまり、この行です。

| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

専任講師：
data に並べられるのが、値の作り方だけだからです。

タロウくん：
・・・第１部で見たとおりですね。

専任講師：
q a b という書き方は、値を作ります。

しかし $\dfrac{a}{b} = \dfrac{a \times k}{b \times k}$ という主張は、値ではありません。

タロウくん：
・・・等しさについての主張。

専任講師：
それを型として記述する手段が、通常の帰納型にはないのです。

専任講師：
frac 1 2 と frac 2 4 は、構成子 frac の適用の仕方が違います。

適用の仕方が違えば、別の値です。

タロウくん：
・・・そこに例外を作る手段がない。

専任講師：
Arend 公式論文も、この点に触れています。

（原文引用）

The notion of quotient type is known to be difficult to handle in MLTT due to the intensionality of the equality.

（筆者による日本語訳）

商型の概念は、等式の内包性ゆえに MLTT では扱いが難しいことがよく知られている。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・「内包性」というのは。

専任講師：
書き方が違えば別のものとして扱う、という性質です。

frac 1 2 と frac 2 4 は、書き方が違います。だから別の値になります。

タロウくん：
・・・中身が同じでも、書き方で区別される。

専任講師：
では、どうすればよいか。

次の部で、その答えを見ましょう。

第４部 ── 等式の構成子を、data に並べる

pic_4.jpg

data の中に、等しさを書き込む

専任講師：
第３部で見たコードを再掲します。

＜Arend のコード＞

\data Q
  | q Nat Nat
  | same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

１行目の q は、これまで見てきた構成子です。
Nat を２つ受け取って、Q の値を作ります。

２行目の same は、違います。

same が作るのは、Q の値ではありません。
q a b = q (a*k) (b*k) という型の値です。

タロウくん：
・・・等しさを表す型ですね。

専任講師：
第３回目の記事で扱った同一視型です。

過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

x = y と書くと、それは「$x$ と $y$ が等しい」という主張を表す型になります。その型の値が、等しさの根拠にあたります。

タロウくん：
same は、その根拠を与えている。

専任講師：
このような構成子を、経路構成子と呼びます。

HoTT では等しさを経路として捉えるため、その名が付いています。

何をするか
通常の構成子 その型の値を作る
経路構成子 値どうしの等しさを与える

タロウくん：
・・・data に、２種類の行が並ぶ。

専任講師：
値の作り方と、２つの値を同一視するという指定。
その両方を、同じ場所に記述することができます。

改めて、その２行を並べます。

| q Nat Nat                                              -- 値を作る
| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k) -- 同一視する
行 何を作るか 数式でいえば
q Nat Nat Q の値 $\dfrac{a}{b}$ という分数そのもの
same ... 値どうしの等しさ $\dfrac{a}{b} = \dfrac{a \times k}{b \times k}$ という主張

タロウくん：
・・・１行目は分数を作り、２行目はその分数どうしの関係を作る。

専任講師：
Cubical Agda でも、同じ２行が並びます。

  q : Nat → Nat → Q
  same : (a b k : Nat) → q a b ≡ q (a * k) (b * k)

Haskell には、２行目にあたるものがありません。

なお、経路構成子が等しさの型そのものを定義しているのではないことについては、本稿末尾のコラム欄（経路構成子は、等しさの型を定義しているのではありません）をご参照ください。

高次帰納型とは何か

経路構成子を持つ帰納型を、高次帰納型（higher inductive type）と呼びます。

データ型の種類 data に並べられるもの 例
帰納型 値の作り方だけ | q Nat Nat
高次帰納型 値の作り方＋２つの値を同一視するという指定 | same (a b k : Nat) : q a b = q (a*k) (b*k)

タロウくん：
「高次」というのは、何が高次なのですか。

専任講師：
値だけでなく、値どうしの等しさも構成するからです。

そして、等しさどうしの等しさも構成できます。

タロウくん：
・・・階層が上がっていく。

専任講師：
その階層の高さを指して「高次」と呼びます。

タロウくん：
「高次」と「高階」は、違うのですか。

専任講師：
別の概念です。

英語では、高次が higher、高階が higher-order です。

高階とは、関数を受け取る関数のような、階数の話を指します。
ここでいう高次は、等しさの階層の高さです。

タロウくん：
・・・訳語が似ているだけ。

専任講師：
本記事では「高次帰納型」と表記します。

なお、名前の似た「高次帰納-帰納型」との違いについては、本稿末尾のコラム欄（「高次帰納型」と「高次帰納-帰納型」の違い）をご参照ください。

除去規則は、どうなるのか

タロウくん：
先生、第２部で「構成子を並べると、除去規則は自動的に決まる」と伺いました。

経路構成子がある場合は、どうなるのですか。

専任講師：
その行についても、値を与えることになります。

第５部で、実際に確かめましょう。

タロウくん：
・・・値の行と、等しさの行の両方を埋める。

専任講師：
そこが、高次帰納型を使うときの要点になります。

第５部 ── 同じ仕組みで、図形を記述できる

円周とは何か

円周とは、平面上で中心から等しい距離にある点の集まりです。輪ゴムの形だとお考えください。

数学では $S^1$ と書きます。

タロウくん：
・・・それを、型として定義するのですか。

専任講師：
点をひとつ置き、その点から自分自身への道をひとつ置く。それだけです。

＜Arend のコード＞

\data S1
  | base
  | loop : base = base

＜Arend の型検査結果＞

$ java -jar Arend.jar T5A.ard

--- Typechecking \default ---
[ ] src.T5A
--- Done (127ms) ---

base が、円周の上の点です。１点だけ置きます。

loop が、base から base への道です。

タロウくん：
・・・出発点と到着点が、同じ点。

専任講師：
円周を一周すると、元の場所に戻ります。その一周が loop です。

タロウくん：
点がひとつしかないのに、円周になるのですか。

専任講師：
HoTT では、型を空間として捉えます。

空間の情報は、点の数ではなく、点どうしの結ばれ方に宿ります。

タロウくん：
・・・道の側に、情報がある。

専任講師：
base から base への道が、idp のほかにもうひとつある。それが円周の本質です。

なお、一点と一本のループが円周を表せる理由については、本稿末尾のコラム欄（一点と一本のループが、なぜ円周を表せるのか）をご参照ください。

loop は、idp とは別のものです

タロウくん：
先生、base = base なら、idp で足りるのではありませんか。

専任講師：
idp も base = base の値です。しかし、loop はそれとは別の値です。

タロウくん：
・・・同じ型の、別の値。

専任講師：
第３回目の記事で扱った「等しさの根拠が複数ある」という話です。

過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

3 = 3 の根拠は、実質１本でした。何通りに書いても、それらは互いに等しくなります。

しかし Bool = Bool の根拠は２本ありました。 何も変えない対応と、true と false を入れ替える対応です。

タロウくん：
・・・円周では、base = base の根拠が複数ある。

専任講師：
idp と loop は、別の根拠です。

この２つを同じものにしてしまうと、円周が点ひとつに潰れます。

なお、idp と loop の違いをより正確に述べる場合については、本稿末尾のコラム欄（idp と loop は何が違うのか）をご参照ください。

商型と円周は、同じ「同一視」なのか

タロウくん：
先生、確かめさせてください。

ここまで「２つの値を同一視する」という説明が続きました。

円周も、同じことをしているのですか。

専任講師：
商型については、そのとおりです。

しかし、円周では違います。

タロウくん：
・・・違うのですか。

専任講師：
順に見ていきましょう。

まず、商型のほうです

＜Arend のコード＞

\data Q
  | q Nat Nat
  | same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

冒頭と第３部で見たものです。 ２行目は $\dfrac{a}{b} = \dfrac{a \times k}{b \times k}$ を表しています。

この Q には、値が２つあります。

式 表す分数
q 1 2 $1/2$
q 2 4 $2/4$

タロウくん：
・・・別々の値です。

専任講師：
q に渡した数が違うので、別の値になります。

そして same が、この２つを同一視します。

＜Arend のコード＞

\func d1 : Q => q 1 2
\func d2 : Q => q 2 4
\func joined : d1 = d2 => same 1 2 2

＜Arend の型検査結果＞

$ java -jar Arend.jar TWO.ard

--- Typechecking \default ---
[ ] src.TWO
--- Done (161ms) ---

タロウくん：
・・・別の値だった q 1 2 と q 2 4 が、同じになった。

専任講師：
これが、まさに「$1/2$ と $2/4$ を同一視する」です。

次に、円周のほうです

＜Arend のコード＞

\data S1
  | base
  | loop : base = base

タロウくん：
・・・こちらも、同じ形に見えます。

専任講師：
base が何を表すか、確かめてください。

タロウくん：
円周の上の点です。

専任講師：
そして、点はこの base ひとつだけです。

タロウくん：
・・・あ。

専任講師：
loop の型は base = base でした。

左辺も右辺も、同じ base です。

タロウくん：
・・・別々の値ではない。

専任講師：
q 1 2 と q 2 4 は、別の値でした。

しかし base と base は、もともと同じ値です。

タロウくん：
では、loop は何をしているのですか。

専任講師：
その点から、その点への道を１本増やしています。

＜Arend のコード＞

\func p1 : base = base => idp
\func p2 : base = base => loop

p1 も p2 も、base = base の値です。そして、この２つは別の値です。

タロウくん：
・・・base はひとつなのに、base = base の値は２つある。

専任講師：
idp と loop です。等しさの根拠が、２本あります。

２つを並べます

① 商型 Q ② 円周 S1
左辺と右辺 q 1 2 と q 2 4。別の値 base と base。同じ値
経路構成子がすること その２つの等しさに、値を与える 同じ点どうしの等しさに、値をもう１つ与える
結果 別だった値が、同じになる 等しさの根拠が、１本から２本になる

タロウくん：
・・・やっていることは、同じですか。

専任講師：
同じです。どちらも、a = b という型に値を与えています。

違うのは、a と b が別の値か、同じ値かです。

タロウくん：
・・・別の値どうしなら、それらが同じになる。

専任講師：
同じ値どうしなら、根拠が増えます。

「同一視」という語について

タロウくん：
・・・では、円周のほうも「同一視」と呼ぶのですか。

専任講師：
呼びません。base と base は、もともと同じ点だからです。

何も同一視していません。

タロウくん：
・・・では、２つをまとめて何と呼べばよいのですか。

専任講師：
a = b という型に値を与える、という言い方が最も正確です。

本記事で「同一視する」と述べてきたのは、商型を念頭に置いた言い方でした。

円周を含めるなら、この言い方に切り替える必要があります。

群同型との違いにも触れておきます

タロウくん：
先生、もうひとつ伺いたいのですが。

同型な２つの群を同じとみなす、という話がありました。あれも同じことですか。

専任講師：
別の話です。

タロウくん：
・・・どう違うのですか。

専任講師：
高次帰納型がするのは、ある型の中で、値どうしの等しさを扱うことです。

Q のなかで q 1 2 と q 2 4 を扱う。S1 のなかで base と base を扱う。どちらも、型の中の話です。

タロウくん：
・・・同型な群のほうは。

専任講師：
２つの型を等しいとみなすことです。

群 $G$ と群 $H$ が同型であるとき、その２つを等しいとみなす。扱っているのは、型と型です。

概念 何を扱うか どこで扱ったか
高次帰納型 型の中の、値どうし 本記事
一価性 型と型 第１回目から第３回目までの記事

タロウくん：
・・・階層が違う。

専任講師：
構造同一性原理、つまり「同型な群は等しい」は、一価性から導かれます。

高次帰納型からではありません。

タロウくん：
・・・混ぜてはいけない。

専任講師：
どちらも「同じとみなす」という言葉で語られるため、混同しやすい箇所です。

除去規則を、確かめる

専任講師：
円周から関数を作ってみます。

＜Arend のコード＞

\func toNat (x : S1) : Nat \elim x
  | base => 0
  | loop => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar S1F.ard

--- Typechecking \default ---
[ ] src.S1F
--- Done (179ms) ---

タロウくん：
・・・loop の行も書いていますね。

専任講師：
構成子が２つあるので、行も２つ要ります。

書かないと、どうなるか見てみましょう。

＜Arend のコード＞

\func toNat (x : S1) : Nat \elim x
  | base => 0

＜Arend の型検査結果＞

$ java -jar Arend.jar S1F2.ard

[ERROR] src.S1F2:5:7: Some clauses are missing
  loop i
  In: toNat

「節が足りない」と指摘されます。

タロウくん：
・・・loop i と書かれています。

専任講師：
そこは、第６部で扱います。

いまは、経路構成子の行も埋める必要があることを押さえてください。

loop の行には、何を書くのか

タロウくん：
loop => idp と書きましたが、これは何を意味していますか。

専任講師：
toNat は、base を 0 へ写します。

loop は base から base への道でした。

タロウくん：
・・・両端とも base に写る。

専任講師：
0 から 0 への道を、返すことになります。

そして「何も動かない道」が idp です。

円周の側 Nat の側
base 0
loop（base から base への道） 0 から 0 への道

タロウくん：
・・・道は道へ写る。

専任講師：
点は点へ、道は道へ。それが、高次帰納型からの関数の作り方です。

円周の道は、いくらでも増える

専任講師：
円周の上で、道を２本つなげてみます。

＜Arend のコード＞

-- 道をつなげる
\func concat {A : \Type} {a b c : A} (p : a = b) (q : b = c) : a = c \elim q
  | idp => p

-- 逆向きの道
\func inv {A : \Type} {a b : A} (p : a = b) : b = a \elim p
  | idp => idp

-- 二周する道
\func loop2 : base = base => concat loop loop

-- 三周する道
\func loop3 : base = base => concat loop2 loop

-- 逆一周
\func loopInv : base = base => inv loop

＜Arend の型検査結果＞

$ java -jar Arend.jar PI1.ard

--- Typechecking \default ---
[ ] src.PI1
--- Done (161ms) ---

タロウくん：
・・・二周、三周と作れますね。

専任講師：
そして、逆向きに回ることもできます。

タロウくん：
・・・マイナス一周。

専任講師：
一周と逆一周をつなげると、何も動かないのと同じになります。

タロウくん：
・・・打ち消し合う。

基本群

専任講師：
道の集まりが、整数と同じ構造をなします。

$\ldots, -2, -1, 0, 1, 2, \ldots$。何周したかを、整数で数えられます。

この構造を、円周の基本群と呼びます。

$$\pi_1(S^1) = \mathbb{Z}$$

タロウくん：
第４回目の記事で扱った群ですね。

専任講師：
道をつなげる操作が演算、何も動かない道が単位元、逆向きの道が逆元にあたります。

群の要素 円周でいえば
演算 道をつなげる
単位元 何も動かない道（idp）
逆元 逆向きに回る道

タロウくん：
・・・第４回目の記事で定義した Monoid や Group の形ですね。

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

本記事では、この定理の証明には立ち入りません。

HoTT の枠組みでこの定理が証明できることだけを、押さえておいてください。

なお、証明の概要については、本稿末尾のコラム欄（円周の基本群の証明について）をご参照ください。

トーラスも、同じ仕組みで記述できる

タロウくん：
円周以外の図形も、記述することができるのですか。

専任講師：
できます。トーラスを見てみましょう。

トーラスとは、ドーナツの表面の形です。

＜Arend のコード＞

\data Torus
  | point
  | line1 : point = point
  | line2 : point = point
  | face : Path (\lam i => line1 i = line1 i) line2 line2

＜Arend の型検査結果＞

$ java -jar Arend.jar TORUS.ard

--- Typechecking \default ---
[ ] src.TORUS
--- Done (115ms) ---

タロウくん：
・・・道が２本ありますね。

専任講師：
ドーナツには、２通りの回り方があります。

道 どう回るか
line1 ドーナツの穴を通って、内側を回る
line2 ドーナツの周りを、外側に沿って回る

タロウくん：
・・・確かに、２通りあります。

専任講師：
そして４行目の face は、その２つの回り方をつなぐ面です。

タロウくん：
・・・道どうしの関係を、さらに指定している。

専任講師：
点、道、面。３つの階層が並んでいます。

そして、それらがすべて data のなかに書かれています。

タロウくん：
・・・「高次」というのは、こういうことですか。

専任講師：
値だけでなく、等しさも、等しさどうしの等しさも構成できる。その階層の高さです。

他の言語で、円周を定義できるか

pic_5.jpg

タロウくん：
先生、確かめさせてください。

この円周の定義は、他の言語でも記述することができるのですか？

専任講師：
処理系によって、はっきり分かれます。

処理系 円周を定義できるか 方式
Arend できる 中核が支える。２通りの書き方がある
Cubical Agda できる 中核が支える
Rocq／Coq 標準ではできない HoTT ライブラリが回避策を使う
標準の Agda 標準ではできない 同じ回避策を使う
Lean 4 できない 公理として仮定するしかない

タロウくん：
・・・第４回目の記事とは、事情が違いますね。

専任講師：
第４回目の記事では、どの処理系でも代数構造の階層を組み上げられました。違うのは、どこで支えるかでした。

本記事では、そもそも中核で支えている処理系が限られます。

順に見ていきましょう。

Lean 4 の場合

（原文引用）

Lean 4 does not natively support higher-inductive types (HITs). Unlike Agda's --cubical mode or Coq's HoTT library, there is no built-in mechanism for defining types with both point and path constructors.

（筆者による日本語訳）

Lean 4 は、高次帰納型を中核で支えていない。Agda の --cubical モードや Coq の HoTT ライブラリとは違い、点の構成子と道の構成子の両方を持つ型を定義する仕組みが、組み込みで用意されていない。

出典：Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira, "The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups", arXiv:2512.03175, 2025年

タロウくん：
・・・書く手段がない。

専任講師：
実際に試してみます。

＜Lean 4 のコード＞

inductive S1 : Type where
  | base : S1
  | loop : base = base

＜Lean 4 の型検査結果＞

$ lean S1.lean

S1.lean:3:11: error(lean.ctorResultingTypeMismatch): Unexpected resulting type for constructor `S1.loop`: Expected
  S1
but found
  base = base

弾かれます。

タロウくん：
・・・「構成子の結果の型は S1 であるべきだが、base = base になっている」。

専任講師：
Lean 4 の inductive では、構成子が返せるのは定義中の型そのものだけです。

等しさの型を返す構成子は、宣言できません。

タロウくん：
・・・第４部で見た経路構成子が、書けない。

専任講師：
公理として仮定することはできます。しかし、そうすると計算規則が伴いません。

本連載シリーズの第１回目の記事で扱った論点です。

タロウくん：
・・・証明は記述できるが、走らせると途中で止まる。

なぜ Lean 4 では扱えないのか

専任講師：
Lean には、かつて HoTT モードがありました。

（原文引用）

The standard mode is for proof irrelevant reasoning, in which Prop, the bottom universe, contains types whose objects are considered to be judgmentally equal. Since this is incompatible with homotopy type theory, a second HoTT mode was added.

（筆者による日本語訳）

標準モードは証明無関係な推論のためのものである。そこでは最下層の宇宙 Prop が、その要素どうしが判定的に等しいとみなされる型を含む。これはホモトピー型理論と両立しないため、第２のモードとして HoTT モードが追加された。

出典：Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz, "Homotopy Type Theory in Lean", arXiv:1704.06781

タロウくん：
・・・「証明無関係」というのは。

専任講師：
同じ主張についての証明は、すべて等しいとみなすという規則です。

確かめてみます。

＜Lean 4 のコード＞

-- 同じ主張についての2つの証明は、rfl だけで等しいと示せる
example (p q : (2:Nat) = 2) : p = q := rfl
example (P : Prop) (p q : P) : p = q := rfl

＜Lean 4 の型検査結果＞

$ lean PI.lean

何も出力されません。型検査を通過しています。

タロウくん：
・・・rfl だけで、２つの証明が等しいと示せている。

専任講師：
証明の中身を見ずに、等しいと判定されているのです。

タロウくん：
・・・等しさの根拠が、１本しかないことになる。

専任講師：
円周では、base = base の根拠が複数あります。

idp、一周する道、二周する道。それらが別のものでなければ、円周になりません。

タロウくん：
・・・証明無関係だと、全部同じになってしまう。

専任講師：
円周が、点ひとつに潰れます。

この非両立を避けるために、Lean 2 では HoTT モードが別に用意されました。

そして、Lean 3 以降で廃止されました。

タロウくん：
・・・本連載シリーズの第１回目の記事の表にあった話ですね。

Rocq／Coq と、標準の Agda の場合

専任講師：
どちらも、中核では高次帰納型を支えていません。

しかし、回避策があります。

（原文引用）

Coq does not implement higher inductive types natively, so we simulate them using Licata's trick. This method was originally used in Agda; to make it possible in Coq, experimental private inductive types had to be added.

（筆者による日本語訳）

Coq は高次帰納型を中核で実装していないため、我々は Licata の技法を用いてそれを模倣する。この方法はもともと Agda で使われていた。Coq で可能にするには、実験的な private inductive type を追加する必要があった。

出典：Andrej Bauer 他, "The HoTT Library: A formalization of homotopy type theory in Coq", arXiv:1610.04591

タロウくん：
・・・どういう技法ですか。

専任講師：
２段階に分けます。

まず、モジュールの中に、点の構成子だけを持つ型を定義します。この型は、モジュールの外からは中身が見えません。

次に、道の構成子を公理として足します。

タロウくん：
・・・点は普通に作り、道は公理として仮定する。

専任講師：
そして、除去規則も自分で定義し、その計算規則も公理として足します。

タロウくん：
・・・手作業ですね。

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

（原文引用）

Just adding HITs as constants is not satisfactory, because then the computation rules are not judgmental equalities.

（筆者による日本語訳）

高次帰納型を単に定数として追加するだけでは満足できない。そうすると、計算規則が判定的な等しさにならないからである。

出典：Floris van Doorn 他, "Homotopy Type Theory in Lean"（同上）

タロウくん：
・・・だから、モジュールで囲むという工夫が要る。

専任講師：
標準の Agda でも、同じ事情です。

実際に試してみます。

＜標準の Agda のコード＞

module S1STD where

open import Agda.Builtin.Equality

data S¹ : Set where
  base : S¹
  loop : base ≡ base

＜Agda の型検査結果＞

$ agda S1STD.agda

/tmp/ag/S1STD.agda:7,3-21
The target of a constructor must be the datatype applied to its
parameters, base ≡ base isn't
when checking the constructor loop in the declaration of S¹

弾かれます。

タロウくん：
・・・「構成子の結果の型は、その定義中のデータ型でなければならない」。

専任講師：
Lean 4 と同じ理由です。

そして、--cubical を付けると通ります。

＜Cubical Agda のコード＞

{-# OPTIONS --cubical #-}
module S1 where

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

data S¹ : Set where
  base : S¹
  loop : base ≡ base

＜Agda の型検査結果＞

$ agda S1.agda

Checking S1 (/tmp/ag/S1.agda).

通ります。

タロウくん：
・・・同じコードなのに、オプションひとつで結果が変わる。

専任講師：
--cubical は、Agda の型理論そのものを切り替えるオプションです。

この切り替えによって、経路構成子を宣言できるようになります。

タロウくん：
・・・回避策を使わずに済む。

専任講師：
そこまでして、高次帰納型を使えるようにしているのです。

そして、この技法の上で大きな成果が上がっています。

Rocq／Coq の HoTT ライブラリは、この方式で書かれています。

なお、Licata の技法の手順については、本稿末尾のコラム欄（Licata の技法の詳細）をご参照ください。

Arend と Cubical Agda の場合

専任講師：
この２つは、中核で支えています。

回避策を使わずに、data の中に道の構成子を並べられます。

タロウくん：
・・・先ほど書いたコードが、そのまま通る。

専任講師：
そして、除去規則も自動的に決まります。第２部で扱ったとおりです。

整理すると

処理系 道の構成子を、どう扱うか 除去規則
Arend data の中に並べる 自動的に決まる
Cubical Agda data の中に並べる 自動的に決まる
Rocq／Coq モジュールで囲み、公理として足す 自分で定義し、計算規則も公理として足す
標準の Agda 同上 同上
Lean 4 公理として仮定する 同上

タロウくん：
・・・回避策を使うか、公理として足すか。

専任講師：
そこが、HoTT を扱う処理系の分かれ目です。

タロウくん：
Lean 4 では、HoTT の研究ができないということですか。

専任講師：
そうではありません。

公理として仮定すれば、形式化はできます。 Lean 2 の HoTT ライブラリには、大きな蓄積がありました。

できないのは、計算規則を伴う形で扱うことです。

Lean 4 で高次帰納型を扱った、実際の例

タロウくん：
・・・公理として仮定した形式化は、実際にあるのですか？

専任講師：
2025年に公開された論文が、その例です。

ザイフェルト＝ファン・カンペンの定理という、基本群を計算するための定理を Lean 4 で形式化したものです。

タロウくん：
・・・第５部で扱った基本群ですね。

専任講師：
そのとおりです。円周だけでなく、クラインの壺、実射影平面、種数 $g$ の曲面、レンズ空間の基本群まで計算されています。

規模を、論文から引きます。

項目 値
Lean 4 のコード 41,130行
モジュール数 107
カーネル公理 36個（すべて高次帰納型のため）

タロウくん：
・・・４万行。

専任講師：
そして、円周のために７個の公理が使われています。

公理 何を宣言するか
Circle 型そのもの
circleBase 基点
circleLoop ループ
circleRec 除去規則
circleRec_base 基点についての計算規則
circleRec_loop ループについての計算規則
circleInd 帰納法の原理

タロウくん：
・・・本記事の第２部で扱った、構成子と除去規則ですね。

専任講師：
Arend では data に２行書けば済むものが、Lean 4 では７個の公理になります。

なぜ公理が必要なのか

論文は、その理由を円周について述べています。

（原文引用）

Needs a non-trivial loop loop : Path(base, base) that is not ρ. No Lean type has this property without axioms.

（筆者による日本語訳）

$\rho$ ではない非自明なループ loop : Path(base, base) が必要である。公理なしに、この性質を持つ Lean の型は存在しない。

出典：Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira, "The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups", arXiv:2512.03175, 2025年

タロウくん：
・・・$\rho$ というのは？

専任講師：
この論文で、何も動かない道を表す記号です。Arend の idp にあたります。

「idp ではない loop を持つ型は、公理なしには作れない」ということです。

証明無関係の問題を、どう回避したのか

タロウくん：
先ほど、Lean 4 では証明無関係のために円周が潰れると伺いました。

公理を足すだけで、その問題は解決するのですか。

専任講師：
それだけでは解決しません。この論文は、別の工夫をしています。

（原文引用）

If paths were identified solely by their equality proofs, all loops at a point would be equal, collapsing π1 to the trivial group.

（筆者による日本語訳）

もし道が、その等しさの証明のみによって同一視されるなら、ある点におけるすべてのループが等しくなり、$\pi_1$ が自明な群へ潰れてしまう。

出典：同上

タロウくん：
・・・本記事で述べたとおりです。

専任講師：
そこで、この論文では道を「書き換えの手順の並び」として表しています。

＜Lean 4 のコード＞

structure Path {A : Type u} (a b : A) where
  steps : List (Step A)  -- 書き換え手順の明示的な並び
  proof : a = b          -- 導かれた等しさの証明

steps のほうが、道を区別する情報です。

タロウくん：
・・・等しさの証明ではなく、手順の並びで区別する。

専任講師：
同じ端点を持つ２つの道が、違う手順の並びを持つことがあります。

そして、手順の並びを変換する規則が別に定められています。

この例が示すこと

タロウくん：
・・・Lean 4 でも、基本群の計算はできる。

専任講師：
できます。ただし、公理と工夫が必要です。

Arend・Cubical Agda Lean 4
円周の宣言 data に２行 ７個のカーネル公理
道の表し方 言語の等しさの型 書き換え手順の並びを持つ構造体
証明無関係への対処 不要 道を証明とは別に区別する設計が必要

タロウくん：
・・・回り道をしている。

専任講師：
そして、その回り道が41,130行という規模につながっています。

なお、この論文はトーラスについて、公理を追加せずに済ませています。 $T^2 = S^1 \times S^1$ として構成し、円周の公理だけを使うためです。

本記事の第５部で、トーラスを高次帰納型として定義しました。 Arend では、そちらの書き方も可能です。

タロウくん：
・・・本連載シリーズの第１回目の記事の論点に戻りますね。

専任講師：
公理として扱うか、計算対象として扱うか。
そこがポイントになります。

第６部 ── Arend では、条件を書いて定義する

まず、整数で見てみます

専任講師：
円周に入る前に、もっと単純な例で仕組みを確かめましょう。

整数を、データ型として定義してみます。

整数は、$0$ 以上の数と、$0$ 未満の数に分けられます。

＜Arend のコード＞

\data MyInt
  | pos Nat
  | neg Nat \with {
    | zero => pos zero
  }

＜Arend の型検査結果＞

$ java -jar Arend.jar T5D.ard

--- Typechecking \default ---
[ ] src.T5D
--- Done (151ms) ---

タロウくん：
・・・pos が $0$ 以上、neg が $0$ 未満ですね。

専任講師：
pos n が $n$ を表し、neg n が $-n$ を表します。

式 表す整数
pos 0 $0$
pos 1 $1$
pos 2 $2$
neg 1 $-1$
neg 2 $-2$

タロウくん：
先生、neg 0 はどうなるのですか。

専任講師：
$-0$ は $0$ です。pos 0 と同じものです。

タロウくん：
・・・２通りの書き方で、同じ数を表してしまう。

専任講師：
そこで、条件を書きます。

| neg Nat \with {
    | zero => pos zero
  }

「neg に zero を渡したときは、pos zero と同じである」という指定です。

タロウくん：
確かめてみたいのですが。

専任講師：

＜Arend のコード＞

\func a : MyInt => pos 0
\func b : MyInt => neg 0
\func c : a = b => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar T5G.ard

--- Typechecking \default ---
[ ] src.T5G
--- Done (126ms) ---

idp だけで通ります。証明を書く必要がありません。

タロウくん：
・・・計算して同じ形になる、ということですね。

なぜ、neg の側だけに条件があるのか

タロウくん：
先生、ひとつ分からないことがあります。

なぜ neg の側だけに zero の場合分けが定義されていて、pos の側には定義されていないのですか。

$0$ が重複しているのなら、どちらに書いても同じではありませんか。

専任講師：
２つ理由があります。順に見ていきましょう。

理由① ── 片方だけ書けば足りる

専任講師：
条件の役割は、重複を潰すことです。

pos 0 と neg 0 という２つの表し方があるとき、片方をもう片方に寄せれば済みます。

タロウくん：
・・・両方に書く必要がない。

専任講師：
neg zero は pos zero である、と一度書けば、重複は消えます。

そして残る表し方は、次のとおりです。

表し方 表す整数
pos 0, pos 1, pos 2, ... $0, 1, 2, \ldots$
neg 1, neg 2, neg 3, ... $-1, -2, -3, \ldots$

タロウくん：
・・・neg 0 は、この一覧に入っていません。

専任講師：
pos 0 に吸収されたからです。すべての整数が、ちょうど１通りで表されます。

理由② ── 両方には書けない

専任講師：
仮に、両方に書いてみます。

＜Arend のコード＞

\data MyInt2
  | pos2 Nat \with {
    | zero => neg2 zero
  }
  | neg2 Nat \with {
    | zero => pos2 zero
  }

＜Arend の型検査結果＞

$ java -jar Arend.jar T5F.ard

[ERROR] src.T5F:10:7: Constructors may refer only to previously defined constructors
  In: | zero => neg2 zero

弾かれます。

タロウくん：
・・・「構成子は、すでに定義された構成子のみを参照できる」。

専任講師：
pos2 を定義している時点では、neg2 はまだ定義されていません。

先に書いた構成子は、後に書く構成子を参照できないのです。

タロウくん：
・・・だから、後ろに書いた neg の側にしか条件を書けない。

専任講師：
neg は pos より後に定義されているので、pos を参照できます。

タロウくん：
順序が決まっていたのですね。

専任講師：
条件が循環しないように、この規則が置かれています。

もし両方が互いを参照できたら、pos zero は neg zero であり、neg zero は pos zero である、という循環になります。

タロウくん：
・・・どちらに寄せればよいのか、決まらなくなる。

専任講師：
片方だけに書く。そして、後ろに書いたほうに書く。

その２つが、この定義の理由です。

条件は、関数を書くときにも効いてきます

専任講師：
条件を書いた型から、関数を作ってみます。

＜Arend のコード＞

\func f (x : MyInt) : Nat
  | pos n => n
  | neg n => suc n

＜Arend の型検査結果＞

$ java -jar Arend.jar T5E.ard

[ERROR] src.T5E:9:5: Conditions check failed
  f (neg n) [n = 0] => 0
  while the right hand side
  suc n [n = 0] => 1
  In: | neg n => suc n

弾かれます。

タロウくん：
・・・「条件の検査に失敗した」。

専任講師：
neg 0 は pos 0 と同じものでした。

そのため、f (neg 0) と f (pos 0) は同じ値にならなければなりません。

タロウくん：
・・・f (pos 0) は 0 です。

専任講師：
しかし f (neg 0) は、suc 0 つまり 1 になります。

食い違います。

タロウくん：
・・・エラーメッセージに、その食い違いが書かれていますね。

専任講師：
0 になるはずのところが 1 になっている、と指摘されています。

条件を書き込むと、型検査器がそれを守らせてくれるのです。

この形の定義を、条件付き帰納型と呼びます。

通常の帰納型に、「この位置ではこの値になる」という条件を添えたものです。

なお、条件付き帰納型の一般形については、本稿末尾のコラム欄（条件付き帰納型の一般形）をご参照ください。

同じ仕組みで、円周を定義する

pic_6.jpg

専任講師：
条件付き帰納型の仕組みを使って、円周を定義してみます。

＜Arend のコード＞

\data S1'
  | base'
  | loop' I \with {
    | left => base'
    | right => base'
  }

＜Arend の型検査結果＞

$ java -jar Arend.jar T5A.ard

--- Typechecking \default ---
[ ] src.T5A
--- Done (127ms) ---

タロウくん：
・・・すみません、分かりません。

なぜこれが円周になるのですか。left、right のあたりから分からなくなりました。

専任講師：
順に見ていきましょう。

まず、区間 I とは何か

専任講師：
第２回目の記事で扱った区間 I です。過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

I は、２つの端点を持つ型です。

端点 名前
始点 left
終点 right

タロウくん：
・・・数学の閉区間 $[0, 1]$ のようなものですか。

専任講師：
似ていますが、別のものです。

I からは、left と right 以外の値を取り出すことができません。$0.5$ にあたる値を取り出す手段が、言語に用意されていないのです。

タロウくん：
・・・両端しか見えない。

専任講師：
それでも、I は「両端をつなぐもの」として振る舞います。

loop' I は、何を表すのか

専任講師：
loop' I という行を見てください。

これは、loop' が区間 I の値をひとつ受け取る構成子であることを表します。

タロウくん：
・・・区間を受け取って、S1' の値を返す。

専任講師：
区間の各位置に対して、S1' の値がひとつ決まります。

区間の位置 loop' が返す値
left ？
途中 ？
right ？

タロウくん：
・・・値が並んでいる。

専任講師：
区間に沿って値が並ぶ。それが「道」です。

\with が、両端での値を決める

専任講師：
\with の中を見てください。

| left => base'
| right => base'

「left では base'、right では base' になる」という指定です。

タロウくん：
・・・両端とも base'。

専任講師：
表を埋めます。

区間の位置 loop' が返す値
left base'
途中 loop' の値（base' とは限らない）
right base'

タロウくん：
・・・出発点と到着点が、同じ点。

専任講師：
そこが、円周になる理由です。

なぜ、それが円周なのか

専任講師：
ひもを１本、思い浮かべてください。

タロウくん：
はい。

専任講師：
そのひもの両端を、同じ場所に留めます。

タロウくん：
・・・輪になりますね。

専任講師：
それが円周です。

コードの要素 ひもでいえば
I ひも１本
base' 留める場所
left => base' 左端を、そこに留める
right => base' 右端を、同じ場所に留める

タロウくん：
・・・１本のひもの両端を、同じ場所に留めた。

専任講師：
点はひとつしかありません。しかし、その点から出て、その点に戻る道があります。

タロウくん：
なぜ、点がひとつで足りるのですか。

専任講師：
HoTT では、型を空間として捉えます。

空間の情報は、点の数ではなく、点どうしがどう結ばれているかに宿ります。

タロウくん：
・・・道の側に、情報がある。

専任講師：
base' から base' への道が、idp のほかにもうひとつある。それが円周の本質です。

先ほどの書き方と、並べる

専任講師：
第５部で見た書き方を、もう一度示します。

＜Arend のコード＞

\data S1
  | base
  | loop : base = base

タロウくん：
・・・こちらのほうが短いですね。

専任講師：
表しているものは同じです。書き方が違います。

書き方 何を書くか
等式で書く loop : base = base 等しさの型を、そのまま書く
区間で書く loop' I \with { ... } 区間を受け取り、両端での値を書く

タロウくん：
先生、第５部でエラーメッセージに loop i と書かれていました。

専任講師：
loop : base = base と書いた場合でも、Arend の内部では区間を受け取る構成子として扱われています。

タロウくん：
・・・書き方が違うだけで、中身は同じ。

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

タロウくん：
なぜ、２つの書き方があるのですか。

専任講師：
そこが、次の部で扱う論点です。

区間を使う書き方が、Arend の設計の核心にあたります。

トーラスも、区間で記述できる

専任講師：
トーラスも、同じ仕組みで記述することができます。

＜Arend のコード＞

\data Torus
  | point
  | line1 I \with { | left => point | right => point }
  | line2 I \with { | left => point | right => point }

＜Arend の型検査結果＞

$ java -jar Arend.jar TORUS2.ard

--- Typechecking \default ---
[ ] src.TORUS2
--- Done (107ms) ---

タロウくん：
・・・ひもが２本、同じ場所に留められている。

専任講師：
２通りの回り方が、そこから生まれます。

第７部 ── 第２回の設計判断が、ここで実を結ぶ

区間を使う方式の利点

専任講師：
Arend 公式論文が、区間を使う方式についてこう述べています。

（原文引用）

Having the interval type I, path constructors can be simply defined as constructors with a parameter of the interval type.

（筆者による日本語訳）

区間型 I があれば、道の構成子は、区間型の径数を持つ構成子として単純に定義できる。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・「単純に定義できる」。

専任講師：
そして、定義の一般的な図式についても述べています。

（原文引用）

The general scheme of such inductive definitions can be easily formulated: it is the standard scheme plus specification of a valid form of conditions, which is rather simple.

（筆者による日本語訳）

この種の帰納的定義の一般的な図式は、容易に定式化できる。それは標準的な図式に、条件の妥当な形の指定を加えたものであり、それはかなり単純である。

出典：同上

タロウくん：
・・・「標準的な図式に、条件を加えたもの」。

専任講師：
通常の帰納型の仕組みが、そのまま使えるということです。

新しい仕組みを持ち込むのではなく、既存の仕組みに条件を添えるだけで済みます。

なお、ここでいう「一般的な図式」が何を指すかについては、本稿末尾のコラム欄（高次帰納型の一般的な図式について）をご参照ください。

HoTT Book の方式との比較

専任講師：
同じ論文が、教科書の方式についてはこう述べています。

（原文引用）

In this approach to HITs it is not at all obvious how to formulate a rigorous general scheme for such general inductive definitions.

（筆者による日本語訳）

この高次帰納型への手法では、この種の一般的な帰納的定義の厳密な図式をどう定式化するかは、まったく自明でない。

出典：同上

タロウくん：
・・・「まったく自明でない」。

専任講師：
教科書の方式では、道の構成子を等式の型として宣言します。

その場合、一般的な図式を定式化するのが難しいということです。

第２回目の記事で述べたことを、振り返ります

専任講師：
本連載シリーズの第２回目の記事で、Arend は区間を普通の型として置きました。仕様を単純に保つためです。

その代わりに、計算しきる力を手放しました。

そして、その単純さが、ここで見返りを生みました。

タロウくん：
分かりやすいです。

と同時に確認したいことが出てきました。

区間を普通の型とは異なる扱いをする Cubical Agda では、区間に対して、普通の型に対して行うように、高次帰納型のデータ処理はできないということですか。

専任講師：
そこは、正確に分けて答える必要があります。

Cubical Agda でも、高次帰納型は定義できます

専任講師：
Cubical Agda は、高次帰納型を扱えます。円周も定義できます。

＜Cubical Agda のコード＞

{-# OPTIONS --cubical #-}
module S1 where

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

data S¹ : Set where
  base : S¹
  loop : base ≡ base

＜Agda の型検査結果＞

$ agda S1.agda

Checking S1 (/tmp/ag/S1.agda).

出典：Cubical, Agda Documentation

タロウくん：
・・・Arend の１つ目の書き方と、同じ形ですね。

専任講師：
そのとおりです。「できない」という話ではありません。

違うのは、構成子の宣言の仕方です

タロウくん：
では、何が違うのですか。

専任講師：
Arend では、道の構成子を区間を引数に取る通常の構成子として宣言できます。

\data S1'
  | base'
  | loop' I \with {
    | left => base'
    | right => base'
  }

loop' I の I が、引数の型です。Nat や Bool を引数に取るのと、同じ書き方です。

Cubical Agda では、この書き方ができません。

道の構成子は、loop : base ≡ base のように等式の型として宣言します。

タロウくん：
・・・なぜ、その違いが生じるのですか。

専任講師：
Cubical Agda の区間 I が、通常の型と同じ場所に住んでいないからです。

Cubical Agda の区間は、特別な場所に住んでいます

専任講師：
Cubical Agda の開発者のひとり、Andrea Vezzosi は、こう述べています。

（原文引用）

As Agda doesn't have a notion of non-fibrant types (yet?) the interval I lives in Setω.

（筆者による日本語訳）

Agda は非ファイブラント型という概念を（まだ）持たないため、区間 I は Setω に住む。

出典：Cubical Agda, Homotopy Type Theory blog, 2018年12月6日

タロウくん：
・・・Setω というのは。

専任講師：
Agda の宇宙階層のいちばん外側にある、特別な宇宙です。

通常の型が住む Set 0、Set 1、Set 2 のどれにも収まりません。

タロウくん：
・・・階層の外に置かれている。

専任講師：
そのため、I を通常の型と同じようには扱えません。構成子の引数の型として、そのまま書くこともできないのです。

なお、Setω と非ファイブラント型については、本稿末尾のコラム欄（Setω と非ファイブラント型）をご参照ください。

ただし、除去の側では区間変数を使います

タロウくん：
では、Cubical Agda では区間をまったく使わないのですか。

専任講師：
使います。関数を定義するときです。

＜Cubical Agda のコード＞

{-# OPTIONS --cubical #-}
data Torus : Set where
  point : Torus
  line1 : point ≡ point
  line2 : point ≡ point
  square : PathP (λ i → line1 i ≡ line1 i) line2 line2

t2c : Torus → S¹ × S¹
t2c point = (base , base)
t2c (line1 i) = (loop i , base)
t2c (line2 j) = (base , loop j)
t2c (square i j) = (loop i , loop j)

＜Agda の型検査結果＞

$ agda T2.agda

Checking T2 (/tmp/ag/T2.agda).

出典：同上

t2c (line1 i) の i が、区間の変数です。

タロウくん：
・・・パターンマッチの側には、区間が現れる。

専任講師：
構成子を宣言するときには区間を書かず、その構成子を使うときには区間変数が現れる。

Cubical Agda は、そういう設計です。

整理すると

Arend Cubical Agda
高次帰納型を定義できるか できる できる
区間が住む場所 通常の型と同じ Setω（階層の外）
構成子の宣言で区間を使えるか 使える 使えない
等式の型で宣言できるか できる できる
除去の側で区間変数を使うか 使う 使う

タロウくん：
・・・「できない」ではなく、「書き方が違う」。

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

そして、一般的な図式について

タロウくん：
先ほど、公式論文が「一般的な図式を容易に定式化できる」と述べていました。

Cubical Agda には、その図式がないのですか。

専任講師：
あります。

Agda の公式ドキュメントは、こう述べています。

（原文引用）

This is what makes the general schema for higher inductive types work, following the CHM paper.

（筆者による日本語訳）

これによって、CHM 論文に従った、高次帰納型のための一般的な図式が機能する。

出典：Cubical, Agda Documentation

タロウくん：
・・・Cubical Agda にも、一般的な図式がある。

専任講師：
Arend 公式論文が「自明でない」と述べているのは、HoTT Book の方式についてです。

Cubical Agda ではなく、教科書の方式との比較です。

タロウくん：
・・・そこを混ぜてはいけない。

専任講師：
３つの方式を並べます。

方式 道の構成子の宣言 一般的な図式
HoTT Book 等式の型として 公式論文は「定式化が自明でない」と述べている
Cubical Agda 等式の型として CHM 論文の図式に従う
Arend 区間を引数に取る構成子として 公式論文は「容易に定式化できる」と述べている

タロウくん：
・・・Cubical Agda も、図式を持っている。

専任講師：
どちらも図式を持ちます。そこに至る道筋が違うのです。

円周は、どのホモトピーレベルにも収まらない

pic_7.jpg

専任講師：
最後に、円周がどこに位置するかを見ておきます。

タロウくん：
・・・第４回目の記事で扱った、宇宙の表ですね。

専任講師：
過去の記事で論じた内容の振り返りになりますが、ここで改めて解説します。

Arend の宇宙は、２つの数で指定されます。縦軸が大きさ、横軸がホモトピーレベルでした。

ホモトピーレベルは、等しさの根拠が何本ありうるかを表す階層です。

名前 ホモトピーレベル 意味
\Prop $-1$ 要素が高々１つしかない型
\Set0 $0$ 等しさの根拠が高々１本の型
\1-Type0 $1$ 等しさの根拠どうしの等しさが、高々１本

タロウくん：
・・・円周は、どこに入るのですか。

専任講師：
どこにも入りません。

タロウくん：
・・・入らない。

専任講師：
円周の上では、一周する道、二周する道、三周する道が、それぞれ別の道でした。

そして、その道どうしの関係も無限に増えていきます。

等しさを何回重ねても、「高々１本」に落ち着きません。

（原文引用）

We say that a type is of homotopy level ∞ if no such k exists.

（筆者による日本語訳）

そのような k が存在しないとき、その型はホモトピーレベル無限大であるという。

出典：Fedor Part, Valery Isaev, Sergey Sinchuk, "Theorem prover Arend"

タロウくん：
・・・本連載シリーズの第４回目の記事で、この型の存在に触れていました。

専任講師：
円周が、その実例です。

そして、この型を扱えることが、HoTT が空間を扱えることの中身です。

本記事を振り返って

タロウくん：
・・・整理させてください。

Haskell の data は、値の作り方だけを並べるものでした。

専任講師：
型理論では、ほとんどすべての型がそこから作られています。

タロウくん：
しかし、$1/2$ と $2/4$ を同じものとして扱うことができなかった。

専任講師：
そこで、等式の構成子を並べます。

タロウくん：
２つの値を同一視する、という１行。それが高次帰納型でした。

| same (a b k : Nat) : q a b = q (a Nat.* k) (b Nat.* k)

$\dfrac{a}{b} = \dfrac{a \times k}{b \times k}$ という主張を、型の定義に書き込む。そういう１行です。

専任講師：
そして、同じ仕組みで図形を記述することができます。

タロウくん：
点をひとつ置き、その点から自分自身への道をひとつ置く。それだけで円周になる。

専任講師：
Arend では、その定義を区間を使って記述します。

タロウくん：
・・・本連載シリーズの第２回目の記事で、区間を普通の型として置いたからですね。

専任講師：
仕様を単純に保った代わりに、計算しきる力を手放しました。

その単純さが、高次帰納型の定義の単純さを生んでいます。

タロウくん：
・・・何かを手放して、何かを得る。

専任講師：
本連載シリーズを通じて、その形が繰り返し現れます。

次回の予告

【Arend Theorem Prover 連載（６回目）】では、宇宙の設計を扱います。

本記事で、円周がどのホモトピーレベルにも収まらないことを見ました。

では、そのホモトピーレベルとは何なのか。

本連載シリーズの第４回目の記事では、２つの軸を持つ表として紹介しました。第６回では、その仕組みをコードで詳しく見ます。

Agda や Lean では、ある型が集合であることを使いたいとき、その証明を関数から関数へ渡し続ける必要があります。

Arend では、その必要がありません。
その理由は、宇宙の設計にあります。

そして、Arend の開発者自身が、その設計思想を公開時に語っているのです。

連載リンク

関連記事

【発展篇】中上級者向けのコラム

この記事は分かりやすい入門者向けの記事を心がけましたので、厳密な議論を犠牲にした部分があります。

以下、中上級者向けに補足説明すべき箇所を、本文の部ごとに分けて述べます。

第１部・第２部について

📌 中上級者向け：「ほとんどすべてが帰納型」は、どこまで一般的な言い方か

本文では、Lean の公式ドキュメントを引いて「宇宙と依存関数型を除けば、すべてが帰納型である」と述べました。

この記述の範囲を、補います。

引用が述べる範囲

本文で引いた文は、Lean のライブラリにおいて、宇宙と依存関数型を除く具体的な型や型構成子の多くが帰納型の実例だ、という趣旨です。

自然数、リスト、真偽値、等しさなどを実際に帰納型として扱えることを強調しています。

一般の型理論については

「すべての型理論で、ほとんどすべてが帰納型である」と一律に言えるわけではありません。

理論や処理系によって、次のものの扱いは異なります。

# 扱いが異なるもの
① 商型
② 余帰納型
③ 部分型
④ 古典公理
⑤ 型宇宙

Arend では、区間型 I が特別な位置を占めています。 本文の第６部で扱ったとおりです。

入門記事で伝えたい点

それでも、依存型を持つ定理証明支援系では、帰納型が非常に中心的な構成手段であることは確かです。

本記事では、普段は単にデータを作る道具に見える data が、型理論の大きな部分を支えていることを伝えるために、この表現を用いています。

📌 中上級者向け：`\Set0` と `\Prop` の「高々１つ」は何を数えているのか

本文の記号一覧表では、\Prop を「要素が高々１つしかない型を集めた場所」、\Set0 を「等しさの根拠が高々１本の型を集めた場所」と説明しました。

同じ「高々１つ」でも、数えているものが違います。

\Prop が数えるもの

\Prop は、要素が高々１つしかない型を集める宇宙です。

命題が真であることの証明は、あっても本質的に区別しない、という考えに対応します。

タロウくんの理解でいえば、「証明の違いを見ない」ということです。

\Set0 が数えるもの

\Set0 では、型の要素そのものが１つとは限りません。

たとえば自然数には $0, 1, 2, \ldots$ と多くの要素があります。

ここで高々１つなのは、任意の２つの要素のあいだの等しさの根拠です。

等しさの根拠どうしを、さらに区別しない型を考えます。

並べると

何が高々１つか 例
\Prop 要素そのもの 「この数は偶数である」という主張
\Set0 等しさの根拠 自然数、文字列、真偽値

例

自然数の $3 = 3$ には、表現を変えた証明を複数記述できるように見えるかもしれません。

しかし集合として扱う型では、それらの等しさの根拠は互いに等しいものとして扱われます。

一方、円周 S1 は base = base に非自明な道を持つため、集合としては扱えません。

本文の第７部で扱った「どのホモトピーレベルにも収まらない型」が、その例です。

本文の目的

入門段階では、次のように捉えると十分です。

捉え方
\Prop 証明の違いを見ない
\Set0 要素は複数あってよいが、等しさの証拠の細部は見ない

本連載シリーズの第４回目の記事で、この階層を詳しく扱いました。

📌 中上級者向け：帰納型の厳密な定義について

本文では、帰納型を「構成子を並べることで定義される型」と説明しました。そして、その型の値は「構成子を有限回組み合わせて作れるものに限られる」と述べました。

これは直感的な説明であり、形式的な定義ではありません。

型理論では、帰納型は始代数として特徴づけられます。構成子の集まりから作られる関手について、その始代数が帰納型にあたります。

この定式化により、次の２つが同時に保証されます。

性質 意味
no junk 構成子で作れないものは、その型に属さない
no confusion 異なる構成子で作った値は、異なる値である

本文の「構成子で作れるものが、すべてです」は、この２つを合わせた直感的な言い換えです。

そして、高次帰納型ではこの特徴づけが変わります。 経路構成子によって、異なる構成子で作った値が同一視されうるためです。no confusion が、そのままの形では成り立ちません。

📌 中上級者向け：依存関数型と依存和型

本文では、依存関数型（$\Pi$ 型）を扱いました。

依存型理論には、もうひとつの基本的な型があります。依存和型（$\Sigma$ 型）です。

$\Pi$ 型が「引数の値によって返す型が変わる関数」を表すのに対し、$\Sigma$ 型は「第１成分の値によって第２成分の型が変わる組」を表します。

Arend では \Sigma と記述します。本連載シリーズの第４回目の記事で扱いました。

何を表すか 論理でいえば
$\Pi$ 型 依存関数 すべての〜について
$\Sigma$ 型 依存する組 〜が存在する

本文で引用した Lean の記述に「依存関数型以外のすべての型構成子は帰納型である」とありました。

$\Sigma$ 型は、この記述では帰納型に含まれます。実際、Lean では Sigma が structure として定義されています。

第３部について

📌 中上級者向け：厳密に有理数を定義するなら、何を追加するのか

本文の Q は、「分子と分母に同じ数を掛けて表し直したものを結ぶ」という考え方を示すための、小さな例です。

same 1 2 2 によって q 1 2 = q 2 4 を作れるので、経路構成子が何をするかは、この例だけで十分に見えます。

ただし、数学でいう有理数全体を厳密に作るには、もう少し条件が要ります。

分母が $0$ であってはいけません

本文のコードでは、分母に何を渡しても構いません。q 1 0 と書けてしまいます。

しかし $1/0$ は、通常の分数として扱いません。

有理数を定義するには、分母が $0$ でないという条件を型に持たせる必要があります。

掛ける数も $0$ であってはいけません

本文で扱ったとおりです。k = 0 を許すと、型全体が潰れます。

suc k とするか、$k \neq 0$ という条件を持たせます。

同じ数を表す組を、どう結ぶか

有理数では、通常、分母が $0$ でない整数の組 $(a, b)$ を用います。

そして、次の条件で同一視します。

$$ad = bc \quad \Longrightarrow \quad (a, b) \text{ と } (c, d) \text{ は同じ有理数}$$

本文で扱ったたすきがけの条件です。

そのほかに決めること

# 決めること
① 符号をどちらに持たせるか（分子か、分母か）
② 分母を正にそろえるか
③ 既約分数を代表元に選ぶか

どれも、有理数ライブラリを実装するときに判断が要る点です。

本記事の例の役割

本記事の目的は、有理数ライブラリを完成させることではありません。

「通常の構成子で値を作るだけでなく、経路構成子で値どうしの関係を型の中に記述できる」という仕組みを見ることです。

その目的では、$1/2$ と $2/4$ を結ぶこの最小例が、最も見通しのよい入口になります。

📌 中上級者向け：ここでの `Group` は、なぜ群の公理を省略しているのか

本文では、Group に法則を書き加えた版と、省いた版の両方を示しました。

以降のコードでは、省いた版を使っています。

省いている理由

本文の Group は、Bool 側と Bit 側で、対応する要素・演算・単位元・逆元の形を並べて見るための簡略化した構造です。

そこで示したいのは、２つの型のあいだに往復する対応を作り、一価性によって型の等しさへ進む流れです。

法則の証明を列挙すると、その流れが見えにくくなります。

通常の群に必要なもの

数学でいう群には、演算、単位元、逆元だけでなく、次の法則も必要です。

法則 内容
結合律 $(x \cdot y) \cdot z = x \cdot (y \cdot z)$
単位元律 $e \cdot x = x$ かつ $x \cdot e = x$
逆元律 $x^{-1} \cdot x = e$ かつ $x \cdot x^{-1} = e$

本文では、左側の法則だけを書き加えました。 右側も同様に必要です。

この例では、実際に成り立ちます

Bool と xor、Bit と xor。どちらも、２要素の群の法則を満たします。

本文で示したとおり、必要な証明を追加すれば、両者を本来の意味で群として形式化できます。

読み方

本文の Group は、「群の完全な定義」ではなく、「群の例で現れるデータの骨組み」です。

群そのものを厳密に形式化する場合には、法則も型の中に持たせることになります。

本連載シリーズの第４回目の記事で、その形を詳しく扱いました。

📌 中上級者向け：同型から型の等しさが出るのは、なぜか

本文では、iso に４つのものを渡すことで Bool = Bit を示しました。

その４つが何をしているのかを、補います。

本文で作ったもの

f は Bool から Bit への対応、g は逆向きの対応です。

gf と fg は、往復すれば元へ戻ることを示しています。

この４つによって、Bool と Bit のあいだの同型、より正確には型の同値を与えています。

同値と等しさは、別の段階です

通常、２つの型のあいだに往復できる対応があることと、２つの型が等しいことは、別の主張です。

たとえば集合論では、要素数が同じ２つの集合があっても、集合として同一とは限りません。

本連載シリーズの第１回目の記事で扱った論点です。

一価性がすること

ホモトピー型理論の一価性は、型の等しさと型の同値が対応する、と述べます。

Arend の path (iso f g gf fg) は、作った同値から型の等しさを取り出す箇所です。

本文で「４つが揃えば型は等しい」と読めるのは、Arend がこの一価性を使える体系だからです。

高次帰納型との違い

何を扱うか
高次帰納型 ある１つの型の内部にある、値どうしの経路
一価性 型そのものどうしの等しさ

どちらも等号型を扱いますが、見ている階層が異なります。

📌 中上級者向け：setoid と商型の関係を、厳密にいうと

本文では、setoid を「型と、その型の上の同値関係を組にしたもの」と説明しました。

より正確には、setoid の圏と商型の関係は、次のように整理されます。

型と同値関係の組を対象とし、同値関係を保つ関数を射とする圏を考えます。この圏において、商を取る操作は、忘却関手の左随伴として特徴づけられます。

商型を持つ体系では、この随伴が型理論の内部で実現されます。

setoid 方式では、その随伴を利用者が手作業で扱うことになります。「関係を持ち回る」という本文の表現は、この作業を指しています。

なお、setoid には「setoid モデル」という別の役割もあります。 型理論の意味論として、外延性を持つ型理論を内包的な型理論の上で解釈する手法です。本文で扱った実務上の方式とは、別の論点です。

📌 中上級者向け：Coq が商型を持たない理由

本文で引用した論文は、Coq が商型を持たない理由を「型検査が決定不能になるため」と述べています。

この記述を、少し補います。

商型を素朴に導入し、商の等しさを判定的な等しさとして扱うと、型検査器は「２つの値が同値関係にあるか」を判定する必要が生じます。

その同値関係が任意のものである以上、判定が停止する保証はありません。

そのため、商型を持つ体系では、次のいずれかの設計が採られます。

設計 例
商の等しさを、命題としてのみ扱う Lean 4 の Quot
経路として扱い、計算規則を与える Arend、Cubical Agda
商型を導入しない Rocq／Coq

Lean 4 の Quot が型検査を決定可能に保っているのは、Quot.sound が命題レベルの等しさを与えるだけで、判定的な等しさには影響しないためです。

本記事では、この違いに深入りしていません。

第４部・第５部について

📌 中上級者向け：`idp` と `loop` は何が違うのか

本文では、idp と loop を「別の根拠」と述べました。

この言い方を、少し正確にします。

本文での比較の意味

idp は、ある値が自分自身と等しいときに使える、何も動かない道です。

loop は base = base という同じ型に対して、円周を表すために宣言で追加した道です。

本文では、この２つを比べることで、「点の情報だけでなく、点を結ぶ道にも情報がある」ことを示しています。

「別に与える」とは

loop は idp から計算で出てきたものではありません。

\data S1 の宣言が、base に加えて loop という経路構成子を明示的に与えます。

この意味で、loop は idp とは別に指定された、円を一周することを表す道です。

「異なると証明する」は、別問題です

一方で、内部の型理論だけを見て直ちに $\text{loop} \neq \text{idp}$ を証明できるかは、別の問いです。

その区別には、型のモデルや追加の原理を使う議論が関わります。

具体的には、円周の基本群が $\mathbb{Z}$ であることを示す議論が必要になります。

入門段階では、「loop は idp と別に導入された生成的な道である」と捉えるのが適切です。

道は２本だけではありません

また、円周の自己経路は idp と loop の２本で尽きるわけではありません。

loop を続けてたどる、逆向きにたどる、といった合成も考えられます。

本文の「２つ」は、最初に比べる２つの代表的な道を指しています。

発展的には、それらの繰り返しが整数と対応し、円周の基本群が $\mathbb{Z}$ になる話へつながります。

📌 中上級者向け：一点と一本のループが、なぜ円周を表せるのか

本文では、点をひとつ置き、その点から自分自身への道をひとつ置くだけで円周になると述べました。

この点を、補います。

点集合として数えているわけではありません

ここでの S1 は、平面に描かれた円周上の点を、１個ずつ列挙する定義ではありません。

base が１つだけあるからといって、「円周に点が１つしかない」と主張しているわけでもありません。

見るのは、形のつながり方です

ホモトピー型理論では、型を空間のようなものとして読みます。

そのとき大切なのは、点が何個見えているかだけではなく、点どうしを結ぶ道がどう存在するかです。

base に loop : base = base を加えると、「出発点へ戻る一周の道を持つ空間」という情報が入ります。

CW複体との対応

位相幾何では、円周は次のように作れます。

順 手順
① 一点、すなわち $0$ 次元の部品を１つ置く
② その点の両端につながる、１本の $1$ 次元の部品を貼り付ける

base と loop の宣言は、この作り方を型理論の言葉で表したものだと見ることができます。

本文の第６部で扱った「ひもの両端を、同じ場所に留める」という説明が、まさにこの手順です。

何が「円周」なのか

より厳密には、この高次帰納型は、普通の幾何学的な円周と同じホモトピー型を表すモデルです。

長さ、半径、平面上の位置といった情報は持ちません。

その代わり、穴を１つ持ち、一周するループが縮められないという、円周の位相的な特徴を捉えます。

📌 中上級者向け：命題切断と集合切断とは何か

本文で引いた論文は、高次帰納型の例として円周のほかに命題切断と集合切断を挙げています。

どちらも、等しさの根拠を意図的に潰すための高次帰納型です。

命題切断

命題切断（propositional truncation）とは、どの２つの要素も同一視してしまう構成です。

型 $A$ から作り、$|A|$ と書きます。

＜Arend のコード＞

\data PTrunc (A : \Type)
  | inP A
  | squashP (x y : PTrunc A) (i : I) \with {
    | x, y, left => x
    | x, y, right => y
  }

inP が、もとの型の要素を運び込む構成子です。

squashP が、どの２つの要素のあいだにも道を１本引く構成子です。

＜Arend のコード＞

\data Bool | true | false

\func a : PTrunc Bool => inP true
\func b : PTrunc Bool => inP false
\func same : a = b => path (squashP a b)

＜Arend の型検査結果＞

$ java -jar Arend.jar TRUNC.ard

--- Typechecking \default ---
[ ] src.TRUNC
--- Done (131ms) ---

もとの Bool では true と false は別の値でした。しかし PTrunc Bool では、等しくなります。

どの２つの要素についても、同じことが示せます。

＜Arend のコード＞

\func anyTwo (x y : PTrunc Bool) : x = y => path (squashP x y)

＜Arend の型検査結果＞

$ java -jar Arend.jar TRUNC2.ard

--- Typechecking \default ---
[ ] src.TRUNC2
--- Done (130ms) ---

その結果、要素は高々１つになります。

何のために使うのか

「存在する」ことだけを述べ、どれが存在するかは伏せたいときに使います。

たとえば「この方程式には解がある」と述べたいが、どの解かは問題にしない場合です。

$\Sigma$ 型で書くと、具体的な解を取り出せてしまいます。命題切断をかけると、取り出せなくなります。

本連載シリーズの第４回目の記事で扱った \Prop が、この切断と対応しています。

集合切断

集合切断（set truncation）とは、どの２つの平行な道も同一視してしまう構成です。

「平行な」というのは、始点と終点が同じ、という意味です。

タロウくんの理解でいえば、こうなります。

何を潰すか
命題切断 要素どうしの区別
集合切断 等しさの根拠どうしの区別

円周では、base = base の根拠が idp と loop の２本ありました。

集合切断をかけると、その２本が同一視されます。

そして、円周は１点に潰れます。

階層でいうと

本連載シリーズの第４回目の記事で扱ったホモトピーレベルと対応しています。

切断 結果として得られる型 ホモトピーレベル
命題切断 要素が高々１つ $-1$（\Prop）
集合切断 等しさの根拠が高々１本 $0$（\Set0）

タロウくん：
・・・上の階層を、下の階層へ落とす操作ですね。

専任講師：
そのとおりです。そして、その操作自体が高次帰納型として定義されます。

本記事では扱いません

本記事の主題は、円周を定義することでした。

命題切断と集合切断は、高次帰納型のもうひとつの使い道です。

どちらも、arend-lib で実際に使われています。

📌 中上級者向け：経路構成子は、等しさの型を定義しているのではありません

本文では、経路構成子を「値どうしの等しさを与える構成子」と説明しました。

「与える」という語を選んだのには、理由があります。

経路構成子は、等しさの型そのものを定義しているのではありません。

$a = b$ という型は、どんな型についても存在します。経路構成子があってもなくても、記述することができます。

確かめてみます。

＜Arend のコード＞

-- 経路構成子を持たない、点ひとつだけの型
\data Point
  | pt

-- pt = pt という型は、記述できる
\func eqType : \Type => pt = pt

-- その値として、idp がある
\func e1 : pt = pt => idp

＜Arend の型検査結果＞

$ java -jar Arend.jar PATHC.ard

--- Typechecking \default ---
[ ] src.PATHC
--- Done (122ms) ---

Point には経路構成子がありません。それでも pt = pt という型は存在し、idp という値を持ちます。

では、円周では何が違うのか。

＜Arend のコード＞

\data S1
  | base
  | loop : base = base

\func e2 : base = base => idp
\func e3 : base = base => loop

base = base という型に、値が２つあります。idp と loop です。

経路構成子がしたことは、この型に値を１つ増やすことでした。

タロウくんの理解でいえば、「等しさの根拠を１本、用意する」ということになります。

そして Point では、loop にあたるものがありません。

＜Arend のコード＞

\func bad : pt = pt => loop

＜Arend の型検査結果＞

[ERROR] src.PATHC2:4:24: Cannot resolve reference 'loop'

「loop という名前を解決できない」と指摘されます。そんな構成子は宣言されていないからです。

用語の使い分けについて

以上を踏まえ、本記事では次のように使い分けています。

動詞 どこで使うか
作る 構成子が、その型の値を作るとき
与える 経路構成子が、等しさの型に値を与えるとき
定義する data の宣言によって、型そのものを定義するとき

「等しさを作る」と書くと、等しさの型そのものを新しく作っているように読めます。

実際には、すでにある型に値を１つ足しているのです。

📌 中上級者向け：高次帰納型の一般的な図式について

本文では、Arend 公式論文が「一般的な図式を容易に定式化できる」と述べていることを引きました。

「一般的な図式」（general scheme）とは何かを補います。

通常の帰納型には、どのような構成子の並びが許されるかを定める規則があります。厳密正値性（strict positivity）などの条件です。

この規則があるおかげで、任意の帰納型について除去規則が自動的に導かれます。

高次帰納型についても、同様の規則が求められます。どのような経路構成子の並びが許されるか。そして、そこから除去規則をどう導くか。

HoTT Book では、個々の高次帰納型を例として挙げるにとどまり、この一般規則は与えられていません。

Cubical Agda は CHM 論文の図式に従い、Arend は条件付き帰納型という形で規則を与えています。

📌 中上級者向け：円周の基本群の証明について

本文では、円周の基本群が整数と同じ構造をなすことに触れ、証明には立ち入らないと述べました。

この定理は、HoTT の初期の重要な成果のひとつです。

$$\pi_1(S^1) = \mathbb{Z}$$

証明の骨格は、次のとおりです。円周の上に、整数を「巻きつける」被覆を構成します。そして、その被覆の全体が可縮であることを示します。

この構成には、一価性が使われます。 整数から整数への「１だけずらす」対応が同値であることから、Nat の上の道を作る場面で必要になります。

HoTT Book の第８章に、この証明が収められています。

本記事では、円周が定義できることまでを扱いました。その上で何が証明できるかは、別の主題です。

📌 中上級者向け：Licata の技法の詳細

本文では、Rocq／Coq と標準の Agda が「Licata の技法」で高次帰納型を模倣していると述べました。

その手順を、もう少し詳しく記します。

順 手順
１ モジュールの中に、点の構成子だけを持つ private inductive type を定義する
２ 道の構成子を、公理として宣言する
３ 除去規則を、モジュール内部のパターンマッチを使って定義する
４ 道の構成子についての計算規則を、公理として宣言する
５ モジュールの外へ、これらを公開する

private inductive type は、モジュールの外からパターンマッチできません。

そのため、利用者は手順３で定義した除去規則を通してしか、この型を使えません。その除去規則が、道の構成子の行も要求するように作られています。

この技法により、点の構成子については判定的な計算規則が得られます。 道の構成子については、公理として足した計算規則が使われます。

ただし、道の構成子の計算規則は判定的ではありません。 その点が、中核で支える方式との違いです。

第６部・第７部について

📌 中上級者向け：条件付き帰納型の一般形

本文では、整数と円周という２つの例で条件付き帰納型を扱いました。

一般形を記しておきます。

構成子は、引数のなかに区間 I の値を取ることができます。そして \with の節で、その引数が left または right である場合の値を指定します。

指定できる条件には、制約があります。

# 制約
① 条件の右辺は、すでに定義された構成子のみを参照できる
② 複数の区間引数を持つ場合、条件は矛盾しないよう整合していなければならない
③ 条件を持つ型からの関数は、その条件を満たすことが検査される

③が、本文で示した Conditions check failed というエラーの正体です。

なお、条件は区間引数に限られません。 本文の整数の例では、Nat の引数について zero の場合の条件を指定しました。

📌 中上級者向け：`Setω` と非ファイブラント型

本文では、Cubical Agda の区間 I が Setω に住むと述べました。

この背景を補います。

立方体型理論では、型は Kan 条件を満たすもの（ファイブラント）と、満たさないもの（非ファイブラント）に分かれます。区間は、後者にあたります。

本連載シリーズの第２回目の記事で扱った二層理論は、この区別を体系のなかに持ち込む設計です。

Agda には、非ファイブラント型という概念がありません。そのため、区間を通常の宇宙階層に置くことができず、階層の外側にある Setω に置いています。

Setω は、もともと宇宙多相な定義を扱うために用意された宇宙です。 区間をそこに置くのは、便宜的な扱いといえます。

Arend では、区間が通常の型として扱われます。 そのため、この問題が生じません。その代わりに、一価性を完全に計算可能にするための構造を備えていません。

📌 中上級者向け：「高次帰納型」と「高次帰納-帰納型」の違い

本文では、高次帰納型を扱いました。

これに似た名前の概念に、高次帰納-帰納型（higher inductive-inductive type、HIIT）があります。

帰納-帰納型とは、２つ以上の型を同時に定義し、一方の定義のなかで他方を参照するものです。

高次帰納-帰納型は、それに経路構成子を加えたものです。

Arend は、公開時からこれを扱えると述べています。Lean、Rocq／Coq、標準の Agda では、中核で支えていません。

本記事では、この概念に踏み込んでいません。 高次帰納型の理解が先だからです。

記事全体について

📌 中上級者向け：本記事のコードの検証環境について

本記事に掲載したコードは、Arend、Haskell、Agda、Lean 4 のすべてを実機で検証しました。

処理系 バージョン
Arend 1.10（Java 21）
GHC 9.4.7
Agda 2.6.3
Lean 4.33.1

型検査の結果とエラーメッセージは、実行時の出力をそのまま掲載しています。

エラーメッセージのファイルパスについて。 本記事に掲載したエラーには、/tmp/ag/S1STD.agda のような検証環境上のパスが含まれています。お手元で実行された場合、この部分は異なります。

Cubical Agda の検証について。 本記事では、標準ライブラリを使わず、Agda.Primitive.Cubical と Agda.Builtin.Cubical.Path を直接読み込む形で検証しました。cubical ライブラリを使う場合、記法が一部異なります。

Rocq／Coq については、執筆環境に処理系を用意できませんでした。

Licata の技法についての記述は、査読論文の記載に基づくものです。

📌 中上級者向け：訳語について

本記事で用いた訳語のうち、日本語として定着していないものがあります。原語を併記しておきます。

訳語 原語 備考
高次帰納型 higher inductive type 「高次帰納的型」と訳す文献もあります
経路構成子 path constructor ──
条件付き帰納型 inductive type with conditions Arend 固有の語です
除去規則 elimination rule ──
構成子 constructor ──
依存関数型 dependent function type $\Pi$ 型とも呼ばれます
非ファイブラント non-fibrant ──
setoid setoid 定訳がないため、原語のまま用いました

訳語の選定にあたっては、上村太一氏『ホモトピー型理論』を参考にしました。

なお、本連載シリーズの第３回目の記事では「高次帰納的型」と表記しました。 本記事では「高次帰納型」に統一しています。

出典一覧

Arend

Cubical Agda

setoid と商型

Lean・Coq の HoTT 対応

型理論における帰納型・高次帰納型

ホモトピー型理論

検証環境

本記事に掲載したコードは、次の処理系で実機検証しました。

処理系 バージョン
Arend 1.10（Java 21）
GHC 9.4.7
Agda 2.6.3
Lean 4.33.1

型検査の結果とエラーメッセージは、実行時の出力をそのまま掲載しています。

Rocq／Coq については、執筆環境に処理系を用意できませんでした。 Licata の技法についての記述は、査読論文の記載に基づくものです。

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?