第15章：保存・進行・型安全性#

型の付いた閉項が実行中に行き詰まらないことを、型検査器が受理したという事実だけから結論してよいでしょうか。必要なのは、各一段が型を保つことと、型の付いた閉項が値でなければ次の一段を持つことです。この二つは別の帰納法で証明され、どちらか一方だけでは型安全性になりません。

本章では内在的に型付けされた構文に値呼びの意味論を与え、保存を一段関係の型に組み込みます。その上で関数型の値の形を分類し、進行定理を完全に証明します。最後に「行き詰まらない」という系を導き、停止や意図した仕様の充足までは保証しないことを反例の形から確認します。

一段簡約の両端へ同じ型を要求する#

型 A の項から型 A の項への関係として一段簡約を定義します。β規則の右辺は前章の型保存代入 substituteTop で作られるため、異なる型の項へ簡約する規則は構成できません。

外在的な通常の定式化では、保存と進行は

\frac{\Gamma\vdash t:A\qquad t\longrightarrow t'} {\Gamma\vdash t':A} \qquad\text{および}\qquad \varnothing\vdash t:A\Longrightarrow (\mathsf{Value}(t)\lor\exists t'.\,t\longrightarrow t')

です。本章の内在的構文では前者を一段関係の添字へ移し、後者を帰納法で証明します。

Leankernel-checked counterpartL32–49

namespace FormalLab.TypeTheory.TypeSafety

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

inductive Value : Tm Γ A → Prop where
  | lam : Value (Tm.lam body)

