An exercise in dependent types

プログラミング言語の理論を計算機上で記述する際にほとんど常に問題になることの一つに,対象言語の変数の扱い方があります。特に変数を束縛する構文を含む言語(関数型言語はほとんどそう)を扱いたい場合には避けて通れない問題です。何が難しいのか,どういう解決策が考えられるのかといった詳細がまとまっている文献が存在するのかどうか知りませんが,有名かつ重要な問題であり,おそらく古くから認識されていることなのできっと探せばあるでしょう(探してない)。

これを何とかする方法はいろいろ知られていますが (de Bruijn index, higher-order abstract syntax, etc),それらとは別に,依存型を使ってどうにかできないかということを以前からぼんやりと思っていました。一言で言うと,(対象言語の)文脈を表す(メタ言語の)型をまず定義し,それに依存する型として(対象言語)項を表す(メタ言語の)型を定義したらどうだろうか,ということなのですが,例を見るのがわかりやすいでしょう。この記事でも後で出てきますが,その他の例としては cpdt の 9.2.1 にλ計算を書く話があります。ちなみに関連する練習問題も exercises の 0.7 にあります。これは二年半ほど前やってみたらえらく大変だった記憶があります。

ちょっと脱線気味になりますが,背景として何を考えているかということを少し述べておきます。近頃,時間があれば最近自分がやっていたこと(ホーア論理の拡張)を Coq で書いてみたらどうだろうかということを少し思いつつも,あんまり時間がないし単に頑張ったらできましたというだけでは誰も興味を持たないだろうということで手をつけずにいました。ところが先日ちょっと真面目に考えてみたところ,上記と同様の問題が発生するようだ(あるいはもしかしたらもっと深刻かもしれない)ということがすぐにわかりました。同様のといっても手続き型言語のホーア論理なので変数の束縛はないのですが,新しい変数を作るという操作が必要な箇所があるので,たぶん似たようなものなのではないかと。その問題を認識すると同時に,これは依存型を用いる方法で解決しないだろうかとも思いました。実際にやってみないことにはうまくいくかどうかわかりませんし,他の方法で解決しないと思うわけでもありませんが,依存型がこういうときにどれくらい使えるものなのかということには興味があったので,試してみてもいいのではないかと。

そんなことを思ったのと同時に,ちょうど HoTT 本を読んでいたら依存型の扱い方が少し分かってきたような気もしてきていたため,ちょっと依存型を使って何かやってみたかったという動機もあります。ちょうどいい例題になったりしないだろうかと。そこで,まずは練習問題として普通のホーア論理の健全性の証明をやってみることにしました。

以下,ホーア論理そのものについてはきちんと解説してないので適宜調べましょう。確か Software Foundations とかにも書いてあります。

準備

とりあえずいろいろ import しておく。ついでに ssreflect の練習もしようとしています。

Require Import ZArith ssreflect ssrbool eqtype seq.
Set Implicit Arguments.

構文の定義をしなければ始まらないのでまずは構文を定義しよう。と言いたいところですが,その前に変数(として使うためのデータ構造)とそれに関連する操作を定義しなければなりません。

Inductive vtype : Set := VTint | VTbool.

Definition context := seq vtype.

Inductive member : context -> Set :=
| Mhead : forall x c, member (x :: c)
| Mtail : forall x c, member c -> member (x :: c).

Fixpoint type_of_var c (m : member c) : vtype :=
  match m with
    | Mhead x _ => x
    | Mtail _ _ m' => type_of_var m'
  end.

vtype は値の型を表す型(ややこしい)。とりあえず int と bool があることにしてあります。具体的にどういうデータ型が扱えるかは,少なくとも今回はあまり関係がありませんが,bool はあったほうが条件分岐が書きやすそうなので入れました。int でもできますけど。

context が文脈の型。seq は list と同じ。文脈を型の列で表現しているので,型付き de Bruijn index みたいな雰囲気になっている気がします。

member はリストの位置を指すデータ。自然数などを使うと範囲外を指してしまう可能性がありますが,こうやって専用の型を定義してやればそんなことにはなりません。同じものが cpdt にも出てきます。見た目がちょっと違う気もするけどたぶん等価です。

type_of_var は,リストの位置を指し示すデータであるところの member を受け取って,対応する要素を返す関数です。nth みたいなものと思えばよいのですが,必ず対応する要素が存在するのがいいところです。ただし依存型を使うことになるので,扱いにくい場合もあるのが欠点。

構文の定義

構文を定義します。式とプログラムがあります。

