嵌套递归类型的非平凡固定点

问题描述 投票：0回答：1

给出 Coq 中二叉树和任意分支树（K 树）的两个标准定义（

nat
为简单起见硬编码）：

Inductive bintree : Type :=
  | Leaf : bintree
  | Node : bintree -> nat -> bintree -> bintree.

Inductive tree :=
  | TNode : nat -> list tree -> tree.

我想定义一个函数 

encode : tree -> bintree
将 K 树转换为具有相同节点的二叉树，最终目标是定义 
decode : bintree -> tree
这样 
forall t, decode (encode t) = t
和这个证明和一些其他次要属性。一个简单的想法如下：我们将节点 
x
和子节点 
ts
的树编码为二叉树，其中左子树被编码为以其最左边的孩子为根的树，右子树被编码为以 
x 的直接邻居为根的树
向右。在 Haskell 中：

data Tree a = TNode a [Tree a]
data BinTree a = Leaf | BNode (BinTree a) a (BinTree a)

encode :: Tree a -> BinTree a
encode t = go [t]
 where
  go [] = Leaf
  go ((TNode x ts) : ts') = BNode (go ts) x (go ts')

Coq 中的一个类似定义是错误的：

Fixpoint encode_list (l: list ntree) :=
  match l with
    | [] => Leaf
    | (TNode x ts) :: ts' => Node (encode_list ts) x (encode_list ts')
  end.

Error: Recursive definition of encode_list is ill-formed.
(* ... *)
Recursive call to encode_list has principal argument equal to "ts" instead of "ts'".
Recursive definition is:
"fun l : list tree =>
 match l with
 | [] => Leaf
 | t :: ts' =>
     match t with
     | TNode x ts => Node (encode_list ts) x (encode_list ts')
     end
 end".

很容易看出 

ts
和 
ts'
都是 
l
的严格子项，但是 Coq 的启发式方法不足以断言这一点。我尝试对 here 中描述的技巧应用类似的技巧，但是编码树是在节点的右兄弟节点的上下文中完成的，因此很难（不可能？）编写给定节点及其兄弟节点的函数) 产生一棵二叉树，但在结构上仅递归其一个参数的结构，即该定义无效，因为我们迭代了两个参数：

(* ns : right siblings of t *)
Fixpoint encode' (t: tree) (ns: list tree) :=
  let '(TNode x cs) := t in
    match cs, ns with
      | [], [] => Node Leaf x Leaf
      | [], n :: ns' => Node Leaf x (encode' n ns')
      | c :: cs', [] => Node (encode' c cs') x Leaf
      | c :: cs', n :: ns' => Node (encode' c cs') x (encode' n ns')
    end.

(* Error: Cannot guess decreasing argument of fix. *)
(* Definition encode (t: tree) = encode' t []. *)

我最终设法通过 

Program Fixpoint
获得了我的第一个定义，其中 
measure
是树列表中的节点总数。但我想知道这是否可以在不诉诸有根据的递归的情况下实现？有人会认为我们应该能够在这种情况下使用嵌套 
fix
函数的技巧，但我没有成功。完整片段如下：

Require Coq.Program.Wf.
Require Import Lia.

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Inductive bintree (A: Type) : Type :=
  | Leaf : bintree A
  | Node : bintree A -> A -> bintree A -> bintree A.

Inductive tree (A: Type) :=
  | TNode : A -> list (tree A) -> tree A.

Definition ntree := tree nat.

Arguments Leaf {A}.
Arguments TNode [A].

Fixpoint n_nodes (t: ntree) :=
  let '(TNode n ns) := t in
  let fix n_nodes_list (l: list ntree) :=
    match l with
      | [] => 0
      | x :: xs => n_nodes x + n_nodes_list xs
    end
  in 1 + n_nodes_list ns.

Fixpoint sum_n_nodes (l: list ntree) :=
  match l with
    | [] => 0
    | t :: ts => n_nodes t + sum_n_nodes ts
  end.

Program Fixpoint encode_list (l: list ntree) {measure (sum_n_nodes l)} :=
  match l with
    | [] => Leaf
    | (TNode x ts) :: ts' => Node (encode_list ts') x (encode_list ts)
  end.

Next Obligation.
destruct ts'; simpl; lia.
Defined.

