import FormalLab.TypeTheory.TypeSafety

/-!
# 第16章：正規形・弱正規化・強正規化

ある評価戦略が値へ到達すること、どこかの簡約列が正規形へ到達すること、どの簡約列を選んでも有限で
終わることは、三つの異なる主張です。さらに正規形の存在を証明することと、正規形を計算する具体的な
アルゴリズムを与えることも同じではありません。

本章では一段簡約から弱正規化と強正規化を定義し、自己ループする項が強正規化しないことをLeanで
証明します。型付き項については、値が強正規化する最初の基底場合を検査し、STLC全体の強正規化定理を
正確な命題として固定します。一般証明に必要な論理関係は後の章で構成するため、ここで定理名だけを
証明済みとして扱いません。

## 正規形は一段先を持たない

簡約関係 `Step` に対し、`t` が正規形であるとは `t → u` となる `u` が存在しないことです。
この定義は値構文を参照しません。どの位置のredexを一段関係が許すかによって、同じ項でも正規形か
どうかは変わります。

$$
\mathsf{NF}(t)\;:\!\Longleftrightarrow\;\neg\exists u.\;t\longrightarrow u.
$$
-/

namespace FormalLab.TypeTheory.Normalization

open FormalLab.Foundation.UntypedLambdaCalculus
open FormalLab.TypeTheory.OperationalSemantics

def NormalForm (term : Term) : Prop :=
  ¬∃ next, FormalLab.TypeTheory.OperationalSemantics.Step term next

theorem valueIsNormalForm {term : Term} (value : Value term) : NormalForm term := by
  rintro ⟨next, step⟩
  exact valueCannotStep value step

theorem identityIsNormalForm : NormalForm identity :=
  valueIsNormalForm .lam

/-!
本章の `Step` はラムダ本体の内側へ進まない弱い値呼び関係なので、全てのラムダ抽象が正規形です。
完全β簡約なら本体中のredexも対象になり、この定理はそのままでは成立しません。正規形という語だけで
簡約関係を省略せず、弱頭正規形、値、β正規形のどれを指すかを確定します。

## 弱正規化は一つの有限経路を要求する

弱正規化は、ある正規形へ有限回で到達する簡約列の存在です。反射推移閉包に零回を含めるため、すでに
正規形である項は直ちに弱正規化します。

$$
\mathsf{WN}(t)\;:\!\Longleftrightarrow\;
\exists n.\;t\longrightarrow^{*}n\land\mathsf{NF}(n).
$$
-/

def WeaklyNormalizing (term : Term) : Prop :=
  ∃ normal, Steps term normal ∧ NormalForm normal

theorem normalFormIsWeaklyNormalizing {term : Term} (normal : NormalForm term) :
    WeaklyNormalizing term :=
  ⟨term, .refl, normal⟩

theorem valueIsWeaklyNormalizing {term : Term} (value : Value term) :
    WeaklyNormalizing term :=
  normalFormIsWeaklyNormalizing (valueIsNormalForm value)

/-!
弱正規化では「よい経路が一つある」だけです。別のredex選択が無限列を作る可能性を排除しません。
一段関係が決定的なら経路は高々一つなので差は縮まりますが、完全β簡約のような非決定的関係では
量化の違いが本質的です。

## 強正規化は全ての一段列の整礎性である

`Acc r t` は、`t` から関係 `r` を逆向きにたどる全ての枝が整礎であることを表します。一段簡約の
後続項 `u` を `r u t :⇔ Step t u` と置けば、`Acc r t` は `t` から無限簡約列を始められないという
強正規化の帰納原理になります。

$$
\mathsf{SN}(t)\;:\!\Longleftrightarrow\;
\mathsf{Acc}(\lambda u\,t.\;t\longrightarrow u,\,t).
$$
-/

def StronglyNormalizing (term : Term) : Prop :=
  Acc (fun next current => FormalLab.TypeTheory.OperationalSemantics.Step current next) term

theorem selfLoopIsNotStronglyNormalizing {term : Term}
    (loop : FormalLab.TypeTheory.OperationalSemantics.Step term term) :
    ¬StronglyNormalizing term := by
  intro accessible
  induction accessible with
  | intro current _smaller inductionHypothesis =>
      exact inductionHypothesis current loop loop

theorem omegaIsNotStronglyNormalizing : ¬StronglyNormalizing omega :=
  selfLoopIsNotStronglyNormalizing omegaOneStep

/-!
証明は項の大きさを測っていません。自己ループを一度たどると同じ項へ戻ります。そのため `Acc` が要求する
「全ての後続項は再びaccessibleである」という証拠が、自分自身へ無限に降下して矛盾します。
β簡約では代入により項の大きさが増えることがあるので、構文サイズだけを一般の減少測度にはできません。

## 型付き値は強正規化する

型安全性章の一段関係について同じ定義を置きます。値は一段先を持たないため、後続項が全て強正規化する
という `Acc` の条件を空虚に満たします。これはSTLC強正規化証明の基底場合ですが、適用と代入を含む
一般の場合ではありません。
-/

namespace Typed

open FormalLab.TypeTheory.SimplyTypedLambdaCalculus
open FormalLab.TypeTheory.StructuralRules