Section syntax.
  Variable c : context.

  Parameter unary_ops : vtype -> vtype -> Set.
  Parameter binary_ops : vtype -> vtype -> vtype -> Set.

  Inductive expression : vtype -> Set :=
  | Evar : forall m : member c, expression (type_of_var m)
  | Euop : forall t1 t2,
             unary_ops t1 t2 -> expression t1 -> expression t2
  | Ebop : forall t1 t2 t3,
             binary_ops t1 t2 t3 -> expression t1 -> expression t2 ->
             expression t3.

  Inductive program : Set :=
  | PAssign : forall m : member c, expression (type_of_var m) -> program
  | PSkip : program
  | PSeq : program -> program -> program
  | PIf : expression VTbool -> program -> program -> program
  | PWhile : expression VTbool -> program -> program.
End syntax.

最初に文脈 c を宣言しています。変数の束縛がないので(正確には束縛子がないと言うべきか?),文脈をひとつ固定して,その下でのプログラムとは何かを定義します。関数抽象があると構文定義の途中で文脈が変化するのでこういう書き方はできません。

式を定義するためには演算が必要なのですが,特にどんな演算があるかは今回は重要ではないので parameter として演算の集まりを宣言してしまいます。ただし,引数の型と返り値の型をパラメータにしておきます。例えば足し算とか掛け算(を表す対象言語の演算子)の型は binary_ops VTint VTint VTint,整数の間の大小比較の型は binary_ops VTint VTint VTbool,論理否定の型は unary_ops VTbool VTbool,などとなります。binary までしか宣言してませんが特にそうした理由はなく,三項以上の演算も入れたければ入れられます。

expression が式の型です。int 型と bool 型を分けて,型が合うような式だけが作れるようにしてあります。なんかコンストラクタがたくさん引数をとったりしててややこしく見えるかもしれませんが,式が具体的にどうなってるかはわりとどうでもいい部分だったりするので細かいところは気にしなくてもいいです。

program がプログラムの型です(そのままですが)。大事なのは代入で,ここで最初の引数になっている m が文脈の中のどれを参照する変数かを表しています。代入すべき式の型は m と同じにしなければならないので type_of_var m になります。それ以外はだいたい普通です。if と while の条件式は bool 型にしておきます。

意味論の定義

次に意味論を与えます。式の評価とプログラムの実行の二つに分けられます。まずは式の方から。

Definition denot_of_type (t : vtype) : Type :=
  match t with
    | VTint => Z
    | VTbool => bool
  end.

Definition environment (c : context) :=
  List.fold_right prod unit (List.map denot_of_type c).

Parameter denot_of_uop : forall t1 t2,
                           unary_ops t1 t2 -> denot_of_type t1 -> denot_of_type t2.
Parameter denot_of_bop : forall t1 t2 t3,
                           binary_ops t1 t2 t3 ->
                           denot_of_type t1 -> denot_of_type t2 -> denot_of_type t3.

denot_of_type は,対象言語の型をメタ言語 (Coq) の型に写す関数。

environment は,変数の値を表す型です。context の各要素の denotation をとってから,それらの直積をとります。cpdt では fhlist という名前がついています。例えば c = [VTint, VTbool, VTint] だったら Z * (bool * (Z * unit)) になります。最後に unit がくっついてるのはあまり意味はありません。

denot_of_uop, denot_of_bop は各演算を Coq の関数と対応付けるための関数です。普通は足し算に (+) を対応させたり論理積に andb を対応させたりするマッピングを列挙しますが,今回は演算を具体的に定めずに parameter にしているので,ここも parameter で済ませます。

次は式の評価。