Next Obligation.
destruct ts.
simpl; lia.
simpl sum_n_nodes at 1.
replace (sum_n_nodes (TNode x (t :: ts) :: ts')) with (1 + n_nodes t + sum_n_nodes ts + sum_n_nodes ts') at 1 by reflexivity.
lia.
Defined.

Definition encode (l: ntree) := encode_list [l].
coq theorem-proving
1个回答
0
投票

您不能仅使用具有递减类型

encode
的参数的递归函数来定义
list tree
，因为它不能在头部递归。相反，你必须有一个函数，其参数类型为 
tree
，它可以在列表的头部调用自己。

当我们说“必须对递减参数的子项进行递归调用”时，“子项”的确切定义有些复杂且违反直觉。它不像“t 是 C t 的子项，其中 C 是构造函数”那样天真。有这种奇怪的情况，其中 

t
是 
TNode n (t :: ts)
的子项，但不是 
t :: ts
的子项（不知何故，因为 
list
没有出现在构造函数 
_ :: _
的第一个参数中，在 
list
的定义中） . 我依稀记得这种微妙之处是有充分理由的，但我想不起来了。

您必须以某种方式将 

encode_list
对列表头部（的内容）的递归调用转换为 
encode
的递归调用。您还需要一个嵌套的递归函数来遍历列表，所以
encode_list
仍然存在。

在有趣的案例中展开

encode
应该是什么，一棵玫瑰树和一片非空森林
TNode n (t :: ts)
。目标是根据 
encode t
重写右侧。 （一般情况下，你可能需要找到一个更复杂的辅助函数，并得到你想要的函数作为它的特例，但幸运的是，在这种情况下它工作得足够简单。）

encode (TNode n (t :: ts)) = Node (encode_list (t :: ts)) n Leaf


encode t
是
encode_list (t :: [])
，它看起来与
encode_list (t :: ts)
相似但不完全相同。

encode_list (t :: []) = Node _ _ Leaf
encode_list (t :: ts) = Node _ _ (encode_list ts)

其中下划线是 

t
的一些函数，为简洁起见我省略了这些函数。 我们可以根据 
encode_list (t :: ts)
重写 
encode t
，方法是用 
encode_list ts
替换它的右子树，使用下面的辅助 
append
函数：

encode_list (t :: ts) = append (encode t) (encode_list ts)

在哪里

append (Node l n r) rr = Node l n rr


Leaf
的
append
情况没有指定，因为它在
encode
的执行中永远不会发生，所以我们可以随意填写：

append Leaf rr = Leaf

在 Coq 中：

Definition append (t rr : bintree) : bintree :=
  match t with
  | Leaf => Leaf (* should not happen *)
  | Node l n _ => Node l n rr
  end.

Fixpoint encode (t : tree) : bintree :=
  let fix encode_list ts' :=
    match ts' with
    | [] => Leaf
    | t' :: ts' => append (encode t') (encode_list ts')
    end in
  match t with
  | TNode n ts => Node (encode_list ts) n Leaf
  end.

该定义的一个技术方面是

encode_list
“嵌套”在
encode
中（
fix
在
Fixpoint
/
fix
内），而不是与
encode
（
fix ... with ...
）相互定义。这在上面的“Haskelly”演示中并不明显，并且依赖于 Coq 类型检查器使用的“subterm”定义的更多技术细节。

或者，您可以通过先定义

append
和
encode
的组合来避免
append
中无用且不雅的分支，并获得
encode
作为特例。的确，在前面
encode
的定义中，它的递归调用都传递给了
append
，我们知道右子树永远是
Leaf
.

(* append_encode t w = append (encode t) w *)
Fixpoint append_encode (t : tree) (w : bintree) : bintree :=
  let fix encode_list ts' :=
    match ts' with
    | [] => Leaf
    | t' :: ts' => append_encode t' (encode_list ts')
    end in
  match t with
  | TNode n ts => Node (encode_list ts) n w
  end.

Definition encode (t : tree) : bintree := append_encode t Leaf.

完整的要点

请注意，没有可以编码为 

tree
的 
Leaf
，因此 
decode
必须是部分的，否则您将不得不以某种方式重新考虑问题陈述。

最新问题
© www.soinside.com 2019 - 2024. All rights reserved.