逻辑向更高类型可行性问题的若干应用
计算机科学中的逻辑
2007-05-23 v1
摘要
本文演示了基本可行函数类具有递归论性质，这些性质自然推广了可行函数类相应的性质。我们改进了 Kapron-Cook 关于基本可行函数机器表示的结果。我们的证明基于基本的逻辑应用。我们引入了一个弱的第二阶算术片段，其中第二阶变量范围是从 N 到 N 的函数，这足以特征化基本可行函数，并表明它是调查基本可行函数性质的有用工具。特别是，我们提供了一个示例，说明如何从使用非可行函数（如二次多项式）的数学证明中提取可行“程序”。
引用
@article{arxiv.cs/0204045,
title = {Some applications of logic to feasibility in higher types},
author = {Aleksandar Ignjatovic and Arun Sharma},
journal= {arXiv preprint arXiv:cs/0204045},
year = {2007}
}