可计算性逻辑中分支切换复用运算研究

【摘要】可计算性逻辑(ComputabilityLogic)简称CoL,是由Japaridze首先提出的,它将经典逻辑中的真值理论发展成为可计算性的正式理论,是对经典逻辑的发展。在CoL中,我们将可计算性的问题看成是由机器和环境两种角色参加的博弈,问题的可计算性表示存在一个交互图灵机总能在表示这个问题的博弈中取胜；逻辑运算符代表可计算性问题上的运算；逻辑公式的永真性表示是永远可计算的问题。在对博弈和博弈运算的研究中,博弈运算的静态属性是可计算性逻辑中最基础也是非常重要的内容。在CoL中,我们更多关注的是参加博弈的角色在博弈进行过程中会做出什么动作,采取什么策略实现在博弈中取胜,而不关注他们的博弈速度,这就是静态博弈的含义。我们称一个博弈A是静态的,当且仅.当对于博弈的角色(机器或者环境)(?),博弈过程中产生的行程△和r,△是Γ的(?)-延迟,如果Γ是A中的一个使得(?)取胜的行程,那么△也是一个使得(?)取胜行程。因为在CoL中我们研究的博弈都是静态博弈,所以,每一个CoL中的运算都需要具有静态属性。CoL是经典逻辑的扩展,其运算符的语义在CoL中与经典逻辑的语义是一致的。目前,随着CoL的发展,研究者们已经提出了很多新的运算符,其中分支切换(补)复用运算((?)和(?))是目前最难也是最复杂的一种运算。Japaridze已经给出了关于该运算的定义描述,但是没有给出其静态属性证明。这个问题也成为了CoL中的open问题之一。所以,本文主要研究了以下三个问题：切换分支复用运算的静态属性证明、新的切换分支复用运算的静态属性证明、新旧版本的切换分支复用运算的等价性证明。本文给出了正式的分支切换(补)复用运算的定义,在该定义中,我们采用静态博弈的(Lr,Wn)偶对完成了该运算的定义；并且在定义的基础上给出了该运算的静态性证明。证明过程中,我们首先给出了已知结点、外层已知结点的定义。根据证明的需要,我们使用了CoL中的行程延迟的概念。行程延迟是指在整个博弈过程中,参加博弈的机器或者环境会由于各种原因而导致在某个行程中出现一些运算步的延迟。本文给出了一个引理证明,证明了对于一个已知的静态博弈A,如果在(?)A的某一个行程△中由机器或者环境做出了一个非法的步,而且△是r的一个延迟,那么r也是(?)A一个非法步。在(?)和(?)的静态属性证明中,我们使用该引理的结论,简化了△和r在出现非法步时的分析,从而完成了分支切换复用运算的静态属性证明。由于(?)和(?)运算定义的复杂性,使得基于(?)和(?)的推导演绎系统以及应用系统的研究非常迟缓,这也影响了整个CoL研究的进程。所以,我们需要改进传统的(?)和(?)定义,试图寻找更简单的定义。本文提出了一个新的简单的(?)和(?)定义,为了区分之前的传统定义,我们称传统的定义为紧凑版,新的定义称为宽松版。采用(?)T,(?)T分别表示(?)和(?)的紧凑版,使用(?)L,(?)L分别表示(?)和(?)的宽松版。宽松版的分支切换复用运算定义采用位串表示方法,改变了紧凑版定义中对结点的依赖。本文根据定义也完成了宽松版的静态属性证明。在证明中,我们发现使用宽松版定义的分支切换复用运算需要考虑的情况明显减少,利于后续基于该运算的研究。本文介绍了两个版本的分支切换复用运算,为了在后续的基于分支切换复用运算推演系统和应用研究中使用宽松版的分支切换复用运算,我们需要给出两种版本运算的等价性证明。论文中,我们设计了两个交互算法证明了两种版本运算的等价性。由于CoL是基于博弈的交互计算,所以,我们使用了基于交互计算的图灵机模型-易交互计算模型(Easy-PlayMachine)。通过该交互计算模型,我们给出了在CoL中可计算性问题求解步骤、行程和步的产生过程。运算等价性证明的第一个算法是指存在一个EPMε1在博弈(?)TA→(?)LA即(?)T(?)A∨(?)LA中取胜。我们根据博弈设计了一个取胜策略,使得ε1存在并且能够取胜。第二个算法中,我们设计了一个EPMε2,使得它能在博弈(?)L(?)A∨(?)TA中取胜。我们也设计了一个取胜策略,证明这样的ε2存在。本文的主要研究工作和创新点：一、正式的分支切换复用运算的定义和静态属性证明1.我们给出了基于(Lr,Wn)偶对表示形式的分支切换(补)复用运算的定义。该定义主要是基于树形结构的思想,重点针对分支切换复用运算的分支运算和切换运算进行描述。所以,我们将分支运算中已知结点的概念进行了重新的定义,细化给出了外层已知结点的定义。定义了完成分支运算的结点只能是外层已知结点；完成切换运算的可以是任何已知结点。本文在行程延迟概念的基础上,给出了静态属性证明。借助于引理的结果,我们只需要分析两个具有延迟关系的行程。即一个静态博弈A,如果一个行程Γ是(?)A中的一个(?)取胜行程,那么其(?)-延迟行程△也是(?)A中的(?)取胜行程。从而证明了(?)是静态的。二、新的分支切换复用运算的定义和静态属性证明2.我们根据传统的分支切换(补)复用运算定义,采用基于位串的表示方法,给出了一个新的简单版本定义。该定义打破了已知结点的考虑和限制,定义中直接不需要考虑分支运算,简化了整个运算。完成运算定义之后,我们同样给出了新的分支切换复用运算的静态属性证明。在整个证明过程中,我们发现需要考虑和处理的情况明显减少,利于基于分支切换复用运算的一些演绎系统和应用系统的提出。三、两种版本运算等价性证明3.博弈的交互计算特点需要提出新的交互计算模型的概念,根据应用场合不同,论文介绍了难交互计算模型和易交互计算模型,通过这两种计算模型,我们可以理解博弈的进行过程、步和行程的产生过程。在论文中,我们选用对于机器来说更简单的易交互计算模型。事实上,两种计算模型在计算能力上是等价的。4.运算的等价性证明,是指在CoL中设计基于易交互计算模型的算法,使得机器在博弈运算中取胜。论文中设计了两个算法。在第一个算法中,我们证明存在一个EPMε1在博弈(?)T(?)A∨(?)LA中取胜。第二个算法,我们证明了存在一个EPMε2,使得ε2在博弈(?)L(?)A∨(?)TA中存在取胜策略。从而实现了运算的等价性证明。本文的进一步工作主要包括以下几个方面：1.我们计划设计基于宽松版分支切换(补)复用运算的推理系统。包括给出推理系统的推导原则、新的系统的可靠性和完整性证明。我们计划参考Japaridze提出的CL1-CL15的相关证明方法,设计新的CLx推理系统。2.实现基于分支切换(补)复用运算的应用系统。设计与实现CoL的应用系统,实现真正的人机交互运算。为CoL走向具体应用来设计平台和界面。我们已经设计和实现完成了CL1的交互计算应用,这可以为我们的研究提供基础。3.发现不同的计算机应用领域。CoL可以应用在交互计算、网络协议、知识库系统和基于资源的规划系统中。我们需要在这些领域中发现基于分支切换(补)复用运算的实际应用。
【作者】曲美霞；
【导师】朱大铭；GiorgiJaparidze；
【作者基本信息】山东大学，计算机软件与理论，2014，博士
【关键词】可计算性逻辑；静态博弈；交互计算；行程；位置；分支切换复用；一致永真性；

