如何使Coq接受以下Fixpoint？ [英] How can I make Coq accept the following Fixpoint?

问题描述

我正在尝试为lambda演算编写一个替代函数，并且在以lambda抽象（\x.e）的方式递归调用e之前，我必须在e中重命名变量。我该如何在Coq中表示这种逻辑？

I am trying to write a substitution function for lambda calculus and in case of lambda abstraction (\x.e) before recursively calling substitution on e, I have to rename variables in e. How can I represent this kind of logic in Coq?

以下是一个极小的示例，其中Coq给出了无法猜测递减参数的错误。在简化替换中，为什么Coq不能使e保持相同的归纳大小？

Following is a bare minimum example for which Coq gives the error that it can not guess the decreasing argument. In the simplified replace why can Coq not get that e remains of same Inductive size?

Fixpoint replace (x: nat) (y: nat) (e: exp): exp := e.

Fixpoint substitute (x: nat) (t: exp) (body: exp): exp :=
match body with
| Abs xp e => Abs 0 (substitute x t (replace x 0 e))
| _ => Unit
end.

实际替换看起来像这样

Fixpoint replace (x: nat) (y: nat) (e: exp): exp :=
match e with
| Val => Val
| Var xp => if beq_nat x xp then Var y else e
| Ref f => Ref (replace x y f)
| Abs xp bd => Abs xp (replace x y bd)
| App e1 e2 => App (replace x y e1) (replace x y e2)
| Deref f => Deref (replace x y f)
| Loc l => Loc l
| Assign e1 e2 => Assign (replace x y e1) (replace x y e2)
| Unit => Unit
end.

推荐答案

通常，Coq不会接受形式 f（x）= f（g（x的子项））。当然，这是有道理的，因为 g 可能会增加项的大小。

In general, Coq will not accept recursive Fixpoints of the form f(x) = f(g(subterm of x)). This makes sense, of course, because g could be a function that increases the size of the term.

通常，解决方案是找到终止点，而不是Fixpoint使用的简单的是子项。在这里，您可以定义一个函数 height：exp-> nat ，对于叶节点为0，否则为子树的 max 。然后，Coq具有几种基于这种度量来定义终止函数的方式，例如程序固定点和功能，或者您甚至可以手动定义一个固定点，该固定点需要一个附加参数来表示高度的界限（如果该参数曾经为0，则返回一个哑数值）。程序修订点将向您提供证明义务，即每次递归调用时度量都会减少，并证明您需要证明一个引理，替换可以保留高度。

In general, a solution is to find a termination measure, other than the plain "is a subterm" which Fixpoint uses. Here, you could define a function height : exp -> nat, which is 0 for the leaf nodes and otherwise the max of subtrees. Coq then has several ways of defining terminating functions based on such a measure, e.g. Program Fixpoint and Function, or you can even manually define a Fixpoint which takes an additional argument representing a bound on the height (and returns a dummy value if that argument ever goes to 0). Program Fixpoint will give you a proof obligation that the measure decreases for each recursive call, and to prove that you will need to prove a lemma that replace preserves the height.

在替换的特定情况下，您可以尝试的另一种技巧是定义一个函数以应用多重替换（从变量到表达式的映射），而不是替换函数一个变量。这样，在Abs情况下，您可以将重命名添加到要应用的替换中，而不是直接执行替换，然后该函数在结构上是递归的。

In the particular case of substitutions, a different trick you can try is to define a function to apply multi-substitutions (maps from variables to expressions), instead of a function to substitute for a single variable. This way, in the Abs-case you can add the renaming to the substitution to be applied rather than doing it directly, and then the function is structurally recursive.

这篇关于如何使Coq接受以下Fixpoint？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！