Section eval.
  Fixpoint lookup_env c (env : environment c) (m : member c) :
    denot_of_type (type_of_var m).
    move : env; elim m => /=.
    exact (fun _ _ env => fst env).
    exact (fun _ _ _ _ env => lookup_env _ (snd env) _).
  Defined.

  Variable c : context.
  Variable env : environment c.

  Fixpoint eval_expression t (e : expression c t) : denot_of_type t :=
    match e with
      | Evar m => lookup_env env m
      | Euop _ _ uop e' => denot_of_uop uop (eval_expression e')
      | Ebop _ _ _ bop e' e'' =>
        denot_of_bop bop (eval_expression e') (eval_expression e'')
    end.
End eval.

lookup_env は環境と変数を受け取って,その環境での変数の値を取り出す関数です。なんか型が合うように式を書くのが面倒だったので interactive にやってます。

eval_expression が評価部分です。必要なものはここまでですべて準備されているので簡単です。

次にプログラムの実行。big-step の操作的意味論にします。

Section exec.
  Variable c : context.

  Definition update_env (env : environment c) (m : member c) :
    denot_of_type (type_of_var m) -> environment c.
    move : env; elim : m => /=.
    - exact (fun _ _ p v => (v, snd p)).
    - exact (fun _ _ _ rec p v => (fst p, rec (snd p) v)).
  Defined.

  Inductive exec_program : program c -> environment c -> environment c -> Prop :=
  | Exec_assign : forall m e env,
      exec_program (PAssign m e) env
                   (update_env env m (eval_expression env e))
  | Exec_skip : forall env,
      exec_program (PSkip c) env env
  | Exec_seq : forall p1 p2 env1 env2 env3,
      exec_program p1 env1 env2 ->
      exec_program p2 env2 env3 ->
      exec_program (PSeq p1 p2) env1 env3
  | Exec_if_t : forall (e : expression c VTbool) p1 p2 env1 env2,
      eval_expression env1 e ->
      exec_program p1 env1 env2 ->
      exec_program (PIf e p1 p2) env1 env2
  | Exec_if_f : forall (e : expression c VTbool) p1 p2 env1 env2,
      ~~ eval_expression env1 e ->
      exec_program p2 env1 env2 ->
      exec_program (PIf e p1 p2) env1 env2
  | Exec_while_t : forall (e : expression c VTbool) p env1 env2 env3,
      eval_expression env1 e ->
      exec_program p env1 env2 ->
      exec_program (PWhile e p) env2 env3 ->
      exec_program (PWhile e p) env1 env3
  | Exec_while_f : forall (e : expression c VTbool) p env,
      ~~ eval_expression env e ->
      exec_program (PWhile e p) env env.
End exec.

update_env は代入を処理する関数です。これを定義するための型合わせが楽ではないので,interactive に作ります。

exec_program が実行関係(って訳すんだろうか; execution relation)を表しています。なんか定義が長いですが,中身はよくある big-step semantics をそのまま書いた感じです。

ホーア論理

ようやくホーア論理の定義です。

Section logic.
  Definition assertion c := environment c -> Prop.

  Definition hoare_triple c := (assertion c * program c * assertion c)%type.

assertion (表明って訳すんでしたっけ) は,環境の上の述語です。紙の上でやるときは一階述語論理の論理式だとか言ったりしますが,一階述語論理の構文と意味論をきちんと定義するのが面倒だしそうする必然性もあまり感じないので Prop にします。

hoare_triple は Hoare triple です。そのままです。

  Variable c : context.

  Inductive hoare_provable : hoare_triple c -> Prop :=
  | HAssign : forall m e post,
                hoare_provable
                  ((fun env => post (update_env env m (eval_expression env e))),
                   PAssign m e, post)
  | HSkip : forall post, hoare_provable (post, PSkip c, post)
  | HSeq : forall pre post mid p1 p2,
             hoare_provable (pre, p1, mid) ->
             hoare_provable (mid, p2, post) ->
             hoare_provable (pre, PSeq p1 p2, post)
  | HIf : forall (e : expression c VTbool) p1 p2 pre post,
            hoare_provable ((fun env => pre env /\ eval_expression env e),
                            p1, post) ->
            hoare_provable ((fun env => pre env /\ ~~ eval_expression env e),
                            p2, post) ->
            hoare_provable (pre, PIf e p1 p2, post)
  | HWhile : forall (e : expression c VTbool) p inv,
               hoare_provable ((fun env => inv env /\ eval_expression env e),
                               p, inv) ->
               hoare_provable (inv, PWhile e p,
                               fun env => inv env /\ ~~ eval_expression env e).

推論規則です。代入のところは,assertion の構文をきちんと定義した場合は post の中に現れる m に e を代入した論理式を precondition のところに置きますが,今は assertion language と Coq の Prop とを区別してないので代入とか言っても何のことかよくわかりません。そのかわり,update したあとの環境が post を満たすという形にします。こう書くと何か推論規則を書いているはずなのに意味論を参照しているように見えて変な感じですが。変なのでしょうか,わかりませんが。

健全性

それで健全性を示すわけですが,健全性の主張を述べるためには正しいとはどういうことかを定めなければならないのでまずそれを書きます。

  Definition hoare_valid (ht : hoare_triple c) : Prop :=                           
    let: (pre, p, post) := ht in                                                   
      forall env env', pre env -> exec_program p env env' -> post env'.              

といっても普通の定義です。

で,目標の健全性。

  Theorem hoare_sound : forall ht, hoare_provable ht -> hoare_valid ht.

証明は hoare_provable に関する帰納法ですが,while の場合だけ帰納法の仮定が使えない形になるので,内側で exec_program 関する帰納法を使います。

詳細は読者の演習問題とする。

ではなくて,これがわりと難しかったなーというのが本題なのですが,それはまた後日。