【参考文献】
[1]李雪杰.RNA干扰诱导CD147基因沉默稳定动脉粥样硬化易损斑块的研究[D].南方医科大学,内科学,2012,硕士.
[2]贾佳.《商君书》法律词语研究[D].河北师范大学,汉语言文字学,2012,硕士.
[3]未宏龙.中小学考试分析系统的设计与实现[D].宁夏大学,教育（专业学位）,2014,硕士.
[4]于陆.成都《新民报》副刊《出师表》研究（1943-1945）[D].西南交通大学,传播学,2013,硕士.
[5]王鹤.非病毒载体介导转基因鸡的初步研究[D].河南农业大学,预防兽医学,2012,硕士.
[6]刘少奎.水稻白条纹新基因st9（t）的初步定位[D].南京农业大学,作物遗传育种,2012,硕士.
[7]刘德华.低频超声波穿颅助溶的体外实验性研究[D].重庆医科大学,外科学,2004,硕士.
[8]刘爱华.城市灾害链动力学演变模型与灾害链风险评估方法的研究[D].中南大学,安全科学与工程,2013,博士.
[9]赵耀.心理地位问卷的编制及心理地位与成人依恋的关系[D].首都师范大学,应用心理学,2013,硕士.
[10]杨冬敏.《红楼梦》中称谓词的翻译[D].陕西师范大学,外国语言学及应用语言学,2004,硕士.
[11]杨振龙.全三相△/ψ接线牵引变压器技术研究[D].西南交通大学,电气工程,2013,硕士.
[12]刘艳.非饱和土的广义有效应力原理及其本构模型研究[D].北京交通大学,2010.
[13]林冰.不安抗辩权与预期违约制度研究[D].苏州大学,法律,2003,硕士.
[14]赵亮.光伏水泵MPPT及弱光环境优化控制研究[D].哈尔滨工业大学,电气工程,2014,硕士.
[15]王庆海.液压挖掘机故障诊断系统的方案设计和推理方法研究[D].浙江大学,2002.
[16]梁爽.基于工程建设领域预防腐败的系统研究[D].天津大学,公共管理,2013,硕士.
[17]吕维先,陈红艺,帅贇.数据仓库在大型超市中的应用[J].微型机与应用,2004,12:40-41.
[18]何海涛.角色动画中布料的模拟与渲染研究[D].电子科技大学,计算机应用技术,2012,硕士.
[19]宣研.哈尔滨市建设工程质量政府监督存在的问题及其原因[D].黑龙江大学,公共管理,2012,硕士.
[20]李秩汇.《庄子》受古印度思想影响考论[D].广西民族大学,中国古代文学,2013,硕士.
[21]王晓芳.基于格式塔理论的关中小城镇传统街巷空间研究[D].长安大学,建筑与土木工程（专业学位）,2013,硕士.
[22]陈同馨.义务教育阶段县域内教师流动现状研究[D].西北师范大学,教育经济与管理,2013,硕士.
[23]张军君.ApoA-1、ApoC-Ⅲ、ApoE在小细胞肺癌中的研究及其临床意义[D].河北医科大学,肿瘤学（专业学位）,2014,硕士.
[24]张平.中承式钢管混凝土拱桥悬吊式桥道系破坏机理及对策研究[D].哈尔滨工业大学,桥梁与隧道工程,2013,硕士.
[25]陈宏微.具有字符、图形和图像显示功能的电视场强仪方案的研究[D].天津大学,通信与信息系统,2004,硕士.
[26]沈一.城市基础设施建设中政府融资模式研究[D].云南财经大学,公共管理,2013,硕士.
[27]张哲.孔庙祭祀的历史演变[D].上海戏剧学院,戏剧戏曲学,2013,硕士.
[28]汤怀锋.国内非散货船载运固体散装货物安全分析[D].大连海事大学,交通信息工程及控制,2013,硕士.
[29]张国威.环氧树脂结合剂金刚石磨块制备及性能研究[D].湖南大学,材料科学与工程,2011,硕士.
[30]常青.江苏省FDI流入的地区差异与影响因素分析[D].南京农业大学,金融学,2011,硕士.
[31]曹凌云.基于.NET平台的德州交通局办公自动系统的设计与实现[D].山东大学,软件工程（专业学位）,2012,硕士.
[32]刘德亮,程榕,郑燕萍.机械蒸汽再压缩蒸发结晶系统模拟分析[J].化工时刊,2014,02:5-8.
[33]李军.武钢第二炼钢厂转炉底吹控制系统[J].冶金自动化,1999,01:49-51.
[34]蒋剑.基于T-S模糊模型的非线性离散系统的H_∞滤波[D].南通大学,应用数学,2010,硕士.
[35]祝蕾.国际刑事法院被害人参诉研究[D].哈尔滨工业大学,国际法学,2014,硕士.
[36]黄芸.榨菜受根肿菌侵染后IAA和ZT的时空动态[D].西南大学,植物病理学,2014,硕士.
[37]胡大伟.输变电钢结构中钢材的防腐处理效果与二次修复效果研究[D].西安建筑科技大学,材料学,2013,硕士.
[38]张敏,陆向艳,周敏,潘林琳,农冬冬,王彬彬,陈晓江.数据挖掘在智能题库系统中的应用[J].广西大学学报(自然科学版),2005,S2:24-25.
[39]谈恒贵,李游华,王文杰.对CMAR算法的分析与改进[J].微型机与应用,2005,04:57-60.
[40]关艳阁.现代国家职业标准导向下的高职课程改革研究[D].广东技术师范学院,职业技术教育学,2014,硕士.
[41]黄福莉.纳米TiO_2和SnO_2/CdS薄膜的制备、表征及光电化学性能研究[D].湖南师范大学,物理化学,2013,硕士.
[42]王波.防城港电信公司营销渠道建设研究[D].电子科技大学,高级管理人员工商管理（EMBA）（专业学位）,2012,硕士.
[43]靳剑东.LTE-A系统中异构网下测量量增强关键技术的研究[D].中国地质大学（北京）,电子与通信工程,2013,硕士.
[44]本刊通讯员.2013国际新材料发展趋势高层论坛在成都召开[J].中国材料进展,2013,09:573-576.
[45]张敬普.基于Web Service的教学实训平台的研究与实现[D].西安电子科技大学,计算机技术,2010,硕士.
[46]刘瑾.期货交易所运营管理问题研究[D].东北财经大学,企业管理,2003,硕士.
[47]李洪滨.基于先进控制技术的常减压装置的设计和应用[D].天津大学,控制工程,2013,硕士.
[48]周泉.低温等离子体辅助制备石墨烯基复合材料及其电化学性能研究[D].大连理工大学,2014.
[49]付承晨.《美国发明法案》研究[D].复旦大学,法律,2012,硕士.
[50]郭新文.交互式电子学档支持深度学习研究[D].温州大学,课程与教学论,2012,硕士.