正規形を持つ項は最左最外簡約によってもその正規形に簡約されるのは有名な話. これはかなり嬉しくて,最左最外簡約は値呼びとは何だったのかと言わんばかりの優秀な評価戦略と言えるでしょう.
しかし,この性質は有名な割に定理証明支援系を使った証明を見ない気がします. みんな格好良い型の付いた言語に夢中なんでしょうか?ひとつCoqで証明してみましょう.
最左最外簡約の正規化定理の証明と言えば標準化定理 (任意の簡約列は左から右へ順になるような簡約列に並び変えられるやつ) から導かれるのですが, 黄色い厚い本に書いてある標準化定理の証明はdevelopmentを使っていてCoqで書くにはダルい!
なので今回は適当にネットサーフィンしてたら見付けた鹿島先生のA Proof of the Standardization Theorem in λ-Calculusという論文(?)を参考に証明します. この論文の手法の巧みなところは名前呼びの簡約も織り交ぜて,標準簡約列を簡潔に帰納的定義している所です. そのため定理証明支援系との相性が良く,Coqでも比較的簡単に証明できます.
とりあえず最左最外簡約leftmost
や名前呼びの簡約cbn
なんかの定義やら瑣末な性質の証明やらは面倒なのでここでは割愛.
Self-containedな証明はGithubにあるのでそちらを参照して下さい.
項の定義も勿論割愛.見れば分かると思いますがtvar x
が,tapp t1 t2
が,tabs t
がのつもりです.
束縛はAutosubstを使ってde Bruijn indexで表現してます.
まず標準簡約列st
を定義.論文中での
に相当するものです.
名前呼び簡約の反射推移閉包になっている部分は厳密には という二項関係として帰納的に定義されていますが,等価なので流用します.
Inductive st : relation term := | st_var t x : clos_refl_trans _ cbn t (tvar x) -> st t (tvar x) | st_app t t1 t2 t1' t2' : clos_refl_trans _ cbn t (tapp t1 t2) -> st t1 t1' -> st t2 t2' -> st t (tapp t1' t2') | st_abs t t1 t1' : clos_refl_trans _ cbn t (tabs t1) -> st t1 t1' -> st t (tabs t1').
そしてLemma 3.4とLemma 3.5に相当する瑣末な補題を適当に片付けましょう. Autosubstが並列代入ベースなのでLemma 3.4(5)も並列代入版です.
Lemma st_refl t : st t t. Proof. induction t; eauto. Qed. Lemma st_abs_inv t1 t' : st (tabs t1) t' -> exists t1', t' = tabs t1'. Proof. inversion 1; subst; eauto. - apply cbn_abs_multi_inv in H0. congruence. - apply cbn_abs_multi_inv in H0. congruence. Qed. Lemma cbn_multi_st_comp t1 t2 t3 : clos_refl_trans _ cbn t1 t2 -> st t2 t3 -> st t1 t3. Proof. inversion 2; eauto. Qed. Lemma st_rename t t' : st t t' -> forall r, st (rename r t) (rename r t'). Proof. induction 1; intros ?; simpl. - eapply cbn_multi_st_comp. + apply cbn_multi_rename. eassumption. + apply st_refl. - econstructor; eauto. apply (cbn_multi_rename _ _ _ H). - econstructor; eauto. apply (cbn_multi_rename _ _ _ H). Qed. Lemma st_subst t1 t1' : st t1 t1' -> forall s s', (forall x, st (s x) (s' x)) -> st (t1.[s]) (t1'.[s']). Proof. induction 1; simpl; intros ? ? Hsub. - eapply cbn_multi_st_comp. + apply cbn_multi_subst. eassumption. + apply Hsub. - econstructor; eauto. apply (cbn_multi_subst _ _ _ H). - econstructor. + eapply (cbn_multi_subst _ _ _ H). + apply IHst. intros [| ?]; simpl. * apply st_refl. * apply st_rename. eauto. Qed. Lemma st_red_comp t2 t3 : red t2 t3 -> forall t1, st t1 t2 -> st t1 t3. Proof. induction 1; intros ? Hst; inversion Hst; subst; eauto. - inversion H3; subst. eapply cbn_multi_st_comp. eapply rt_trans. + eassumption. + eapply rt_trans. * apply cbn_app_multi. eassumption. * apply rt_step. eauto. + apply st_subst. * eauto. * intros [| ?]; [ apply H4 | apply st_refl ]. Qed. Hint Resolve st_red_comp.
黄色い厚い本では何とも手強そうだった標準化定理ですが,今回の定義ではそれに相当する定理を何とも簡単に証明できます.
Lemma beta_multi_st t t' : clos_refl_trans _ red t t' -> st t t'. Proof. intros H. apply clos_rt_rtn1 in H. induction H; eauto. - apply st_refl. Qed.
そして,標準化定理を用いれば最左最外簡約の正規化定理を証明できます. 最左最外簡約の定義が複雑なのでちょっと証明も長くなりますが…
Theorem leftmost_theorem t t' : in_normal_form _ red t' -> clos_refl_trans _ red t t' -> clos_refl_trans _ leftmost t t'. Proof. unfold in_normal_form. unfold not. intros ? Hred. apply beta_multi_st in Hred. induction Hred; eauto 7. eapply rt_trans. - apply cbn_multi_leftmost_multi. eauto. - destruct (neutral_dec t1') as [[]|]; subst. + edestruct H; eauto. + destruct (neutral_dec t1) as [[]|]; subst; eauto. * destruct (st_abs_inv _ _ Hred1) as []; subst. edestruct H; eauto. * { apply rt_trans with (y := tapp t1' t2). - apply leftmost_appl_multi; eauto. - apply leftmost_appr_multi; unfold in_normal_form; unfold not; eauto. } Qed.
論文では正規化定理によく似た性質として,正規系を持つλ項は無限個の最左最外簡約を含む簡約列を持たないことも証明されています. 今回はそれを証明して終わりにします.
Lemma red_multi_leftmost_swap t1 t2 t3 : clos_refl_trans _ red t1 t2 -> leftmost t2 t3 -> exists t2', leftmost t1 t2' /\ clos_refl_trans _ red t2' t3. Proof. intros Hrt Hleftmost. apply beta_multi_st in Hrt. generalize dependent t1. induction Hleftmost; inversion 1; subst. - inversion H3; subst. destruct (strip_lemma _ _ _ _ H1) as [|[? []]]; subst; eauto 7. destruct (strip_lemma _ _ _ _ H0) as [|[? []]]; subst; eexists; split; eauto. apply red_subst_multi; eauto. intros [| ?]; simpl; eauto. - destruct (strip_lemma _ _ _ _ H2) as [|[? []]]; subst. + edestruct IHHleftmost as [? []]; eauto. eapply neutral_red_multi in H; eauto 8. + destruct (neutral_dec t0) as [[]|]; subst; eauto 8. - destruct (strip_lemma _ _ _ _ H3) as [|[? []]]; subst; eauto 8. edestruct IHHleftmost as [? []]; eauto. destruct (strip_lemma _ _ _ _ (leftmost_theorem _ _ H0 (st_beta_multi _ _ H5))) as [|[? []]]; subst; eauto. apply neutral_red_multi with (t := t3) in H; eauto. eexists. split; eauto. apply rt_trans with (y := tapp t1 t4); eauto 6. - destruct (strip_lemma _ _ _ _ H0) as [|[? []]]; subst; eauto 8. edestruct IHHleftmost as [? []]; eauto. Qed. Theorem quasi_leftmost_theorem t : Acc (fun t2 t1 => leftmost t1 t2) t -> Acc (fun t3 t1 => exists t2, clos_refl_trans _ red t1 t2 /\ leftmost t2 t3) t. Proof. induction 1 as [t ? IH]. constructor. intros ? [? [Hred Hleftmost]]. destruct (red_multi_leftmost_swap _ _ _ Hred Hleftmost) as [? [Hleftmost']]. destruct (IH _ Hleftmost') as [IH']. constructor. intros ? [? [? ?]]. eauto. Qed.