Nominal Isabelleとラムダ計算 その1

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


前回、4日分に分けてIMPのoperational semanticsの証明の解説をしてみました。 今回はより発展的な話題として、Nominal Isabelleを用いてChurch-Rosser性やSimply-typedのsoundnessなどを示してみようと思います。

定理証明に詳しい人ならもうこれだけでつらさが伝わるかと思うのですが、実際証明はかなり大変なので今回は発展編(応用編)としてこの話題を選んでみました。

今回解説するコードは以下に置いてあります。

myuon/CR.thy

前置き

ラムダ計算

この記事をわざわざ読む人はラムダ計算についてはある程度知っている人が多いと思うのですが、簡単に説明をしておきます。

ラムダ計算は計算のモデルとなるべく作られた言語で、「関数を作る・作った関数を呼び出す(関数を適用すること)」の2つの操作を基本とします。 ここでの「計算」とは数を与えたら数を返す、のような、電卓で行われるような最も我々がイメージしやすい計算のことです。ラムダ計算ではこの「計算」を、項を別の項に変換するような操作によって実現します。 これは単に 1+2 という項があったらそれを 3 へと変換する、あるいは f(x)=x+2 という項があるときに、 f(10)12 へと変換する、そういう操作を計算と呼びますというだけなので難しいことはありません。

さてラムダ計算の項(何がラムダ計算の項かはまだちゃんと説明していないけど)は通常変数の付け替えを同一視します。具体的には f(x)=xf(y)=y を区別しないのですが、この同値をα同値と呼びます。

ラムダ計算の定理証明で最も厄介なのはこのα同値性の扱いで、というか定理証明による形式化ではそもそも「同一視」とか「同値関係で割る」みたいな操作を扱うのがめちゃくちゃ苦手です。 これは主に、一般に同一視されているかが計算によって判定可能でないこと1と、同一視された項同士の計算はしばしば(人間は気にしないけど)それらの項の変形の構成に依存するからだと個人的には思っています。

はてさて真面目にラムダ計算の形式化をやると地獄をみますが、そんな時にNominal Isabelleが便利なんですよ〜!っていうのがこの導入です。

Nominal Isabelle

Nominal Isabelleは(ラムダ項だけではなく; ラムダ計算みたい題材が最も威力を発揮することは間違いないが)binderを含むデータ型を扱う際に利用すると便利なライブラリである。 binderは [x]. M のような形をしていて、この束縛変数 x の変数名の付け替えを区別しないような項である。

Nominal Isabelleではこの変数の付け替え、「例えば変数 xy に付け替える」という操作を「置換 (x,y) を作用させる」という操作とみなす、というところからスタートする。 より厳密には次のようなことである: 無限の変数からなる集合 V が与えられている時、 List (V×V) の元を置換と呼ぶ。このとき置換の作用を でかくことにし、 ((x,y)::xs)∙M := xs∙(Mに出現する自由変数xをyに、yをxに書き換えた項); []∙M := M のようにして定める。

上の変数の書き換えの部分は当然項 M が属するデータ型がどのように定義されているかに依存するが、この辺のあれこれをいい感じにやってくれるのがNominal Isabelleであり、Nominal Isabelleが提供するコマンドだったりするわけである。

また、以下でも登場するが、ある変数 x が項 M (複数ある場合はタプルとかにする)に(自由)出現しない、ということを x♯M で表す。

(余談だが、こういうbinderの変数のつらみというのはほか言語でも当然あるので、例えば(こちらはde Bruijn indexを使った代入規則の自動化に限定されてはいるが)Coqのautosubstというライブラリもあって、同じくラムダ計算の定理証明などに威力を発揮するようだ。)

nominal_datatype

はじめに

Nominal IsabelleはHOLのライブラリ群の中に含まれているはずで、 imports "~~/src/HOL/Nominal/Nominal" とかでインポートできる。(~~ でIsabelleがインストールされているパスを表す) ライブラリのコードはNominal theoryそのものがここ、例がここにあるので見ると良いかもしれない。 (例に今回の目標と同じCRを示しているのがあるけれど、(大まかな流れは同じだけど)これは特に見てないので私の証明とは色々違うと思います)

また、チュートリアルというかマニュアルが以下にあるので必要に応じて参照して欲しい。

nominal_datatype_manual.pdf

nominal_datatype

さて御託を並べるのはこのくらいにして、実際の証明の解説に入る。

  atom_decl var

  nominal_datatype lambda =
    Var var
  | App lambda lambda (infixl "$" 120)
  | Abs "«var»lambda" ("lam [_]._" [100,100] 100)

atom_decl はatomicな型を宣言するためのもの(Nominal Isabelleとは関係ない)。

nominal_datatype はdatatypeのようなものであるが、binderを指定すると上にも述べたような置換の作用と関連する大量の補題が全て自動で定義される。 binderの指定は «var» のように行う。

strong_induction

nominal_datatypeで定義された項は内部的には通常のdatatypeをα同値で割った型として定義されるので、通常のdatatypeとは少し挙動が違ったりする。 代わりにnominal_datatype(と他のいくつかのコマンド)は通常のinductionの他にstrong_inductという帰納法を生成する。

