5

パターンを何度も繰り返していることに気づき、それを抽象化したいと思います。私は、coq がパターンを捉えるのに十分な表現力を持っているとかなり確信していますが、その方法を理解するのに少し苦労しています。構文用語を表す相互に再帰的な帰納的データ型を持つプログラミング言語を定義しています。

Inductive Expr : Set :=
  | eLambda  (x:TermVar) (e:Expr)
  | eVar     (x:TermVar)
  | eAscribe (e:Expr)  (t:IFType)
  | ePlus    (e1:Expr) (e2:Expr)

  | ... many other forms ...

with DType : Set :=
  | tArrow (x:TermVar) (t:DType) (c:Constraint) (t':DType)
  | tInt

  | ... many other forms ...

with Constraint : Set :=
  | cEq (e1:Expr) (e2:Expr)
  | ...

さて、これらの型に対して定義する必要のある関数がいくつかあります。たとえば、すべての自由変数を検索する関数、置換を実行する関数、およびすべての制約のセットを引き出す関数が必要です。これらの関数はすべて次の形式をとります。

Fixpoint doExpr (e:Expr) := match e with
  (* one or two Interesting cases *)
  | ...

  (* lots and lots of boring cases,
  ** all of which just recurse on the subterms
  ** and then combine the results in the same way
  *)
  | ....

with doIFType (t:IFType) := match t with
  (* same structure as above *)

with doConstraint (c:Constraint) := match c with
  (* ditto *)

たとえば、自由変数を見つけるには、変数のケースとバインディングを行うケースで興味深いことを行う必要がありますが、それ以外の場合は、部分式の自由変数をすべて再帰的に見つけて、それらのリストを結合します。すべての制約のリストを生成する関数についても同様です。3 つの関数の結果の型が異なり、部分式を結合するために使用されるコンストラクターも異なるため、置換のケースはもう少しトリッキーです。

Variable x:TermVar, v:Expr.
Fixpoint substInExpr (e:Expr) : **Expr** := match e with
  (* interesting cases *)
  | eLambda y e' =>
      if x = y then eLambda y e' else eLambda y (substInExpr e')
  | eVar y =>
      if x = y then v else y

  (* boring cases *)
  | eAscribe e' t  => **eAscribe** (substInExpr e') (substInType t)
  | ePlus    e1 e2 => **ePlus**    (substInExpr e1) (substInExpr e2)
  | ...

with substInType       (t:Type)       : **Type** := match t with ...
with substInConstraint (c:Constraint) : **Constraint** := ...
.

これらの関数を記述するのは面倒で、エラーが発生しやすい作業です。関数ごとに興味のないケースをすべて書き出す必要があり、すべてのサブタームを再帰する必要があるからです。私が書きたいのは、次のようなものです。

Fixpoint freeVars X:syntax := match X with
  | syntaxExpr eVar    x         => [x]
  | syntaxExpr eLambda x e       => remove x  (freeVars e)
  | syntaxType tArrow  x t1 c t2 => remove x  (freeVars t1)++(freeVars c)++(freeVars t2)
  | _          _       args      => fold (++) (map freeVars args)
end.

Variable x:TermVar, v:Expr.
Fixpoint subst X:syntax := match X with
  | syntaxExpr eVar y      => if y = x then v else eVar y
  | syntaxExpr eLambda y e => eLambda y (if y = x then e else (subst e))
  | syntaxType tArrow ...

  | _ cons args => cons (map subst args)
end.

このアイデアの鍵は、コンストラクターをいくつかの引数に一般的に適用する機能と、引数の型と数を保持するある種の「マップ」を持つ機能です。

_ のケースが正しくないため、明らかにこの疑似コードは機能しません。だから私の質問は、このように編成されたコードを書くことは可能ですか、それとも退屈なケースをすべて手動でリストアップする運命にあるのでしょうか?

4

2 に答える 2

2

これが進むべき方法ですが、それは非常に読みやすいコードを与えません：戦術を使用してください。

さまざまなアリティのコンストラクターが多数ある言語があり、コンストラクターaaaによって指定された場合にのみ特定の目標を適用し、他のすべてのコンストラクターをトラバースして、下に表示される可能性のあるaaaに到達するとします。彼ら。私は次のことができます：

関数A->B（Aは言語のタイプ）を定義したいとします。どのような場合かを追跡する必要があるため、Aの上にファントムタイプを定義し、Bに減らします。

Definition phant (x : A) : Type := B.

ユニオン関数のタイプはB->B->Bであり、Bにはempty_Bというデフォルト値があると思います。

Ltac generic_process f acc :=
  match goal with
    |- context [phan (aaa _)] => (* assume aaa has arith 1 *)
       intros val_of_aaa_component; exact process_this_value val_of_aaa_component
  | |- _ =>
  (* This should be used when the next argument of the current
     constructor is in type A, you want to process recursively
     down this argument, using the function f, and keep this result
     in the accumulator. *)
     let v := fresh "val_in_A" in
     intros v; generic_process f (union acc (f v))
     (* This clause will fail if val_in_A is not in type A *)
  | |- _ => let v := fresh "val_not_in_A" in
    (* This should be used when the next argument of the current
       constructor is not in type A, you want to ignore it *)
       intros v; generic_process f acc
  | |- phant _ =>
    (* this rule should be used at the end, when all
       the arguments of the constructor have been used. *)
    exact acc
  end.

ここで、証明によって関数を定義します。関数がprocess_aaaと呼ばれているとしましょう。

Definition process_aaa (x : A) : phant x.
fix process_aaa 1.
  (* This adds process_add : forall x:A, phant x. in the context. *)
intros x; case x; generic_process process_aaa empty_B.
Defined.

generic_processの定義では、名前で1つのコンストラクター（aaa）のみが言及されており、他のすべてのコンストラクターは体系的な方法で処理されることに注意してください。タイプ情報を使用して、再帰下降を実行するサブコンポーネントを検出します。相互に帰納的なタイプが複数ある場合は、generic_process関数に引数を追加して、各タイプに使用される関数を示し、各タイプの各引数に1つずつ、さらに多くの句を含めることができます。

これはこのアイデアのテストです。言語には4つのコンストラクターがあり、処理される値はコンストラクターに表示される値でvarあり、型natは別のコンストラクター（c2）でも使用されます。自然数のリストのタイプをタイプとして使用し、B変数nilに遭遇したときの結果として空のリストとシングルトンリストを使用します。この関数は、のすべての出現を収集しますvar。

Require Import List.

Inductive expr : Type :=
  var : nat -> expr
| c1 : expr -> expr -> expr -> expr
| c2 : expr -> nat -> expr
| c3 : expr -> expr -> expr
| c4 : expr -> expr -> expr
.

Definition phant (x : expr) : Type := list nat.

Definition union := (@List.app nat).

Ltac generic_process f acc := 
  match goal with
  |- context[phant (var _)] => exact (fun y => y::nil)
  | |- _ => let v := fresh "val_in_expr" in
        intros v; generic_process f (union acc (f v))
  | |- _ => let v := fresh "val_not_in_expr" in
        intros v; generic_process f acc
  | |-  phant _ => exact acc
  end.

Definition collect_vars : forall x : expr, phant x.
fix collect_vars 1.
intros x; case x; generic_process collect_vars (@nil nat).
Defined.

Compute collect_vars (c1 (var 0) (c2 (var 4) 1)
         (c3 (var 2) (var 3))).

var最後の計算では、期待どおりに値0 4 2および3を含むリストが返されますが、コンストラクター内では発生しなかった1は返されません。

于 2013-03-21T01:44:38.317 に答える