def StronglyNormalizing {Γ : Context} {A : SimpleType} (term : Tm Γ A) : Prop :=
  Acc (fun next current => FormalLab.TypeTheory.TypeSafety.Step current next) term

theorem valueCannotStep {Γ : Context} {A : SimpleType} {term : Tm Γ A}
    (value : FormalLab.TypeTheory.TypeSafety.Value term) :
    ¬∃ next, FormalLab.TypeTheory.TypeSafety.Step term next := by
  rintro ⟨next, step⟩
  cases value
  cases step

theorem valueIsStronglyNormalizing {Γ : Context} {A : SimpleType} {term : Tm Γ A}
    (value : FormalLab.TypeTheory.TypeSafety.Value term) : StronglyNormalizing term := by
  constructor
  intro next step
  exact False.elim (valueCannotStep value ⟨next, step⟩)

def STLCStrongNormalization : Prop :=
  ∀ (Γ : Context) (A : SimpleType) (term : Tm Γ A), StronglyNormalizing term

example : StronglyNormalizing (FormalLab.TypeTheory.TypeSafety.typedIdentity .atom) :=
  valueIsStronglyNormalizing .lam

end Typed

/-!
`STLCStrongNormalization` は完全な定理の型を記録した命題であり、この章にその証明はありません。
値の場合だけを証明して全ての型付き項へ一般化すると、適用項の後続とβ代入を扱う根拠が欠けます。

標準的な証明では、原子型では強正規化、関数型 `A ⇒ B` では「任意の計算可能な `A` 型引数へ適用すると
計算可能な `B` 型項になる」という型ごとの述語を定義します。次に変数を計算可能項へ送る代入が型付き項を
計算可能項へ送る**基本補題**を、型導出について帰納的に証明します。恒等代入を選べば全ての型付き項が
計算可能であり、そこから強正規化が従います。

$$
\text{型ごとの計算可能性}
\Longrightarrow\text{名前変更・代入に対する閉性}
\Longrightarrow\text{基本補題}
\Longrightarrow\text{全型付き項の計算可能性}
\Longrightarrow\text{強正規化}.
$$

この論証では型の構造に関する帰納と型導出に関する帰納が異なる役割を持ちます。後の論理関係章では
この依存を展開し、System Fで量化型が加わると関係の解釈がどう変わるかを比較します。

## 正規化と等式の可決定性

二項を正規化して構文的に比較する方法は、変換可能性の決定手続きになり得ます。ただし必要なのは
正規化器の停止だけではありません。簡約が元の等式理論に対して健全で、同値な項が比較可能な標準形へ
至り、標準形が適切な意味で一意であることも必要です。強正規化だけから合流性は従いません。

Leanのkernelが定義的等しさを検査できることを、任意の対象言語の正規化定理として利用してはいけません。
本章の `Term`、`Tm`、`Step` はLean内に定義した対象であり、Lean自身のreducerとは別です。

## 要点

* 正規形は採用した一段関係の後続を持たない項であり、値と常に同じではない。
* 弱正規化は正規形へ至る経路の存在、強正規化は全ての簡約列の有限性を要求する。
* 自己ループは `Acc` の整礎性と両立せず、強正規化しない。
* STLCの強正規化には型ごとの計算可能性と代入に関する基本補題が必要である。
* 正規化から等式決定へ進むには、健全性、完全性、標準形の一意性も検査する。

## 研究史と文献案内

Taitの1967年論文 [TAI67] は有限型の汎関数に対する解釈を展開します。後のreducibilityと
logical relationsによる正規化証明を読む重要な基準点です。本章の `Acc` 定義を同論文の記法へ
遡及させません。型付きラムダ計算の正規化と証明論の関係は [GLT89] を参照してください。
構文から型安全性までの教科書的経路は [TAPL02]、言語のメタ理論としての構成は [PFPL16] が扱います。

## 問題

### 三種類の停止主張を反例で分ける

値呼びの値、弱正規化、強正規化を量化子まで展開し、各含意の向きを調べてください。自己ループ
`omega` が失敗させる条件を `Acc` の一段展開から説明します。非決定的な簡約関係を小さく定義し、
正規形へ至る枝と自己ループする枝を同時に持つ項を作って、弱正規化だが強正規化でないことを証明します。

### 計算可能性述語の関数型場合を読む

原子型を強正規化で解釈し、`A ⇒ B` の計算可能性を全称量化で書いてください。恒等関数と定数関数が
関数型の条件を満たすために必要な仮定を導出し、任意の引数という量化を有限個のテストで置き換えられない
理由を示します。さらに計算可能性から強正規化を得る補題の向きを型ごとに書きます。型帰納と項帰納の
どちらを各段階で使い、代入補題がどこで二つを接続するかを表にすれば完了です。

### 正規化器から等式判定器までの欠落を埋める

二項を正規化して比較する擬似コードを書いてください。停止性、簡約の健全性、標準形の存在、合流性、
構文比較の決定可能性をどこで使うか注記します。強正規化だけを残して合流性を外した抽象的な
簡約系を作り、同じ項が異なる正規形へ至る反例から、判定器の完全性が壊れることを説明してください。
-/

end FormalLab.TypeTheory.Normalization