fetburner.core

コアダンプ

CoqによるZ定理（及び，β簡約の合流性）の証明

Coq

PPL 2019のポスター発表でZ定理[Dehornoy+08]なるものを知ったので，Coqで定式化してみる． それだけでは面白くないので，これを用いて\beta簡約の合流性も証明する．

Z定理[Dehornoy+08]とは？

抽象書き換え系(A,\rightarrow)は，以下のようなZ性を満たすf:A\rightarrow Aが存在すれば満たせば合流するといった定理．

f:id:fetburner:20190518171323p:plain

例えば\beta簡約の合流性を示す際はcomplete development（見えているredexを全て簡約するもの）のZ性を証明するだけでよくて， 良く知られている証明のように並列簡約を用いなくても良いのがうれしいらしい．

Z定理[Dehornoy+08]の証明

合流性と準合流性は等価なので，Z性を満たすfが存在すれば(A,\rightarrow)が準合流性を満たすことを証明すればよい．

a\twoheadrightarrow bならばf(a)\twoheadrightarrow f(b)だけステップ数に関する帰納法で示してしまえば， あとはM_1\rightarrow NとM_{n-1}\rightarrow M_nにZ性を適用するだけで下図のように準合流性を証明できる．

f:id:fetburner:20190518180359p:plain

Coqでの証明も難しくなくて，合流性の定義とか色々抜きにすればたったこれだけ．

Theorem Z map :
  (forall x y, R x y -> clos_refl_trans _ R y (map x)) ->
  (forall x y, R x y -> clos_refl_trans _ R (map x) (map y)) ->
  confluent.
Proof.
  move => Zproperty1 Zproperty2.
  have monotonicity : forall x y,
    clos_refl_trans _ R x y ->
    clos_refl_trans _ R (map x) (map y).
  { induction 1; eauto. }
  apply: semi_confluent_impl_confluent => ? ? ? ? /clos_rt_rtn1_iff Hrt.
  inversion Hrt; subst; eauto.
  move: (H0) => /clos_rt_rtn1_iff /monotonicity ?.
  eauto 6.
Qed.

\beta簡約の合流性の証明

Z定理だけ証明しても嬉しさが分かってこないので，complete development M*がZ性を満たすことから\beta簡約の合流性を証明する．

M*のZ性は以下2つの補題を証明すれば文脈についての帰納法で証明できる．

  • M\twoheadrightarrow M*
  • {(M*)[ x \mapsto N* ] \twoheadrightarrow (M[ x \mapsto N ])* }

これらの補題はMの構造に関する帰納法で示せる．

ところが，complete developmentは以下のようにキモい場合分けをする再帰関数として定義される．

Fixpoint development t :=
  match t with
  | Var x => Var x
  | Abs t => Abs (development t)
  | App (Abs t11) t2 => (development t11).[development t2/]
  | App t1 t2 => App (development t1) (development t2)
  end.

このためCoqで補題を証明しようと思うと，簡約して欲しくないgallina termが簡約されてしまい，自動証明が重くなることも多々あった．

SSReflect 1.6とAutosubstをインストールしたCoq 8.5.3で動作するソースコード一式を Z theorem · GitHub にアップロードしたので，その重さを体感して欲しい．

あとがき

Z定理を用いれば並列簡約なしで\beta簡約の合流性を証明できると言っても， complete developmentはCoqで扱うとウザい類の関数なので，こいつとの触れ合いが増えるのは勘弁して欲しかった．

なにはともあれ，合流性の証明を考える時の手札が増えたので，PPL 2019に参加したのも無意味ではなかった．