我一直在尝试使用Concrete Semantics(为Coq Isabelle/HOL编写)使用Agda编写和验证编译器，以作为引用点。我正在为该文本中使用的相同语言定义编译。
就上下文而言，我已经完成了编译器的编写，并且现在处于验证阶段，但是在机器指令执行的定义上，我必须对具体语义学做出重大贡献。在Agda中，这种区别似乎是必要的，但现在使验证阶段变得异常复杂。
在尝试执行具体语义中给出的指令执行的简化版本时，我遇到了这条线，这可以解释为什么我在将其直接转换为Agda时遇到了麻烦:
对hd []的定义不足是什么意思？这是否等同于在Agda中具有不完整的模式？
汇编指令执行功能严重依赖hd。在我在Agda中实现它的过程中，我为多个类型提供了索引，以使我能够证明堆栈始终具有最少数量的元素，从而避免了不完全的模式匹配问题。现在，我正在尝试验证编译器，证明比“具体语义”中的证明要复杂得多，因为我必须使用这些索引。
我是否缺少某些内容，或者由于未定义hd []而在《具体语义》中的证明不完整吗？
最佳答案
Isabelle/HOL中的hd []已定义；它有一个值(value)，但您对此值(value)一无所知。可以证明hd [] = hd []是因为x = x适用于所有x，但是您无法证明hd []上的其他任何内容(非平凡的)。
它们不是不完整的。依赖hd的行为的证明很可能会假设hd所调用的列表是非空的，或者基于其他假设证明它是非空的。
关于compiler-construction - Coq中的部分函数/未定义？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/53434947/