Nominal Type Theory by Nullary Internal Parametricity

技術的概要：Nullary 内部パラメトリシティによる名目型理論

問題提起
ラムダ計算などのバインダを持つ言語の構文を形式化する際には、$\alpha$-同値、名前の抽象化、および鮮度（freshness）の扱いが必要となる。名目枠組みは「名前抽象化」型（$\@N \multimap -$ と表記）を用いてこれに対処する。しかし、既存のアプローチにはトレードオフが存在する：

1. 存在論的提示（Existential Presentation）： 抽象化を名前と項のペア $\langle x, a \rangle$ として扱う。これは便利な「名目パターンマッチング」（バインダの分解）を可能にするが、複雑な鮮度の伝播を必要とする煩雑な型付け規則という欠点がある。
2. 全称的提示（Universal Presentation）： 抽象化を鮮な名前を消費する関数（アフィン関数）として扱う。これはクリーンな推論規則を提供するが、名目パターンマッチングを行う能力が欠如しているように見える。

現在の名目枠組みは、このギャップを埋めるために外部のセマンティクス（例えば名目集合）や複雑な内部メカニズムに依存することが多い。本論文は、全称的提示のクリーンな規則と存在論的提示のパターンマッチング能力を統合し、完全に型理論的な設定内で実現する基盤を求めようとするものである。

手法
著者らは、Nullary 内部パラメトリック型理論（nullary PTT） に基づいた依存型理論であるパラメトリック名目型理論（PNTT） を提案する。このアプローチは、Cavallo と Harper（CH）の二項内部パラメトリック型理論を、パラメトリシティの次数を 2 から 0 に削減することで適応させたものである。

核心的な手法は以下の通りである：

1. Nullary ブリッジ： 標準的な二項パス/ブリッジ型を nullary ブリッジに置き換える。Nullary ブリッジ $q : \text{Bridge } A \dots$ は、ブリッジ区間 $\@N$ からのアフィン関数として扱われる。これらのブリッジは「鮮な」変数を表す。
2. 構造抽象化原理（SAP）： 理論は SAP によってパラメトリシティを内部化し、型 $K$ とその「ブリッジ型」$\@N \multimap K$ の間の同値性を確立する。重要なのは、SAP がブリッジ型形成子を他のすべての型形成子と可換であると主張することである。
3. 名前帰納： ブリッジ区間 $\@N$ は、第一級の名前型 $\text{Nm}$ に拡張される。新しい消去子である名前帰納（$\text{ind}_{\text{Nm}}$）が導入される。これにより、名前 $n$ に対する場合分けが可能となる：$n$ が現在スコープ内にある特定のアフィン変数 $x$ である場合、または $x$ が $n$ において鮮である場合である。
4. 名目データ型： 非定型ラムダ計算の構文などの標準的な名目データ型は、名前を引数として取りうる構成子を用いて定義される。

主要な貢献

1. 名目パターンマッチングの回復： 論文は、通常存在論的抽象化に関連する名目パターンマッチングが、全称的設定でも回復可能であることを示す。名目データ型 $D$ に SAP を適用することで、ブリッジ型 $\@N \multimap D$ が「パラメトリック変換」$D_1$（例えば $Ltm_1$）と同値であることが示される。$D_1$ には明示的な「穴」構成子が含まれる。したがって、$D$ 内のバインダに対するパターンマッチングは、$D_1$ に対する帰納に還元され、その「穴」の場合が束縛変数に対応する。
2. 統合されたプリミティブ： 著者らは、PNTT が自然に以下をサポートすることを示す：
   • 全称名前抽象化： Nullary ブリッジ型を通じて。
   • 型としての鮮度： 特定の名前が鮮であることを分類する $\text{Gel}$ 型を通じて。
   • 存在論的抽象化： SAP と鮮度型を通じて非原始的に導出される。
   • 名前交換と局所スコープ： アフィン関数と $\nu$-バインダ（$\text{ung}(\lambda x. t)$ として実装）を用いて実装される。
3. 合成クリッキー・パラメトリシティ： 論文は、nullary パラメトリシティをクリッキー二項パラメトリシティと結びつける。名目推論のための nullary パラメトリシティと、標準的な二項パラメトリシティ公理を組み合わせることで、著者らはクリッキーモデルを模倣する。これは、非定型ラムダ計算の De Bruijn 構文とその高次抽象構文（HOAS）エンコーディングの間の同値性を証明することで示される。
4. 名前における構造抽象化原理（SAP）： $\@N \multimap \text{Nm} \simeq 1 + \text{Nm}$ であることを示す具体的な証明が提供される。この同値性は、名前帰納原理とパターンマッチングの回復の中核をなす。

結果

• 理論的健全性： 著者らは、Psh($\square_2 \times \square_0$) というプレシフ圏における PNTT のセマンティックモデルを提供する。ここで $\square_0$ は有限順序数と単射の圏（Schanuel トポスの基底）である。これにより、システムの整合性が確認される。
• 実装の可行性： 論文は、二項 CH 理論が Cubical Agda で実装されているため、PNTT（本質的には nullary CH ＋ 名前帰納）の実装も可能であると主張する。
• ケーススタディ：
  • $\pi$-計算の代入： 著者らは、束縛パターンにマッチングすることで $\pi$-計算プロセスの代入関数を定義し、SAP ベースのアプローチの実用性を示す。
  • HOAS の適切性： 外部の二項パラメトリシティ公理に依存する証明の概要が示され、ラムダ計算の名目構文とその HOAS エンコーディングが同値であることを示す。これは Atkey のクリッキー・パラメトリシティの結果を反映する。

意義と主張
本論文は、存在論的および全称的な名前抽象化の間の歴史的な緊張関係を解決する「正当な名目枠組み」を提供すると主張する。

• 統合： 外部メタ理論を必要とすることなく、全称抽象化のクリーンな推論規則と、存在論的抽象化の実用的なパターンマッチング能力を統合する。
• 内部化： 従来のアプローチではパラメトリシティがメタ理論的性質であったのに対し、PNTT は SAP によってパラメトリシティを内部化し、パラメトリシティの結果を理論内で証明可能にする。
• 新規性： 著者らは、名目型理論の基盤としてnullary パラメトリシティを明示的かつ積極的に利用したのは初めてであると述べる。
• 謙虚さ： 論文は限界を認めている。複雑な項に対する SAP の証明は「扱いにくく」、現在では項構造の手動再現を必要とする。著者らは、将来の研究として SAP 証明の構築を自動化するか、明示的な SAP 証明の必要性を回避するために（Narya 証明支援系におけるような）「観察的」な PNTT 版へ移行することを提案している。また、完全な FreshMLTT の名前交換規則（代入との可換性）は、その場限りの制限なしにはまだ完全に受け入れられていないとも指摘している。

要約すると、本論文は、nullary 内部パラメトリシティを名目型理論の堅牢な基盤として確立し、バインダ、鮮度、パターンマッチングを単一の整合的な型理論システム内で処理する原理的な方法を提供するものである。