算法归约的多种概念与两种逻辑
计算机科学中的逻辑
2011-04-15 v4 逻辑
摘要
在为可计算性逻辑的各个部分寻找公理化的计划中，早先已证明交互式Turing归约的逻辑恰好是Heyting直觉演算的蕴涵片段。这种归约允许对由前件表示的计算资源进行无限制的重复使用。然而，至少同等基本和自然的一种算法归约是不允许这种重复使用的归约。本文表明，将第一种归约的逻辑转化为第二种归约的逻辑，只需从其Gentzen风格公理化中删除收缩规则即可。此外还表明，第一种（Turing）交互式归约具有三种自然版本。虽然这三个版本彼此大不相同，但它们的逻辑行为（在孤立状态下）结果是无法区分的，其共同行为恰好由蕴涵直觉逻辑所刻画。本文的其他贡献包括对一系列新的（有限和有界的）递推操作及相关归约操作的非形式化介绍。关于可计算性逻辑的在线资源可在 http://www.cis.upenn.edu/~giorgi/cl.html 找到。
引用
@article{arxiv.0706.0103,
title = {Many concepts and two logics of algorithmic reduction},
author = {Giorgi Japaridze},
journal= {arXiv preprint arXiv:0706.0103},
year = {2011}
}
评论
To appear in Studia Logica in the Spring of 2009