直觉定点逻辑
摘要：IFP的弹性定点逻辑系统的研究和探讨，它是直观一阶逻辑的扩展，通过正义的归纳和共归纳定义。我们定义了IFP的实现解释，并用它从关于抽象结构的证明中提取出计算内容，这些结构由任意经典真假或无异或公式指定。通过与域论的指称语义和相应的惰性操作语义相结合，该解释被证明是有效的，并且可以从提取的程序中合成出计算结果。我们还展示了如何将提取的程序翻译成Haskell。作为一个应用，我们从相应的共同归纳谓词的包含证明中提取了一个将实数的符号数字表示转换为无限格雷码的程序。
作者：Ulrich Berger, Hideki Tsuiki
论文ID：2002.00188
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-25