鉴于所有 Agda 程序都会终止，评估策略对指称语义无关紧要，但对性能很重要（如果您曾经运行过 Agda 程序）。

那么，Agda 使用什么评估策略呢？是否使用 codata (♯, ♭) 代替数据更改评估策略？有没有办法强制按需调用又名惰性评估？

我在终止检查时遇到问题，与此问题中描述的问题以及此Agda bug report/feature request中描述的问题非常相似。

问题是说服编译器以下unionWith终止。使用重复键的组合函数，unionWith合并表示为按键排序的（键，值）对列表的两个映射。有限映射的 Key 参数是映射中包含的键的（非紧）下限。（定义这种数据类型的一个原因是提供一个语义域，我可以在其中解释 AVL 树，以证明它们的各种属性。）

我无法将引用问题中讨论的解决方案推广到我的设置。例如，如果我引入一个辅助函数unionWith'，它与 相互递归定义unionWith，在这种情况下从后者调用k' < k：

然后，一旦我通过将第一个丢失的案例替换unionWith'为所需的调用来打结递归结unionWith，它就无法终止检查。

我也尝试引入额外with的模式，但这很复杂，因为需要compare在递归调用中使用结果。with（如果我使用似乎对终止检查器没有帮助的嵌套子句。）

有没有办法使用with模式或辅助功能来进行编译？这似乎是一个足够简单的情况，所以我希望这只是一个知道正确技巧的例子。

（也许 Agda 开发分支中的新终止检查器可以处理这个问题，但我想避免安装开发版本，除非我必须这样做。）

我看到几个不同的研究小组，以及至少一本书，都在谈论使用 Coq 来设计认证程序。对于认证项目的定义是否有共识？据我所知，它真正的意思是程序被证明是完全的并且类型正确。现在，程序的类型可能是非常奇特的东西，例如证明它是非空的、已排序的、所有元素 >= 5 等的列表。但是，最终，它是一个经过认证的程序，只有 Coq 显示的是完全的和类型安全的，所有有趣的问题都归结为最终类型中包含的内容？

编辑 1

根据 wjedynak 的回答，我查看了 Xavier Leroy 的论文“Formal Verification of a Realistic Compiler”，该论文链接在下面的答案中。我认为这包含了一些很好的信息，但我认为可以在Sandrine Blazy 和 Xavier Leroy的论文Mechanized Semantics for the C 语言的 Clight 子集中找到更多信息。这是“形式验证”论文添加优化的语言。在其中，Blazy 和 Leroy 介绍了 Clight 语言的语法和语义，然后在第 5 节讨论这些语义的验证。在第 5 节中，列出了用于验证编译器的不同策略，. 这些是：

1. 人工审核
2. 证明语义的性质
3. 已验证的翻译
4. 测试可执行语义
5. 与替代语义等价

无论如何，可能有几点可以补充，我当然想了解更多。

回到我最初的问题，即认证程序的定义是什么，我仍然有点不清楚。Wjedynak 提供了一个答案，但实际上 Leroy 的工作涉及在 Coq 中创建一个编译器，然后在某种意义上对其进行验证。理论上，现在证明关于 C 程序的事情成为可能，因为我们现在可以进行 C->Coq->proof。从这个意义上说，似乎有这个工作流程我们可以

1. 用X语言编写程序
2. Coq 或其他证明辅助工具中步骤 1 中程序模型的形式。这可能涉及在 Coq 中创建编程语言模型，也可能涉及直接创建程序模型（即在 Coq 中重写程序本身）。
3. 证明模型的一些性质。也许这是对价值观的证明。也许这是陈述等价性的证明（诸如 3=1+2 或 f(x,y)=f(y,x) 之类的东西。）
4. 然后，根据这些证明，调用认证的原始程序。

或者，我们可以在证明辅助工具中创建程序的规范，然后证明关于该规范的属性，而不是程序本身。

无论如何，如果有人有替代定义，我仍然有兴趣听到它们。

假设我有一个值x : A，并且我想定义一个仅包含x.

这是我尝试过的：

有更好的方法吗？

为什么我想要这个的一个例子：如果你在某个集合 A 上有一个幺半群，那么你可以形成一个以 A 作为唯一对象的类别。要在 Agda 中表达这一点，您需要一种方法来编写“仅包含 A 的集合”。

我想证明

（和codomain类似）。

如果我有一个domain返回函数类型域的函数，我可以将证明写为

但我认为不可能写出这样的函数。

有没有办法做到这一点？

一些输入：

此函数从类型向量和结果类型构造函数类型：

这是 Arity-Generic Datatype-Generic Programming 论文中的两个组合器：

一些有效的定义：

乃至：

但这不会进行类型检查：

错误：

有什么问题？

有人如何证明这种平等

? 基本情况很明显

但是之后

给

这

抛出错误：“拒绝解决异构约束 refl ...”。

还有这个

引发错误：“xs₁ != xs₁' 类型为 Vec A l₁...”。我写了这个定义：

但是不知道怎么用。

也许有一些来源，我可以从中了解更多关于 with-expressions 的信息？

谢谢。