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

Question

我一直在尝试使用 Concrete Semantics 在 Agda 中编写和验证编译器(这是为 Coq Isabelle/HOL 编写的)作为引用点。我正在为该文本中使用的相同语言定义编译。
对于上下文，我已经完成了编译器的编写，现在处于验证阶段，但是我必须在机器指令执行的定义中对具体语义做出重大改变。这种差异在 Agda 中似乎是必要的，但现在使验证阶段变得异常复杂。
在尝试执行 Concrete Semantics 中给出的更简单的指令执行版本时，我遇到了这一行，这可以解释为什么我无法将其直接转换为 Agda:

Also useful are the head of a list, its first element, and the tail, the rest of the list:

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

Note that since HOL is a logic of total functions, hd [] is defined, but we do not know what the result is. That is, hd [] is not undefined but underdefined.

hd []是什么意思被低估？这是否等同于 Agda 中的不完整模式？
汇编指令执行功能严重依赖 hd .在我在 Agda 中的实现中，我为多种类型提供了索引，以允许我构建堆栈始终具有最少元素数量的证明，以避免不完整的模式匹配问题。现在我正在尝试验证编译器，证明比具体语义中的证明复杂得多，因为我必须使用这些索引。
我是不是遗漏了什么，或者具体语义中的证明不完整，hd []没有被定义？

Answer 1

hd []在 Isabelle/HOL 中定义；它有一个值(value)，但你对那个值(value)一无所知。可以证明hd [] = hd []因为 x = x对所有 x 成立，但您将无法在 hd [] 上证明任何其他(非平凡的) .

Am I missing something or are the proofs in Concrete Semantics incomplete with hd [] not being defined?

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