如何在抽象树中表示替换的 kleisli 组合
How to represent kleisli composition of substitutions in abstract trees
上下文： 我一直在尝试实现统一算法（找到两个抽象语法树的最一般统一器的算法）。由于统一器是一个替换，因此算法需要定义替换的组合。
具体来说，给定一个类型 treeSigma 依赖于另一个类型 X，替换是类型的函数：
X -> treeSigma X
并且函数 substitute 将替换作为输入并具有类型
substitute: (X-> (treeSigma X))-> (treeSigma X) -> (treeSigma X)
我需要定义一个函数来组合两个替换：
compose_kleisli (rho1 rho2: X->(treeSigma X)) : (treeSigma X) := ...
such that,
forall tr: treeSigma X,
substitute (compose_kleisli rho1 rho2) tr = substitute rho1 (substitute rho2 tr).
我对 coq 还很陌生，一直在定义这个组合。
如何定义这个构图？
我尝试使用 Record 来定义它，如下所示：
Record compose {X s} (rho1 rho2: X-> treeSigma X):= mkCompose{
RHO: X-> treeSigma X;
CONDITION: forall t, substitute RHO t = substitute rho2 (substitute rho1 t)
}.
但除此之外，我还需要证明可以为任意两个替换定义组合的结果。类似于：
Theorem composeTotal: forall {X s} (rho1 rho2: X-> treeSigma s X), exists rho3,
forall t, substitute rho3 t = substitute rho2 (substitute rho1 t).
证明这一点需要构造 rho3，它又回到定义 compose 的相同问题。
treeSigma 定义为：
(* Signature *)
Record sigma: Type := mkSigma {
symbol : Type;
arity : symbol -> nat
}.
Record sigmaLeaf (s:sigma): Type := mkLeaf {
cLeaf: symbol s;
condLeaf: arity s cLeaf = 0
}.
Record sigmaNode (s:sigma): Type := mkNode {
fNode: symbol s;
condNode: arity s fNode <> 0
}.
(* Sigma Algebra *)
Record sigAlg (s:sigma) (X:Type) := mkAlg {
Carrier: Type;
meaning: forall f:(sigmaNode s), (Vector.t Carrier (arity s (fNode s f))) -> Carrier;
meanLeaf: forall f:(sigmaLeaf s), Vector.t Carrier 0 -> Carrier
}.
(* Abstract tree on arbitrary signature. *)
Inductive treeSigma (s:sigma) (X:Type):=
| VAR (x:X)
| LEAF (c: sigmaLeaf s)
| NODE (f: sigmaNode s) (sub: Vector.t (treeSigma s X) (arity s (fNode s f)) ).
(* Defining abstract syntax as a sigma algebra. *)
Definition meanTreeNode {s X} (f:sigmaNode s) (sub: Vector.t (treeSigma s X) (s.(arity)
(fNode s f))): treeSigma s X:= NODE s X f sub.
Definition meanTreeLeaf {s X} (c:sigmaLeaf s) (sub: Vector.t (treeSigma s X) 0) := LEAF s X c.
Definition treeSigAlg {s X} := mkAlg s X (treeSigma s X) meanTreeNode meanTreeLeaf.
替换函数定义为：
Fixpoint homoSigma1 {X:Type} {s} (A: sigAlg s X) (rho: X-> (Carrier s X A))
(wft: (treeSigma s X)) {struct wft}: (Carrier s X A) :=
match wft with
| VAR _ _ x => rho x
| LEAF _ _ c => meanLeaf s X A c []
| NODE _ _ f l2 => meanNode s X A f (
(fix homoSigVec k (l2:Vector.t _ k):= match l2 with
| [] => []
| t::l2s => (homoSigma1 A rho t):: (homoSigVec (vlen _ l2s) l2s)
end)
(arity s (fNode s f)) l2)
end.
Definition substitute {X s} (rho: X-> treeSigma s X) (t: treeSigma s X) := @homoSigma1 X s treeSigAlg rho t.
具体来说，替换是rho的同态扩展（这是一个变量值）。
为此，您需要使用 monad 的操作，通常是：
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section MonadKleisli.
(* Set Universe Polymorphism. // Needed for real use cases *)
Variable (M : Type -> Type).
Variable (Ma : forall A B, (A -> B) -> M A -> M B).
Variable (η : forall A, A -> M A).
Variable (μ : forall A, M (M A) -> M A).
(* Compose: o^* *)
Definition oStar A B C (f : A -> M B) (g: B -> M C) : A -> M C :=
fun x => μ (Ma g (f x)).
(* Bind *)
Definition bind A B (x : M A) (f : A -> M B) : M B := oStar (fun _ => x) f tt.
End MonadKleisli.
根据您组织定义的方式，证明您想要的属性可能需要功能扩展性，这通常不是什么大问题，但需要牢记。
像这样的定义很难处理，因为树类型在另一个归纳类型中递归出现。 Coq 无法自行生成这些类型的归纳原理，因此您需要稍微帮助一下。这是一个可能的解决方案，用于稍微简化的设置：
Require Import Coq.Vectors.Vector.
Import VectorNotations.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section Dev.
Variable symbol : Type.
Variable arity : symbol -> nat.
Record alg := Alg {
alg_sort :> Type;
alg_op : forall f : symbol, Vector.t alg_sort (arity f) -> alg_sort;
}.
Arguments alg_op {_} f _.
(* Turn off the automatic generation of induction principles.
This tree type does not distinguish between leaves and nodes,
since they only differ in their arity. *)
Unset Elimination Schemes.
Inductive treeSigma (X:Type) :=
| VAR (x:X)
| NODE (f: symbol) (args : Vector.t (treeSigma X) (arity f)).
Arguments NODE {X} _ _.
Set Elimination Schemes.
(* Manual definition of a custom induction principle for treeSigma.
HNODE is the inductive case for the NODE constructor; the vs argument is
saying that the induction hypothesis holds for each tree in the vector of
arguments. *)
Definition treeSigma_rect (X : Type) (T : treeSigma X -> Type)
(HVAR : forall x, T (VAR x))
(HNODE : forall f (ts : Vector.t (treeSigma X) (arity f))
(vs : Vector.fold_right (fun t V => T t * V)%type ts unit),
T (NODE f ts)) :
forall t, T t :=
fix loopTree (t : treeSigma X) : T t :=
match t with
| VAR x => HVAR x
| NODE f ts =>
let fix loopVector n (ts : Vector.t (treeSigma X) n) :
Vector.fold_right (fun t V => T t * V)%type ts unit :=
match ts with
| [] => tt
| t :: ts => (loopTree t, loopVector _ ts)
end in
HNODE f ts (loopVector (arity f) ts)
end.
Definition treeSigma_ind (X : Type) (T : treeSigma X -> Prop) :=
@treeSigma_rect X T.
Definition treeSigma_alg (X:Type) : alg := {|
alg_sort := treeSigma X;
alg_op := @NODE X;
|}.
Fixpoint homoSigma {X : Type} {Y : alg} (ρ : X -> Y) (t : treeSigma X) : Y :=
match t with
| VAR x => ρ x
| NODE f xs => alg_op f (Vector.map (homoSigma ρ) xs)
end.
Definition substitute X (ρ : X -> treeSigma X) (t : treeSigma X) : treeSigma X :=
@homoSigma X (treeSigma_alg X) ρ t.
(* You can define composition simply by applying using substitution. *)
Definition compose X (ρ1 ρ2 : X -> treeSigma X) : X -> treeSigma X :=
fun x => substitute ρ1 (ρ2 x).
(* The property you are looking for follows by induction on the tree. Note
that this requires a nested induction on the vector of arguments. *)
Theorem composeP X (ρ1 ρ2 : X -> treeSigma X) t :
substitute (compose ρ1 ρ2) t = substitute ρ1 (substitute ρ2 t).
Proof.
unfold compose, substitute.
induction t as [x|f ts IH]; trivial.
simpl; f_equal.
induction ts as [|n t ts IH']; trivial.
simpl.
destruct IH as [e IH].
rewrite e.
f_equal.
now apply IH'.
Qed.
End Dev.
上下文： 我一直在尝试实现统一算法（找到两个抽象语法树的最一般统一器的算法）。由于统一器是一个替换，因此算法需要定义替换的组合。
具体来说，给定一个类型 treeSigma 依赖于另一个类型 X，替换是类型的函数：
X -> treeSigma X
并且函数 substitute 将替换作为输入并具有类型
substitute: (X-> (treeSigma X))-> (treeSigma X) -> (treeSigma X)
我需要定义一个函数来组合两个替换：
compose_kleisli (rho1 rho2: X->(treeSigma X)) : (treeSigma X) := ...
such that,
forall tr: treeSigma X,
substitute (compose_kleisli rho1 rho2) tr = substitute rho1 (substitute rho2 tr).
我对 coq 还很陌生，一直在定义这个组合。 如何定义这个构图？
我尝试使用 Record 来定义它，如下所示：
Record compose {X s} (rho1 rho2: X-> treeSigma X):= mkCompose{
RHO: X-> treeSigma X;
CONDITION: forall t, substitute RHO t = substitute rho2 (substitute rho1 t)
}.
但除此之外，我还需要证明可以为任意两个替换定义组合的结果。类似于：
Theorem composeTotal: forall {X s} (rho1 rho2: X-> treeSigma s X), exists rho3,
forall t, substitute rho3 t = substitute rho2 (substitute rho1 t).
证明这一点需要构造 rho3，它又回到定义 compose 的相同问题。
treeSigma 定义为：
(* Signature *)
Record sigma: Type := mkSigma {
symbol : Type;
arity : symbol -> nat
}.
Record sigmaLeaf (s:sigma): Type := mkLeaf {
cLeaf: symbol s;
condLeaf: arity s cLeaf = 0
}.
Record sigmaNode (s:sigma): Type := mkNode {
fNode: symbol s;
condNode: arity s fNode <> 0
}.
(* Sigma Algebra *)
Record sigAlg (s:sigma) (X:Type) := mkAlg {
Carrier: Type;
meaning: forall f:(sigmaNode s), (Vector.t Carrier (arity s (fNode s f))) -> Carrier;
meanLeaf: forall f:(sigmaLeaf s), Vector.t Carrier 0 -> Carrier
}.
(* Abstract tree on arbitrary signature. *)
Inductive treeSigma (s:sigma) (X:Type):=
| VAR (x:X)
| LEAF (c: sigmaLeaf s)
| NODE (f: sigmaNode s) (sub: Vector.t (treeSigma s X) (arity s (fNode s f)) ).
(* Defining abstract syntax as a sigma algebra. *)
Definition meanTreeNode {s X} (f:sigmaNode s) (sub: Vector.t (treeSigma s X) (s.(arity)
(fNode s f))): treeSigma s X:= NODE s X f sub.
Definition meanTreeLeaf {s X} (c:sigmaLeaf s) (sub: Vector.t (treeSigma s X) 0) := LEAF s X c.
Definition treeSigAlg {s X} := mkAlg s X (treeSigma s X) meanTreeNode meanTreeLeaf.
替换函数定义为：
Fixpoint homoSigma1 {X:Type} {s} (A: sigAlg s X) (rho: X-> (Carrier s X A))
(wft: (treeSigma s X)) {struct wft}: (Carrier s X A) :=
match wft with
| VAR _ _ x => rho x
| LEAF _ _ c => meanLeaf s X A c []
| NODE _ _ f l2 => meanNode s X A f (
(fix homoSigVec k (l2:Vector.t _ k):= match l2 with
| [] => []
| t::l2s => (homoSigma1 A rho t):: (homoSigVec (vlen _ l2s) l2s)
end)
(arity s (fNode s f)) l2)
end.
Definition substitute {X s} (rho: X-> treeSigma s X) (t: treeSigma s X) := @homoSigma1 X s treeSigAlg rho t.
具体来说，替换是rho的同态扩展（这是一个变量值）。
为此，您需要使用 monad 的操作，通常是：
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section MonadKleisli.
(* Set Universe Polymorphism. // Needed for real use cases *)
Variable (M : Type -> Type).
Variable (Ma : forall A B, (A -> B) -> M A -> M B).
Variable (η : forall A, A -> M A).
Variable (μ : forall A, M (M A) -> M A).
(* Compose: o^* *)
Definition oStar A B C (f : A -> M B) (g: B -> M C) : A -> M C :=
fun x => μ (Ma g (f x)).
(* Bind *)
Definition bind A B (x : M A) (f : A -> M B) : M B := oStar (fun _ => x) f tt.
End MonadKleisli.
根据您组织定义的方式，证明您想要的属性可能需要功能扩展性，这通常不是什么大问题，但需要牢记。
像这样的定义很难处理，因为树类型在另一个归纳类型中递归出现。 Coq 无法自行生成这些类型的归纳原理，因此您需要稍微帮助一下。这是一个可能的解决方案，用于稍微简化的设置：
Require Import Coq.Vectors.Vector.
Import VectorNotations.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section Dev.
Variable symbol : Type.
Variable arity : symbol -> nat.
Record alg := Alg {
alg_sort :> Type;
alg_op : forall f : symbol, Vector.t alg_sort (arity f) -> alg_sort;
}.
Arguments alg_op {_} f _.
(* Turn off the automatic generation of induction principles.
This tree type does not distinguish between leaves and nodes,
since they only differ in their arity. *)
Unset Elimination Schemes.
Inductive treeSigma (X:Type) :=
| VAR (x:X)
| NODE (f: symbol) (args : Vector.t (treeSigma X) (arity f)).
Arguments NODE {X} _ _.
Set Elimination Schemes.
(* Manual definition of a custom induction principle for treeSigma.
HNODE is the inductive case for the NODE constructor; the vs argument is
saying that the induction hypothesis holds for each tree in the vector of
arguments. *)
Definition treeSigma_rect (X : Type) (T : treeSigma X -> Type)
(HVAR : forall x, T (VAR x))
(HNODE : forall f (ts : Vector.t (treeSigma X) (arity f))
(vs : Vector.fold_right (fun t V => T t * V)%type ts unit),
T (NODE f ts)) :
forall t, T t :=
fix loopTree (t : treeSigma X) : T t :=
match t with
| VAR x => HVAR x
| NODE f ts =>
let fix loopVector n (ts : Vector.t (treeSigma X) n) :
Vector.fold_right (fun t V => T t * V)%type ts unit :=
match ts with
| [] => tt
| t :: ts => (loopTree t, loopVector _ ts)
end in
HNODE f ts (loopVector (arity f) ts)
end.
Definition treeSigma_ind (X : Type) (T : treeSigma X -> Prop) :=
@treeSigma_rect X T.
Definition treeSigma_alg (X:Type) : alg := {|
alg_sort := treeSigma X;
alg_op := @NODE X;
|}.
Fixpoint homoSigma {X : Type} {Y : alg} (ρ : X -> Y) (t : treeSigma X) : Y :=
match t with
| VAR x => ρ x
| NODE f xs => alg_op f (Vector.map (homoSigma ρ) xs)
end.
Definition substitute X (ρ : X -> treeSigma X) (t : treeSigma X) : treeSigma X :=
@homoSigma X (treeSigma_alg X) ρ t.
(* You can define composition simply by applying using substitution. *)
Definition compose X (ρ1 ρ2 : X -> treeSigma X) : X -> treeSigma X :=
fun x => substitute ρ1 (ρ2 x).
(* The property you are looking for follows by induction on the tree. Note
that this requires a nested induction on the vector of arguments. *)
Theorem composeP X (ρ1 ρ2 : X -> treeSigma X) t :
substitute (compose ρ1 ρ2) t = substitute ρ1 (substitute ρ2 t).
Proof.
unfold compose, substitute.
induction t as [x|f ts IH]; trivial.
simpl; f_equal.
induction ts as [|n t ts IH']; trivial.
simpl.
destruct IH as [e IH].
rewrite e.
f_equal.
now apply IH'.
Qed.
End Dev.