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 *)

例如，要查找自由变量，我需要在变量案例和绑定案例中做一些有趣的事情，但对于其他所有事情，我只是递归地找到子表达式的所有自由变量，然后将这些列表合并在一起。对于生成所有约束列表的函数也是如此。替换情况有点棘手，因为三个函数的结果类型不同，用于组合子表达式的构造函数也不同：

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 的定义仅按名称提及了一个构造函数 aaa，所有其他构造函数都以系统的方式处理。我们使用类型信息来检测我们想要在其中执行递归下降的那些子组件。如果您有多个相互归纳的类型，您可以向 generic_process 函数添加参数，以指示哪个函数将用于每种类型并具有更多子句，每个子句用于每种类型的每个参数。

这是对这个想法的测试，其中语言有 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 回答
2

这是另一种方式，虽然它不是每个人的一杯茶。

这个想法是将递归从类型和评估器中移出，改为参数化它，并将表达式值转换为折叠。这在某些方面提供了便利，但在其他方面提供了更多的努力——这实际上是一个你最终花费最多时间的问题。好的方面是评估器可以很容易编写，并且您不必处理相互递归的定义。然而，一些在其他方面更简单的事情可能会成为这种风格的脑筋急转弯。

Require Import Ssreflect.ssreflect.
Require Import Ssreflect.ssrbool.
Require Import Ssreflect.eqtype.
Require Import Ssreflect.seq.
Require Import Ssreflect.ssrnat.

Inductive ExprF (d : (Type -> Type) -> Type -> Type)
                (c : Type -> Type) (e : Type) : Type :=
  | eLambda  (x:nat) (e':e)
  | eVar     (x:nat)
  | eAscribe (e':e)  (t:d c e)
  | ePlus    (e1:e) (e2:e).

Inductive DTypeF (c : Type -> Type) (e : Type) : Type :=
  | tArrow (x:nat) (t:e) (c':c e) (t':e)
  | tInt.

Inductive ConstraintF (e : Type) : Type :=
  | cEq (e1:e) (e2:e).

Definition Mu (f : Type -> Type) := forall a, (f a -> a) -> a.

Definition Constraint := Mu ConstraintF.
Definition DType      := Mu (DTypeF ConstraintF).
Definition Expr       := Mu (ExprF DTypeF ConstraintF).

Definition substInExpr (x:nat) (v:Expr) (e':Expr) : Expr := fun a phi =>
  e' a (fun e => match e return a with
    (* interesting cases *)
    | eLambda y e' =>
        if (x == y) then e' else phi e
    | eVar y =>
        if (x == y) then v _ phi else phi e

    (* boring cases *)
    | _ => phi e
    end).

Definition varNum (x:ExprF DTypeF ConstraintF nat) : nat :=
  match x with
  | eLambda _ e => e
  | eVar y => y
  | _ => 0
  end.

Compute (substInExpr 2 (fun a psi => psi (eVar _ _ _ 3))
                     (fun _ phi =>
                        phi (eLambda _ _ _ 1 (phi (eVar _ _ _ 2)))))
        nat varNum.

Compute (substInExpr 1 (fun a psi => psi (eVar _ _ _ 3))
                     (fun _ phi =>
                        phi (eLambda _ _ _ 1 (phi (eVar _ _ _ 2)))))
        nat varNum.
于 2015-08-04T03:05:42.927 回答