recursion - 在 Coq 中允许潜在的无限循环
问题描述
我请求您的帮助是因为我想知道是否可以允许在 Coq 中定义潜在的无限固定点,以检查当前定义是否最终产生输出。
我已经尝试过新Unset Guard Checking
命令,我想精确禁用的是递减参数检查(因为我实际上有错误cannot guess decreasing argument of fix
.
我知道在 Coq 中禁用此功能有点可惜,但这只是为了获得一个小的实用程序函数来检查当前定义是否正确,以确保提供递减的参数将在进一步的开发中起作用.
解决方案
Unset Guard Checking
确实禁用递减参数检查。{struct foo}
您可能必须像此示例一样明确指定您希望系统假设减少的参数。
Unset Guard Checking.
Fixpoint y {A} (f : A -> A) {struct f} : A := f (y f).
但是,如果您没有充分的理由,定义可能无限函数的更好方法是添加一个参数来强制终止。
Fixpoint y_opt {A} (lim : nat) (f : A -> A) : option A :=
match lim with
| O => None
| S lim' =>
match y_opt lim' f with
| None => None
| Some x => Some (f x)
end
end.
推荐阅读
- c# - 当我将统一应用程序构建为独立应用程序时,所有着色器都吓坏了?闪烁多色?
- r - 是否有一个 R 函数来过滤一个数据框,其中保留了所有匹配值的列?
- javascript - 长度 - 1 起飞比它应该在 JS
- php - 通过关系创建/保存
- java - 未调用标签提供程序
- reactjs - React Router 在导航之外渲染组件
- javascript - 如何从网页检查 Windows 会话?
- php - 从另一个数组打印目标数组值的正确语法
- html - 元素在父宽度上与空间均匀分布 - Angular Flexlayout 响应式
- turing-machines - 如何确定一种语言是 In R 还是 RE 还是 CoRE