如何使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屋!