从证明中提取总的Amb程序
摘要：支持提取可证明为总体和正确的非确定性和并发程序的逻辑系统CFP（Concurrent Fixed Point Logic）的介绍。CFP是一种直觉主义的一阶逻辑，具有归纳和协同定义，并扩展了两个命题操作符：限制（Rrestriction），一种加强的蕴含，以及用于总体并发的操作符。提取的源是形式CFP证明，目标是一个带有构造函数和递归的λ演算，扩展了一个构造函数Amb（用于McCarthy的amb），该构造函数在操作层面上被解释为全局的天使选择并用于实现非确定性和并发。通过中间的域论语义来证明提取程序的正确性。我们通过提取一个将无限格雷码转换为有符号数字表示的非确定性程序来展示我们系统的有用性。CFP的一个值得注意的特点是其限制和并发的证明规则涉及到经典排中律的变体，这些变体在没有Amb的情况下不会在计算上可解释。
作者：Ulrich Berger, Hideki Tsuiki
论文ID：2307.12454
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-25