Nominal Isabelleとラムダ計算 その3

これは一人Computer Scienceアドベントカレンダー 12日目の記事です。

前回はCRの証明の途中までやったので続きです。 内容多めですが今回で頑張って終わらせます。

confluenceへ (cont.)

coherent lemmas

parallel betaのcoherent lemmaを示す。 証明は基本的に場合分けやるだけなので省略するとして、まぁ常識的なことが成り立つよねという補題である。(説明の放棄)

  lemma elim_pb_var: "Var x ⇒β N ⟹ N = Var x"

  lemma elim_pb_abs:
    assumes "lam [x]. M ⇒β N'" "x ♯ N'"
    obtains N where "M ⇒β N" "N' = lam [x]. N"

  lemma elim_pb_app:
    assumes "M1 $ M2 ⇒β N"
    obtains N1 N2 where "N = N1 $ N2" "M1 ⇒β N1" "M2 ⇒β N2"
       | x P P' L where "M1 = lam[x]. P" "P ⇒β P'" "N = P'[x ::= L]" "M2 ⇒β L" "x ♯ (M2,L)"

  lemma elim_pb_app_nonabs:
    assumes "M1 $ M2 ⇒β N" "nonabs M1"
    obtains N1 N2 where "N = N1 $ N2" "M1 ⇒β N1" "M2 ⇒β N2"

  lemma elim_pb_app_beta:
    assumes "(lam [x]. M1) $ M2 ⇒β N" "x ♯ (M2,N)"
    obtains N1 N2 where "N = (lam [x]. N1) $ N2" "M1 ⇒β N1" "M2 ⇒β N2"
    | N1 N2 where "N = N1[x ::= N2]" "M1 ⇒β N1" "M2 ⇒β N2"

