古典論理の証明図変形の停止性と合流性

古森雄一 (千葉大学理学部)

次の λρ-計算は古典論理の含意断片の自然演繹体系である。

定義 0.1 ( 型なし λρ-項 ) 可算無限個の λ-変数, ρ-変数が与えられているものとする。 λ-変数, ρ-変数をまとめたものを項変数とよぶ。

1. 項変数は λρ-項である。

2. M, N が λρ-項ならば (MN) は λρ-項である。

3. M が λ-項, f が項変数ならば (λf.M) は λρ-項である。

変数 a が ρ-変数のとき, λa.M を ρa.M と表記する。正規型にするための変形規則は次のようなものである。

定義 0.2 ( ρβ-contraction ) ρβ-redex は以下で与えられる左辺の形をした λρ-項で, その contractum は対応する右辺の形をした λρ-項である。

\begin{matrix}(aM)N & ⊳_{1ρβ} & (aM) \\ (λx.M)N & ⊳_{1ρβ} & [N/x]M \\ (ρa.M)N & ⊳_{1ρβ} & ρa.(λx.[λy.a(yx)/a](Mx))N \end{matrix}

この ρβ-reduction の体系は合流性 (Church-Rosser 性) が成り立ち, その証明も容易である。以下の TA_{λ}ρ (これが古典論理の含意断片の体系) が λρ-項の型付の体系である。

定義 0.3 ( The system TA_{λρ} ) TA_{λρ} の推論規則は以下の 4 つである。

\begin{matrix}M : α → β & N : α \\ MN : β \end{matrix} {x : α \atop Π} ; M : β ; λx.M : α → β {M : α \atop aM : β} {Q : α \atop aQ : β} ; Π ; M : α ; ρa.M : α

体系 TA_{λ}ρ で型付可能な λρ-項については強正規化定理が成り立つ。当然, 弱正規化定理も成り立つのであるがその直接証明が (今のところ) できない。次の変形規則を付け加えると弱正規化定理が容易に証明できる。

定義 0.4 ( ∗ρβ-contraction ) ∗ρβ-contraction は ρβ-contraction に次の 3 つの contraction を付け加えたものである。

\begin{matrix}N(ρa.M) & ⊳_{1∗ρβ} & ρa.(λx.[λy.a(xy)/a](xM))N \\ λx.(ρa.M) & ⊳_{1∗ρβ} & ρa.(λx.[λy.a(λz.y)/a]M) \\ ρa.(ρb.M) & ⊳_{1∗ρβ} & ρa.[a/b]M \end{matrix}

しかしこの体系では合流性が成立しない (藤田憲悦 (島根大) 氏指摘)。また, 古典論理の変形規則は η-reduction とも相性が悪く ρβ-reduction + η-reduction の体系は合流性が成立していないようである。合流性が成り立っていない体系がつぶれない (reduction で移れるものを等しいとみなしたときに x = y が出ない) かどうかは興味深い問題である。

問題 0.5 ( ∗ρβ-contraction )

1. 体系 ∗ρβ はつぶれないか?

2. 体系 ρβ + η はつぶれないか?

どちらも型なしでつぶれる場合は型付ではどうか?

新しい進展があったら以下に載せる予定である。 http://www.math.s.chiba-u.ac.jp/˜ komori/gakkai04-09/