资源描述：
《动态逻辑_关于程序的模态逻辑new》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、90*动态逻辑:关于程序的模态逻辑郝一江(中国社会科学院哲学所北京100732)张晓君(中国社会科学院研究生院哲学系北京100732)[中图分类号]B81[文献标识码]A[文章编号]1002-8862(2009)11-0090-05动态逻辑(dynamiclogic,简称DL),又称关于程序的模态逻辑(modallogicofprograms),是进[1]行程序逻辑性质研究、程序正确性证明研究的有力的数学工具。动态逻辑是一种与自然语言的语义分析和人工智能都有密切联系的新思想,为现代逻辑理论的发展提供了新的题材和思路。首先,在逻辑系统方面,动态逻辑为逻辑研究的很多
2、方面提供了崭新的研究视角,它不但改革了经典逻辑的静态语义模型,而且打开了动态算子及其推理的广阔空间。其次,在语言科学方面,它的特点符合人类运用自然语言的认知过程,可以看成是对基于自然语言的思维过程的理论描述,它比经典逻辑更加适合作为理论语言学的逻辑基础与描述工具。最后,在人工智能方面,动态逻辑与计算机程序语言的关系非常密切,它的句法语言直接添加了表现程序概念的表达式,可以据此编制计算机处理自然语言的程序指令,[2]甚至能够直接提供便于计算机处理的算法,动态逻辑能够为计算机理解自然语言提供理论依据。动态逻辑是国外逻辑学界、数学界和计算机科学界研究的热点问题之一。目前,我国在这方面的研究成果可
3、谓凤毛麟角,偶见我国计算机科学界或逻辑学界对动态逻辑进行过零星的,极不系统的研究。究其原因,这与我国数学、计算机科学和逻辑学研究总体滞后以及进行动态逻辑研究需要广博的相关知识和深厚的数学功底有关。研究者要想在动态逻辑方面具备很深的造诣并取得较大的突破,就必须具备数理逻辑、无穷逻辑、算法逻辑、单值程序逻辑、递归论、形式语言、自动机、可计算性与复杂性、程序检验等方面的知识。因此,我国对动态逻辑的研究,尤其是不同学科领域的学者之间的合作研究还有待加强。本文是笔者对动态逻辑进行尝试性研究的阶段性成果,不足之处,敬请赐教。一动态逻辑的基本思想动态逻辑的前身是霍尔(Hoare)于1969年引进的霍尔逻
4、辑(Hoarelogic,简称HL)。霍尔逻辑是最早的一批形式验证系统,它可以用于程序设计的分析,比如,可以用于序列转换程序(sequentialtransformationalprograms)的分析。序列程序是在没有并发(concurrency)的单个处理机(processor)[3]上运行,而转换程序是指经过有限步的运算后,输出一个结果并能够结束的程序。动态逻辑是帕特(VaughanPratt)于1976年提出来的,提出这一理论的基本出发点是他认为把模[4]态逻辑与程序进行很好的融合是可能的。动态逻辑是对程序的输入/输出行为进行推理的形式系统,它是程序逻辑的总称。在关于程序的形式推理
5、的各种方法中,动态逻辑是以模态逻辑为基础,而且它与经典逻辑有着密切的联系。动态逻辑可以看做是一阶谓词逻辑、模态逻辑以及正则事件代数(thealgebra*本文由北京市哲学社会科学十一五规划项目(06BaZX022)资助。动态逻辑:关于程序的模态逻辑91[5]ofregularevents)这三个互相补充的经典成分组成。动态逻辑的基本思想就是把程序语言的每个命令与一个模态联结词[]进行结合,从而引进了[]与<>这两个模态结构,用于探讨一个程序在一个公式的真值上的执行结果。其公式[]的意思是在的每一次结束执行后,是真的,即在停机的任何时候,在满足的状态下也是
6、处于停机状态;其对偶公式<>的意思是存在[6]为真的的一个结束执行,即执行并在满足的状态下停机是可能的。动态逻辑与经典一阶逻辑有什么区别呢?在经典一阶逻辑中,语句的真值是不变的,也就是说,一个公式的真值是由其自由变元在某个结构上的赋值决定的。这一赋值与的真值被看做是不动的,不存在把它们与其他赋值或真值相联系的形式系统。而在动态逻辑中,具有显性语法结构的程序的主要作用是改变变元的赋值,从而公式的真值也相应地得到改变。在动态逻辑中,复合程序是由初始程序通过几个算子递归生成的。在动态逻辑的最简单的版本中,这些程序算子是指!非确定性选择(nondeterministicchoic
7、e)算子、序列合成(sequentialcomposition)算子、*迭代(iteration)算子以及测试(test)算子。这些算子对于计算定义在自然数上的所有的部分递归函数来说足够了。动态逻辑有两种语法范畴:公式与程序,公式用于讨论状态(state),程序用于对状态之间的转换进行分类。动态逻辑语法比部分正确性断定的霍尔逻辑更为灵活,也具有更强的表达力,因为在动态逻辑中,[7]公式的递归定义允许模态算子的