inductive Step : Tm Γ A → Tm Γ A → Prop where
  | beta : Value argument →
      Step (Tm.app (Tm.lam body) argument) (substituteTop argument body)
  | appLeft : Step function function' →
      Step (Tm.app function argument) (Tm.app function' argument)
  | appRight : Value function → Step argument argument' →
      Step (Tm.app function argument) (Tm.app function argument')

def typedIdentity (A : SimpleType) : Tm [] (A ⇒ A) :=
  .lam (.var .zero)

閉じた argument : Tm [] A が必ず値であるとは限りません。適用形の閉項も構成できるためです。したがって恒等関数への任意の引数適用が直ちにβ簡約する、という一般化はできません。β規則へ渡せるのは Value argument の証明がある場合だけです。以下では具体的なラムダ値に限定します。

Leankernel-checked counterpartL57–61

def atomIdentity : Tm [] (.atom ⇒ .atom) :=
  typedIdentity .atom

example : Step (.app (typedIdentity (.atom ⇒ .atom)) atomIdentity) atomIdentity :=
  .beta .lam

関数型の値はラムダ抽象である#

進行証明の適用の場合、関数位置が値ならβ規則へ進むため、その値がラムダ抽象であることを知る必要があります。これは値の構成子を場合分けする標準形補題です。

Leankernel-checked counterpartL69–73

theorem functionValueIsLambda {Γ : Context} {A B : SimpleType}
    {term : Tm Γ (A ⇒ B)} (value : Value term) :
    ∃ body : Tm (A :: Γ) B, term = .lam body := by
  cases value with
  | lam => exact ⟨_, rfl⟩

型だけから項の構文を分類したのではありません。「関数型を持ち、かつ値である」という二条件からラムダ形を得ています。値の定義へ定数や組を加える言語では、型ごとに標準形補題を増やします。

閉じた型付き項は値であるか一段進む#

進行定理は空文脈を仮定します。自由変数 .var は空文脈に所属できないため、その場合は Var [] A の不可能性から閉じます。ラムダは値です。適用では関数側の帰納仮定を先に使い、関数が値なら引数側へ進みます。

Leankernel-checked counterpartL85–97

theorem progress {A : SimpleType} (term : Tm [] A) :
    Value term ∨ ∃ next, Step term next := by
  cases term with
  | var v => cases v
  | lam body => exact Or.inl .lam
  | app function argument =>
      rcases progress function with functionValue | ⟨function', functionStep⟩
      · rcases progress argument with argumentValue | ⟨argument', argumentStep⟩
        · obtain ⟨body, rfl⟩ := functionValueIsLambda functionValue
          exact Or.inr ⟨_, .beta argumentValue⟩
        · exact Or.inr ⟨_, .appRight functionValue argumentStep⟩
      · exact Or.inr ⟨_, .appLeft functionStep⟩
termination_by sizeOf term

証明の分岐は評価戦略そのものです。関数が進めるなら appLeft、関数が値で引数が進めるなら appRight、両方が値なら標準形補題で関数をラムダへ戻して beta を使います。可能性を網羅することが進行の帰納であり、実行例をいくつ試しても代わりにはなりません。

保存は関係の型に現れ、行き詰まりの不在は系になる#

外在的構文では保存定理を

\frac{\Gamma\vdash t:A\qquad t\longrightarrow t'} {\Gamma\vdash t':A}

と述べ、βの場合に代入補題を使います。本章の Step : Tm Γ A → Tm Γ A → Prop は両端の添字を共有するため、保存される文脈と型を関係の宣言へ組み込みました。次の関数は一段の証拠から右端の型付き項を取り出し、保存の情報が失われていないことを型で検査します。

Leankernel-checked counterpartL118–130

def preservation {Γ : Context} {A : SimpleType} {term next : Tm Γ A}
    (_step : Step term next) : Tm Γ A :=
  next

def Stuck {A : SimpleType} (term : Tm [] A) : Prop :=
  ¬Value term ∧ ¬∃ next, Step term next

theorem wellTypedClosedTermIsNotStuck {A : SimpleType} (term : Tm [] A) :
    ¬Stuck term := by
  intro stuck
  rcases progress term with value | step
  · exact stuck.1 value
  · exact stuck.2 step

wellTypedClosedTermIsNotStuck が本章の型安全性の直接の帰結です。型の付いた閉項は値か一段可能なので、値でなく次状態もない項にはなりません。開項には自由変数が残り得るため、空文脈の仮定を落とせません。

型安全性は停止を述べません。再帰や一般不動点を加えた型付き言語では、型を保ったまま無限に進めます。また論理的な仕様の正しさも自動ではありません。Nat → Nat 型の関数が利用者の望む税計算をするかは、単なる型安全性より強い仕様と証明を必要とします。

要点#

保存は一段簡約の前後で文脈と型が同じであることを述べ、代入補題に依存する。
進行は閉じた型付き項が値か一段可能であることを述べ、標準形補題に依存する。
内在的構文では保存を関係の型へ組み込めるが、進行の網羅的な帰納は依然として必要である。
保存と進行から行き詰まりの不在が従うが、停止や外部仕様の充足は従わない。
言語へ新しい型と値を加えるたび、対応する標準形と進行の分岐を監査する必要がある。

研究史と文献案内#

subject reductionはラムダ計算・組合せ論の系譜で研究されてきました。WrightとFelleisenの1994年論文 [WF94] は、操作的意味論に対する構文的な型健全性証明をプログラミング言語へ体系的に適用した基準文献です。本章の純粋STLCと内在的構文は同論文が扱うStandard ML核の再現ではありません。保存・進行・標準形・代入補題の教科書的な完全証明は [TAPL02]、判断の構造を含む展開は [PFPL16] を参照してください。

問題#

進行証明の全分岐を導出木へ戻す#

progress の適用の場合を、関数側と引数側の二つの選言から四つの組合せとして列挙してください。実際に残る三分岐へ appLeft、appRight、beta を割り当て、関数値の標準形補題を使う位置を示します。各分岐の次項を明記し、評価戦略が変わればどの分岐順が変わるか説明すれば完了です。

外在的な保存定理を復元する#

第11章の HasType と第13章の無型 Step を使い、保存定理の正確な型を書いてください。βの場合に必要な代入補題、適用の二場合に必要な帰納仮定を特定します。本章の preservation が短い理由を内在的添字から説明し、短い証明と弱い主張を混同していないことを両定式化の対応表で示してください。

言語拡張が壊す箇所を診断する#

真偽値型、真偽値二値、条件分岐を Tm と Step に加える設計を書いてください。真偽値型の標準形補題と進行証明の新しい場合を列挙し、条件分岐の一規則を意図的に欠かしたときに生じる型付き行き詰まりを構成します。保存と進行のどちらが失敗したかを判定し、欠けた規則を戻した後に標準形、進行、非行き詰まりの系を同じ順で再証明できれば完了です。