代码之家 › 专栏 › 技术社区 › Antal Spector-Zabusky

我可以在没有let绑定的情况下在Coq中进行复杂的互递归吗?

mutual-recursion termination coq recursion

2

Antal Spector-Zabusky · 技术社区 · 6 年前

Forest 非空的 Tree Branch 一个保存一个额外的布尔标志,我们可以使用 isOK .

Inductive Forest a : Type
  := Empty    : Forest a
  |  WithTree : Tree a -> Forest a -> Forest a
with Tree a : Type
  := Branch : bool -> a -> Forest a -> Tree a.

Arguments Empty    {_}.
Arguments WithTree {_} _ _.
Arguments Branch   {_} _ _ _.

Definition isOK {a} (t : Tree a) : bool :=
  match t with
  | Branch ok _ _ => ok
  end.

现在,如果忽略这个布尔标志,我们可以编写一对映射函数来将一个函数应用于 森林 或者 树

Fixpoint mapForest_always {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_always f t) (mapForest_always f ts)
  end
with mapTree_always {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_always f ts)
  end.

但是,假设布尔值表示一些有效性检查,这在实际代码中会更复杂。所以我们首先检查布尔值,只有在必要时才真正递归。这意味着我们有相互递归的函数,但其中一个只是处理工作。不幸的是,这不起作用:

Fail Fixpoint mapForest_bad {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_bad f t) (mapForest_bad f ts)
  end
with mapTree_bad {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  if isOK t
  then mapOKTree_bad f t
  else t
with mapOKTree_bad {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_bad f ts)
  end.

mapTree_bad 调用 mapOKTree_bad

地图树 正在做的是一些预处理后的额外步骤。这个总是终止,但考克看不到。为了说服终止检查器,我们可以定义 mapOKTree_good ,这是相同的,但是本地的 let 让 mapForest_good 和 mapTree_good mapOKTree你好 让 -装订:

Fixpoint mapForest_good {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_good f t) (mapForest_good f ts)
  end
with mapTree_good {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  let mapOKTree_good {a} (f : a -> a) (t : Tree a) : Tree a :=
        match t with
        | Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
        end in
  if isOK t
  then mapOKTree_good f t
  else t.

Definition mapOKTree_good {a} (f : a -> a) (t : Tree a) : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
  end.

这很管用,但不好看。有什么方法可以说服COQ终止检查人员接受 _bad 变体,或者 _good 我最好的把戏?对我有用的命令,例如 Program Fixpoint Function ,也是完全合理的解决方案。

1 回复 | 直到 6 年前

1

3

Li-yao Xia 6 年前

非常片面的回答:我们可以重构 mapOKTree_good 中间定义参数化为 mapForest_good 就在它被定义之前。

Definition mapOKTree_good_ {a} mapForest_good
           (f : a -> a) (t : Tree a) : Tree a :=
  match t with
  | Branch ok x ts => Branch ok (f x) (mapForest_good f ts)
  end.

Fixpoint mapForest_good {a} (f : a -> a) (ts0 : Forest a) {struct ts0} : Forest a :=
  match ts0 with
  | Empty         => Empty
  | WithTree t ts => WithTree (mapTree_good f t) (mapForest_good f ts)
  end
with mapTree_good {a} (f : a -> a) (t : Tree a) {struct t} : Tree a :=
  if isOK t
  then mapOKTree_good_ mapForest_good f t
  else t.

Definition mapOKTree_good {a} := @mapOKTree_good_ a mapForest_good.