型健全性が保証する性質を余帰納的に書いてみた

型健全性というと type preservation と progress が成り立ってればよいというのがよくある話ですが，それでなぜ健全といえるのかというところをわざわざ形式的に書いてみた話です。といっても，わかりやすい説明をしようという気はあまりなくて，知ってる人には余帰納的定義の事例として少しおもしろいかなと思っただけですが。

とりあえず項と簡約関係と値については，中身はどうでもいいので与えられていると仮定しましょう。型付け可能性についても適当に定義されていることにします。

Parameter Terms : Set.
Parameter reduce : Terms -> Terms -> Prop.
Parameter is_value : Terms -> Prop.
Parameter typable : Terms -> Prop.

さらに progress と preservation が成り立つと仮定しましょう。

Axiom progress :
  forall t, typable t ->
    is_value t \/ exists t', reduce t t'.

Axiom preservation :
  forall t t', typable t -> reduce t t' -> typable t'.

このときに，型付け可能な項はよい性質をもつとされるわけで，具体的にどういう性質なんですかというと，よく「値じゃない状態で計算が止まらない」と表現したりします。それを形式的に書くなら以下のように余帰納的に定義することになるでしょう。

CoInductive safe : Terms -> Prop :=
| v_safe : forall t, is_value t -> safe t
| r_safe : forall t t', reduce t t' -> safe t' -> safe t.

progress と preservation があれば safe であるということを証明してみましょう。

Theorem type_soundness :
  forall t, typable t -> safe t.
  cofix.
  intros t H.
  destruct (progress _ H) as [? | [t' ?]].
  apply v_safe; assumption.
  apply r_safe with t'.
  assumption.
  apply type_soundness.
  apply preservation with t; assumption.
Qed.

できました。

だから何，というと，何なんでしょう。元々はもうちょっと別のことを考えていたんですが。