这是我在 Coq 项目中使用的多态二叉树的定义。
Inductive tree { X : Type } : Type :=
| t_a : X -> tree
| t_m : tree -> tree -> tree.
使用此定义声明的自然数二叉树( 1 ( ( 2 3 ) 4 ) ) 将是:
t_m ( t_a 1 ) ( t_m ( t_m ( t_a 2 ) ( t_a 3 ) ) ( t_a 4 ) )
正如您所看到的，随着叶子数量的增加，定义很快就会变得不可用。我想要做的是为树定义一个 Unlambda 风格的表示法，以便我可以将上面的内容替换为
' 1 ' ' 2 3 4
这可能吗？
最佳答案
我试图找到一个仅使用 Coq 符号的解决方案，但无法让它工作。我怀疑 Coq 的可扩展解析器不够强大，无法理解您想要的符号。然而，有一个涉及依赖类型的穷人解决方案。这个想法是为该表示法编写一个解析器，并使用该解析器的类型来编码解析器状态。该类型表示解析器“读取”某个标记(实际上，将该标记作为函数调用的参数)，并进入某个下一个状态，取决于它刚刚读取的标记。 p>
不过，有一个小微妙之处，那就是不能仅使用常规 Coq 函数类型来编写该类型，因为该函数所采用的参数数量将取决于它所应用的所有参数。一种解决方案是使用共归纳类型来编码此行为，声明强制以使其看起来像函数:
Inductive tree (X : Type) : Type :=
| t_a : X -> tree X
| t_m : tree X -> tree X -> tree X.
Arguments t_a {X} _.
Arguments t_m {X} _ _.
CoInductive tree_builder X : nat -> Type :=
| TbDone : tree X -> tree_builder X 0
| TbRead : forall n, (forall o : option X, tree_builder X match o with
| Some x => n
| None => S (S n)
end) ->
tree_builder X (S n).
Arguments TbDone {X} _.
Arguments TbRead {X} _ _.
(* Destructors for tree_builder *)
Definition case0 {X} (x : tree_builder X 0) : tree X :=
match x with
| TbDone t => t
end.
Definition caseS {X n} (x : tree_builder X (S n)) :
forall o : option X, tree_builder X match o with
| Some x => n
| None => S (S n)
end :=
match x with
| TbRead _ f => f
end.
Definition tb X n := tree_builder X (S n).
(* force is what does the magic here: it takes a tb and coerces it to a
function that may produce another tb, depending on what it is applied to. *)
Definition force X n (x : tb X n) : forall o : option X,
match o with
| Some x =>
match n with
| 0 => tree X
| S n' => tb X n'
end
| None =>
tb X (S n)
end :=
fun o =>
match o return tree_builder X match o with
| Some x => n
| None => S (S n)
end ->
match o with
| Some x => match n with
| 0 => tree X
| S n' => tb X n'
end
| None => tb X (S n)
end
with
| Some x => match n return tree_builder X n -> match n with
| 0 => tree X
| S n' => tb X n'
end
with
| 0 => fun t => case0 t
| S _ => fun t => t
end
| None => fun t => t
end (caseS x o).
Coercion force : tb >-> Funclass.
那么，我们的解析器只是一个tb X 0类型的术语。正如通常所做的那样，由于参数数量可变，因此必须以连续传递风格编写。
Fixpoint parser_cont_type X (n : nat) : Type :=
match n with
| 0 => tree X
| S n' => tree X -> parser_cont_type X n'
end.
CoFixpoint parser X n : parser_cont_type X n -> tree_builder X n :=
match n with
| 0 => fun k => TbDone k
| S n' => fun k : tree X -> parser_cont_type X n' =>
TbRead n' (fun o => match o return tree_builder X match o with
| Some _ => n'
| None => S (S n')
end
with
| Some x => parser X n' (k (t_a x))
| None => parser X (S (S n')) (fun (t1 t2 : tree X) => k (t_m t1 t2))
end)
end.
Definition parser' X : tb X 0 :=
parser X 1 (fun t => t).
接下来，我们可以定义一些额外的符号以使其更易于使用:
Notation "[ x ]" := (Some x) (at level 0).
Notation "''" := None (at level 0).
Notation "!" := (parser' _) (at level 20).
例如，以下是编写示例树的方法:
Definition my_tree : tree nat := Eval hnf in ! '' [1] '' '' [2] [3] [4].
注意初始的 ! 来启动对解析器的调用，以及标记叶子所需的 [] 。我也无法让 Coq 的解析器接受 ' 作为其自身的标记。然而，除了这些小细节之外，它与您所拥有的相当接近。
一个问题是，由于解析器是使用 Coq 函数定义的，因此需要进行一点简化才能获得与最初的术语完全相同的术语。这就是我在定义上添加 Eval 调用的原因。这可能不像真正的符号那么实用，而且定义确实有点棘手，但在某些情况下可能非常有用。
这是一个gist与整个 .v 文件。
更新:我写了一个post该技术的简化版本变得更加通用。
关于binary-tree - 在 Coq 中定义 Unlambda 风格的树表示法，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/26208107/