论文标题
直觉固定点逻辑
Intuitionistic Fixed Point Logic
论文作者
论文摘要
我们研究直觉固定点逻辑的IFP，这是通过严格的积极归纳和共同诱导定义的直觉一阶逻辑的扩展。我们定义了对IFP的可靠性解释，并使用它从有关由任意实际上真实脱节的免费公式的抽象结构的证据中提取计算内容。该解释与域理论的指示语义和提取程序功能性语言的相应懒惰操作语义相对于域理论的说法是合理的。我们还展示了如何将提取程序转化为Haskell。作为应用程序，我们提取一个程序，将实数的签名数字表示形式转换为无限的灰代码，从包含相应的共同感应谓词的证明。
We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. We also show how extracted programs can be translated into Haskell. As an application we extract a program converting the signed digit representation of real numbers to infinite Gray-code from a proof of inclusion of the corresponding coinductive predicates.
