Coq中的部分函数/未定义？

Question

我一直在尝试在 Agda 中编写和验证编译器，使用 Concrete Semantics（为 Coq Isabelle/HOL 编写）作为参考点。我正在为该文本中使用的相同语言定义编译。

对于上下文，我已经完成了编译器的编写，现在正处于验证阶段，但是我必须在机器指令执行的定义中对具体语义做出重大改变。这种差异在 Agda 中似乎是必要的，但现在使验证阶段变得异常复杂。

在尝试执行具体语义中给出的更简单的指令执行版本时，我遇到了这一行，这可以解释为什么我无法将其直接翻译成 Agda：

列表的头部（它的第一个元素）和尾部（列表的其余部分）也很有用：

fun hd :: 'a list ⇒ 'a
hd (x # xs) = x

注意，由于HOL是总函数的​​逻辑，所以定义了hd []，但我们不知道结果是什么。 也就是说，hd [] 不是未定义而是未定义。

hd [] 定义不足是什么意思？这是否相当于在 Agda 中有一个不完整的模式？

汇编指令执行功能严重依赖hd。在我在 Agda 中的实现中，我为多种类型提供了索引，以允许我建立堆栈始终具有最少元素数量的证明，以避免不完整的模式匹配问题。现在我正在尝试验证编译器，证明比具体语义中的证明要复杂得多，因为我必须使用这些索引。

我是否遗漏了什么，或者具体语义中的证明不完整，hd [] 未定义？

Answer 1

在 Isabelle/HOL 中定义了hd []；它有一个价值，但你对那个价值一无所知。可以证明hd [] = hd []，因为x = x 适用于所有x，但您将无法证明hd [] 上的任何其他内容（非平凡）。

我是否遗漏了什么，或者具体语义中的证明不完整，未定义 hd []？

它们并不完整。依赖于hd 行为的证明很可能会假设调用hd 的列表是非空的，或者基于其他假设证明它是非空的。