2025-11-15T20:46:11.945579

On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions

Urciuoli

We develop formal theories of conversion for Church-style lambda-terms with Pi-types in first-order syntax using one-sorted variables names and Stoughton's multiple substitutions. We then formalize the Pure Type Systems along some fundamental metatheoretic properties: weakening, syntactic validity, closure under alpha-conversion and substitution. Finally, we compare our formalization with others related. The whole development has been machine-checked using the Agda system. Our work demonstrates that the mechanization of dependent type theory by using conventional syntax and without identifying alpha-convertible lambda-terms is feasible.

academic

単一ソート変数名と多重置換を用いた純型システムの形式的メタ理論について

基本情報

論文ID: 2510.12300
タイトル: On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
著者: Sebastián Urciuoli (Universidad ORT Uruguay, ウルグアイ)
分類: cs.LO (計算機科学における論理)
発表会議: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2025)
論文リンク: https://arxiv.org/abs/2510.12300
コードリンク: https://github.com/surciuoli/pts-metatheory

概要

本論文は、Π型を備えたChurch様式のλ項に対する変換の形式理論を開発した。一階構文、単一ソートの変数名、およびStoughtonの多重置換を使用している。その後、純型システム(Pure Type Systems, PTS)および基本的なメタ理論性質を形式化した：弱化、構文的妥当性、α変換下での閉包性、および置換。最後に、関連する形式化研究と比較した。全体の開発はAgdaシステムを用いて機械検証されている。本研究は、従来の構文を使用し、α変換可能なλ項を同一視しない依存型理論の機械化が実行可能であることを実証している。

研究背景と動機

問題背景

形式化の課題: 依存型理論の機械検証は常に課題であり、特に変数束縛とα等価性の処理において困難である
構文選択のジレンマ: 既存の方法は通常、de Bruijn指数または二重ソート変数名を採用して名前キャプチャの問題を回避するが、これらの方法は実装との乖離がある
置換操作の複雑性: 従来の単項置換の定義は非構造的に再帰的であり、機械検証では複雑な帰納法が必要である

研究動機

スケーラビリティの検証: Stoughton置換理論に基づくフレームワークがより複雑な言語(PTS等)に拡張可能かどうかを検証する
理論と実践のギャップ縮小: 従来の単一ソート変数名構文を使用し、実際の型チェッカー実装に近づける
証明方法の簡略化: α変換定義の改善により、主要補題をより単純な構造的帰納法で証明する

核心的貢献

Stoughton置換フレームワークの拡張: 元の純λ計算フレームワークをChurch様式λ抽象とΠ型に対応するよう拡張
改善されたα変換定義: 新しいα変換定義を提案し、主要補題が構造的帰納法で証明可能に
PTSメタ理論の形式化: PTSの基本メタ理論性質の機械検証：弱化、構文的妥当性、α変換閉包性、置換閉包性
等価性証明: 一般化帰納を用いた無限規則系と標準有限規則系の等価性を証明
完全なAgda実装: 約3000行のコードによる完全な機械検証を提供

方法の詳細

構文定義

論文は従来の一階構文を用いてλ項を定義している：

data Λ : Set where
  c : C → Λ                    -- 定数
  v : V → Λ                    -- 変数  
  λ[_:_]_ : V → Λ → Λ → Λ      -- Church様式λ抽象
  Π[_:_]_ : V → Λ → Λ → Λ      -- Π型
  _·_ : Λ → Λ → Λ              -- 適用

選択関数と置換

核心的な革新は、選択関数を用いてStoughtonの多重置換を使用し、名前キャプチャを回避することである：

X : Res → V
X (σ, xs) = X' (concat (map (fv ∘ σ) xs))

置換操作は構造的再帰として定義される：

λ[ x : A ] M • σ = λ[ y : A • σ ](M • σ , x := v y) 
  where y = X (σ , fv M - x)

改善されたα変換定義

新しいα変換定義は再帰的定義ではなく構文的等価性を使用する：

∼λ : ∀ {x x' y A A' M M'} → A ∼α A' → y ∉ fv M - x → y ∉ fv M' - x'
   → M [ x := v y ] ≡ M' [ x' := v y ] → λ[ x : A ] M ∼α λ[ x' : A' ] M'

PTS型システム

一般化帰納を用いてPTSを定義し、主要規則は以下を含む：

⊢abs : Γ ⊢ A : s₁ → ∀z → z ∉ domΓ → Γ,z : A ⊢ B[y := z] : s₂
     → ∀z → z ∉ domΓ → Γ,z : A ⊢ M[x := z] : B[y := z]
     → R s₁ s₂ s₃
     → Γ ⊢ λ[x : A]M : Π[y : A]B

技術的革新点

1. 制約型の再定義

制約をSub × ΛからSub × List Vに再定義し、より大きな柔軟性を提供：

Res = Sub × List V

2. 構造化されたα変換証明

主要補題iotaAlphaは構造的帰納法で証明可能に：

iotaAlpha : ∀ {M M'} → M • ι ≡ M' • ι → M ∼α M'

3. 適用規則の強化された前提条件

適用規則に型妥当性前提を追加し、後続の証明を簡略化：

⊢app : Γ ⊢ M : Π[x : A]B → Γ ⊢ N : A → Γ ⊢ B[x := N] : s
     → Γ ⊢ M·N : B[x := N]

実験設定

形式化環境

証明支援系: Agdaシステム
コード規模: 約3000行
モジュール分割: フレームワークとPTSメタ理論が各々半分

検証内容

基礎理論: 置換操作の性質、α変換の等価性
PTSメタ理論: 弱化、構文的妥当性、閉包性定理
等価性: 無限規則系と有限規則系の等価性

実験結果

主要成果

完全な機械化: PTSの核心的メタ理論性質の機械検証に成功
証明の簡略化: すべての結果(α変換の完全性を除く)が構造的帰納法で証明される
コード効率: 3000行のコードで完全な理論を実装し、他の研究と比較してより簡潔

主要定理

補題4.1 (弱化): thinning : ∀ {Γ Δ M A} → Γ ⊆ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M : A
補題4.3 (構文的妥当性): syntacticValidity : ∀ {Γ M A} → Γ ⊢ M : A → ∃ λ s → A ≡ c s ⊎ Γ ⊢ A : c s
補題4.4 (α変換閉包性): closAlphaAsg : ∀ {Γ Δ M N A} → Γ ≈α Δ → M ∼α N → Γ ⊢ M : A → Δ ⊢ N : A
補題4.6 (置換閉包性): closureSub : ∀ {Γ Δ M A σ} → σ : Γ ⇀ Δ → Δ ok → Γ ⊢ M : A → Δ ⊢ M • σ : A • σ