logo标签列表

Coq中归纳数据类型的通用折叠

foldcoq
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.

这个想法的关键在于能够将构造函数应用于若干参数，并且有一种“映射”能够保留参数的类型和数量。

显然，这个伪代码并不能正常工作，因为_的情况是不正确的。所以我的问题是，是否有可能编写这种组织方式的代码，或者我只能手动列出所有无聊的情况？

这似乎很相关，尽管我还没有亲自实践过，所以无法从经验上谈论：http://adam.chlipala.net/cpdt/html/Generic.html - t0yv0
该文件是自动生成的，但你可以在这里查看定义：http://dl.dropbox.com/u/3989078/aflang.v 。为了保护无辜者，我的问题更改了名称 - 文件中的DType是IFType。 - mdgeorge
2个回答
2
这里有一种方法可以实现，但它并不会产生非常易读的代码：使用策略。
假设我有一种语言，其中有许多具有不同元数的构造函数，并且我想仅将特定目标应用于给定的 aaa 构造函数情况，并且我想遍历所有其他构造函数，以到达可能出现在它们下面的 aaa。 我可以执行以下操作：
假设您想要定义一个函数 A -> B（A 是语言类型），您需要跟踪您所处的情况，因此您应该在 A 上定义一个幻影类型，使其减少到 B。
Definition phant (x : A) : Type := B.

我认为联合函数的类型是B -> B -> B，你需要在B中设置一个名为empty_B的默认值。

注：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))).

最后一次计算返回了一个包含值0、4、2和3的列表，这是预期的，但没有出现在var构造函数中的1。
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.
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接