par_to_star 

  lemma pb_subst: "⟦ t1 ⇒β s1; t2 ⇒β s2 ⟧ ⟹ t1 [x ::= t2] ⇒β s1 [x ::= s2]"
  apply (nominal_induct avoiding: x t2 s2 rule: par_beta.strong_induct, auto)
    apply (rule, rule, simp, simp)
    apply (rule, simp)
    apply (simp add: fresh_atm pb_beta subst_gfresh' substitution)
  done
    
  lemma par_to_star: "⟦ t ⟶* t1; t ⇒β t2 ⟧ ⟹ t2 ⇒β t1"
  apply (nominal_induct avoiding: t2 rule: bstar.strong_induct)
    using elim_pb_var apply blast
    apply (erule elim_pb_abs, simp, simp, rule, simp)
    apply (erule elim_pb_app, simp, rule, simp, simp, simp)
    apply (erule elim_pb_app_beta, simp, simp, rule, simp, simp, simp)
    apply (simp, rule pb_subst, simp, simp)
  done

pb_substは、parallel betaがsubstitutionに対しても成り立つよね、という補題である。

そしてpar_to_starは示したかった性質その3にあたるものである。これはstar変換についての帰納法であるが、帰納法を行うと t ⇒β t2 ⟹ t2 ⇒β t1 のtとt1に具体的な項が入ったものを含むsubgoalが一杯出現する。 このときに示しておいたcoherent lemmaを使う。 (IMPの時にも述べた気がするが、このようなcoherent lemmaをその場で示すのはgoalが不必要な具体化と複雑化している関係で困難なので補題を置いたほうがはるかに簡単だと思う)

star_existence

次に、bstarが常に存在する(どんなラムダ項に対してもbstarの行き先が存在する)ことを言う。

  lemma bstar_fresh:
    fixes x :: var
    assumes "M ⟶* N"
    shows "x ♯ M ⟹ x ♯ N"

  lemma elim_bs_abs:
    assumes "lam [x]. t ⟶* s"
    obtains t' where "t ⟶* t'" "s = lam [x]. t'"

  lemma lambda_nonabs_case:
    fixes M :: lambda
    shows "(nonabs M ⟹ thesis) ⟹ (⋀x M'. M = lam [x]. M' ⟹ thesis) ⟹ thesis"
  by (nominal_induct M rule: lambda.strong_induct, auto)

bstar_freshはbstarがfreshnessを保つことを言う。これは簡約によって新たに変数が出現することはないということから分かる。 elim_bs_absはcoherenceのbstar_abs版。 lambda_non_abs_caseは、要はラムダ項Mに対して、 nonabs M であるか、x M'が存在して M = lam [x]. M' となるのいずれかが成り立つという補題である。

補足しておくと、lemmaの宣言で obtains t where P(t) と書いたらこれは(HOLではなくIsabelle組み込みの方のPure logicの意味で)同値な変形によって (⋀t. P(t) ==> thesis) ==> thesis と変形される。 これと同じようにして上のlambda_non_abs_caseを言いたかったが、nonabsのケースはobtainsに来るべきものがない(存在量化の形ではない)ので、このように最初から変形した形でステートメントを与えている。

  lemma star_exist:
    obtains t' where "t ⟶* t'"
  proof-
    have "∃t'. t ⟶* t'"
      apply (nominal_induct t rule: lambda.strong_induct, auto)
      apply (rule, rule)
      defer
      apply (rule, rule, simp)
      proof-
        fix M1 M2 N N'
        assume hyp: "M1 ⟶* N" "M2 ⟶* N'"
        show "∃t'. M1 $ M2 ⟶* t'"
          apply (rule_tac lambda_nonabs_case [of M1])
          apply (rule, rule, simp, rule hyp, rule hyp)
          proof-
            fix x M'
            assume M1: "M1 = lam [x].M'"
            then obtain N1 where N1: "N = lam [x].N1" "M' ⟶* N1"
              using elim_bs_abs hyp(1) by blast
            have "M1 $ M2 ⟶* N1 [x ::= N']"
              by (simp add: M1, rule bs_beta, simp add: N1, simp add: hyp)
            thus ?thesis by blast
          qed
      qed
    thus "(⋀t'. t ⟶* t' ⟹ thesis) ⟹ thesis" by blast
  qed

さて目的のstar_existである。 証明は帰納法による。applicationの場合に、上で示したlambda_nonabs_caseという場合分けを行う必要があるのでそれを使う。

場合分けだけなので簡単だけど結構準備が大変。

confluence

par_confluent

欲しい性質は全て言えたので、ようやくconfluenceの証明に移る。

  lemma par_confluent:
    assumes "t ⇒β t1" "t ⇒β t2"
    obtains s where "t1 ⇒β s" "t2 ⇒β s"
  proof-
    obtain t' where t': "t ⟶* t'"
      using star_exist by auto 
    have "t1 ⇒β t'" "t2 ⇒β t'"
      using par_to_star [OF t'] assms by auto
    thus "(⋀s. t1 ⇒β s ⟹ t2 ⇒β s ⟹ thesis) ⟹ thesis" by blast
  qed

まずparallel betaの1stepがconfluentなこと。 これは示したpar_to_starとstar_existにより分かる。

long_parallel_beta

次にlong_parallel_betaというのを定める。 まぁpar_betaのrefl-trans closure取るだけなので。

そして、par_to_longbetaとone_to_parによりこれがlong_betaと同値なこともわかる。

  abbreviation long_par_beta (infixl "⟹β" 50) where
    "long_par_beta == par_beta⇧*⇧*"

  lemma long_pb_iff_long_b: "t ⟹β s ⟷ t ⟶β s"
  apply rule
  apply (induct rule: rtranclp_induct)
    apply simp
    apply (rule rtranclp_trans, simp, simp add: par_to_longbeta)
  apply (induct rule: rtranclp_induct)
    apply simp
    apply (rule rtranclp_trans, simp, rule r_into_rtranclp, simp add: one_to_par)
  done

Church-Rosser 

  lemma CR:
    assumes "t ⟶β t1" "t ⟶β t2"
    obtains s where "t1 ⟶β s" "t2 ⟶β s"
  proof-
    have CR_one_long: "⋀t t1 t2. ⟦ t ⟹β t2; t ⇒β t1 ⟧ ⟹ ∃s. t1 ⟹β s ∧ t2 ⇒β s"
      proof-
        fix t t1 t2
        show "⟦ t ⟹β t2; t ⇒β t1 ⟧ ⟹ ∃s. t1 ⟹β s ∧ t2 ⇒β s"
          proof (induct arbitrary: t1 rule: rtranclp_induct)
            fix t1 show "t ⇒β t1 ⟹ ∃s. t1 ⟹β s ∧ t ⇒β s"
              by (rule par_confluent, rule pb_refl, simp, blast)
          next
            fix y z t1
            assume t: "t ⟹β y" "y ⇒β z" and hyp: "⋀t1. t ⇒β t1 ⟹ ∃s. t1 ⟹β s ∧ y ⇒β s" and t2: "t ⇒β t1"
            obtain s where s: "t1 ⟹β s" "y ⇒β s" using hyp t t2 by blast
            obtain s' where s': "s ⇒β s'" "z ⇒β s'" using par_confluent [OF t(2) s(2)] by blast
            have "t1 ⟹β s'" "z ⇒β s'"
              by (rule, rule s, rule s', rule s')
            thus "∃s. t1 ⟹β s ∧ z ⇒β s"
              by blast
          qed
      qed

    have CR_long_long: "⟦ t ⟹β t1; t ⟹β t2 ⟧ ⟹ ∃s. t1 ⟹β s ∧ t2 ⟹β s"
      apply (induct arbitrary: t2 rule: rtranclp_induct)
        apply (rule, rule, simp, simp)
        using CR_one_long apply (meson rtranclp.rtrancl_into_rtrancl)
      done

    have "t ⟹β t1" "t ⟹β t2"
      using assms by (simp add: long_pb_iff_long_b, simp add: long_pb_iff_long_b)
    hence "∃s. t1 ⟹β s ∧ t2 ⟹β s"
      by (rule CR_long_long)
    hence "∃s. t1 ⟶β s ∧ t2 ⟶β s"
      by (simp add: long_pb_iff_long_b)
    thus "(⋀s. t1 ⟶β s ⟹ t2 ⟶β s ⟹ thesis) ⟹ thesis"
      by blast
  qed

長いので順番に行こう。

最初に、 CR_one_long: "⋀t t1 t2. ⟦ t ⟹β t2; t ⇒β t1 ⟧ ⟹ ∃s. t1 ⟹β s ∧ t2 ⇒β s" が成り立つ。これはlong_par_betaと1step par_betaでconfluentであることを言っている。 confluentはよく菱形の図で表現されるが、これは片方が長くてもう片方が短い矢印が長方形を歪めたような形で合流するみたいな感じである(伝わるかなぁ？)。

次に、 CR_long_long: "⟦ t ⟹β t1; t ⟹β t2 ⟧ ⟹ ∃s. t1 ⟹β s ∧ t2 ⟹β s" が成り立つ。これはlong_par_betaとlong_par_betaのconfluentで、大きな菱形の合流性である(伝わるかなぁ？その2)。

結論としてはlong_par_beta同士も合流するよということが言えた。 そしてこれとlong_par_betaがlong_betaと同値であったことを組み合わせれば、long_betaの合流性が言えるのも分かるだろう。

というわけで以上により、Church-Rosserが成り立つ。

まとめ

結構大変だったけれど一応CRが示せたのでよかった。 説明があまりに雑すぎて伝わる気がしないし、Isabelleでの証明の説明をしつつラムダ計算の解説もしては流石にキツイということが分かった。

とりあえず、あの面倒なChurch-RosserもNominal Isabelleでなら頑張れば示せるぜ！ということが伝わればいいかなと。 実際この証明は手で示すのもこんな感じで結構大変だし、Isabelleだから煩雑になった部分は最初の補題いくつかくらいであとは手の証明と大体同じ流れでいけるので、Nominal Isabelleってすごいなって思ってもらえるかと思います。 正直これを普通のIsabelleで示すとか考えただけで目眩がするので(strong_inductが使えなくて変数の取り直しを手動でしないといけない！)ラムダ計算やりたい各位はぜひぜひ使っていきましょう。

次回はsimply-typedのtype soundnessを1日で(！)示します。