lambda.inductlambda.strong_induct を比べてみよう。

  thm lambda.induct

  (⋀var. ?P (Var var)) ⟹
  (⋀lambda1 lambda2. ?P lambda1 ⟹ ?P lambda2 ⟹ ?P (lambda1 $ lambda2)) ⟹
  (⋀var lambda. ?P lambda ⟹ ?P (lam [var].lambda)) ⟹ ?P ?lambda

  thm lambda.strong_induct

  (⋀var z. ?P z (Var var)) ⟹
  (⋀lambda1 lambda2 z.
      (⋀z. ?P z lambda1) ⟹ (⋀z. ?P z lambda2) ⟹ ?P z (lambda1 $ lambda2)) ⟹
  (⋀var lambda z. var ♯ z ⟹ (⋀z. ?P z lambda) ⟹ ?P z (lam [var].lambda)) ⟹
  ?P ?z ?lambda

strong_inductの方には余分な引数 z が追加されており、ラムダ抽象の部分では新たに var ♯ z が帰納法の仮定に追加されている。 この部分がまさにstrong_inductであり、「帰納法を回す際に、binderの変数として与えられた項とはかぶらないものが取れる」ということを言っている。

より正確には、α同値により、「もし仮に lam[x].M のxがzに出現した場合、freshな変数x'をとり、α同値性により lam[x].M = lam[x']. [(x,x')]∙M なので、命題中の M[(x,x')]∙M に、 xx' に取り替えることで最初から x はzの中でfreshなものとしてとってきてもよい」ということを含んでいるのがこのstrong_inductである。

substitution

項の代入を行うsubstitutionを定義しよう。

  nominal_primrec subst ("_[_::=_]" [100,100,100] 120) where
    "(Var x)[y ::= s] = (if x = y then s else Var x)"
  | "(M1 $ M2)[y ::= s] = (M1 [y ::= s]) $ (M2 [y ::= s])"
  | "x♯(y,s) ⟹ (lam [x]. M)[y ::= s] = lam [x]. (M[y ::= s])"
  apply (finite_guess+, auto)
  apply (simp add: abs_fresh)
  apply (fresh_guess+)
  done

nominal_datatypeについてのprimitive recursive functionは nominal_primrec で定義する。 primrecとほぼ同じだが、nominal_primrecは定義に出現している項がいくつかの性質を満たしていることを示す必要がある。 finite_guessfresh_guess を上手く使うとなんとかなることが多い。

また、ラムダ抽象の項に対する代入は当然ながら束縛変数と代入する変数が被らないようにしないと色々まずいのでここでは仮定として追加している。

lemmas for substitution

代入関連の補題を先に示しておく。

  lemma subst_gfresh':
    assumes "x ♯ t" "x ♯ s" "x ≠ y"
    shows "x ♯ t [y ::= s]"
  using assms
  apply (nominal_induct t avoiding: x y s rule: lambda.strong_induct)
    apply (simp add: assms(2))
    apply simp
    apply (metis abs_fresh(1) fresh_prod lambda.fresh(3) simps(3))
  done

まずは、 xts に出現せず y と異なる時、 xt[y::=s] に自由出現であるという補題である。 さてこれを示すためには t についての帰納法をすればよさそうだが、今 t はnominal_datatypeなのでそのままの帰納法は使えない。nominal_datatypeに対する帰納法を行うコマンドに、 nominal_induct がある。

nominal_inductは rule によってどの帰納法を使うか(lambda.strong_induct はnominal_datatypeが自動で導出した帰納法である)を指定する必要がある。 また、strong_inductを用いる場合には avoiding というattributeにより与えれた項にfreshな変数を使って帰納法が回るようになる。

上のstrong_inductのところでみた var ♯ z のzとしてこの avoiding で与えた項をとって帰納法を回すことになる。 言い換えれば、 avoiding:z とかくと t = lam[x].t' の形の時にxがzにfreshであるという仮定を追加することができるようになる。

Nominal Isabelleで最も大切なのがこのstrong_inductを用いたnominal_inductで、このようにbinderに出現する変数を特定の項に被らないようにして帰納法が回せるというのがポイントである。

  lemma subst_fresh: "x ♯ s ⟹ x ♯ t[x ::= s]"
  apply (nominal_induct t avoiding: x s rule: lambda.strong_induct)
  apply (auto simp add: fresh_atm abs_fresh)
  done

  lemma subst_gfresh:
    fixes x y :: var
    assumes "x ♯ t" "x ♯ s"
    shows "x ♯ t [y ::= s]"
  apply (cases "x = y")
    using assms(2) subst_fresh apply blast
    using assms(1) assms(2) subst_gfresh' apply auto
  done

  lemma no_subst: "x ♯ t ⟹ t[x ::= s] = t"
  apply (nominal_induct t avoiding: x s rule: lambda.strong_induct)
    apply (simp add: fresh_atm)
    apply simp
    apply (simp add: abs_fresh(1) fresh_atm)
  done

  lemma substitution:
    assumes "x ≠ y" "x ♯ L"
    shows "M [x ::= N] [y ::= L] = M [y ::= L] [x ::= N [y ::= L]]"
  using assms 
  apply (nominal_induct M avoiding: x y N L rule: lambda.strong_induct)
    apply (simp add: no_subst)
    apply simp
    apply (simp add: fresh_atm subst_gfresh')
  done

あとの補題はさらっと見るだけにしよう。

どれも基本的な補題であるが、最後のsubstitution lemmaは割とよく使われる重要な性質である。 ステートメント自体は有名だが仮定にxとyが異なること、そしてxがLにfreshなことが必要であることに注意しよう。

まとめ

Nominal Isabelleの説明をして補題を示したら長くなってしまったので一旦ここで分割する。 次回はbeta reductionとかの諸々の証明をします。


1

逆に、計算によって判定可能な関係を含む項書換えについては計算機で扱いやすい形でよく使われていると思う