姚从军,陈宝爱
(湘潭大学碧泉书院,湖南 湘潭 411105)
中国科学院的唐稚松院士是我国著名的逻辑学家和计算机科学家。①唐稚松院士科研团队从20世纪80年代初开始,历经3个五年计划的科研攻关,终于在1995年开发了世界上独创的大型软件工程工具系统XYZ。XYZ系统被称为系列化语言组,其对应的汉语拼音为Xiliehua Yuyan Zu,因此简称XYZ。这项创新性成果荣获1989年国家自然科学奖一等奖和1996年何梁何利科学技术进步奖,它是我国软件工程领域发展的一个里程碑,同时也是我国为世界软件工程领域所做的重要贡献之一。
唐院士提出了世界上第一个可执行时序逻辑语言XYZ/E,该语言在逻辑系统中引入状态转换的控制机制,是时序逻辑形式化理论与最新软件技术交叉研究的创新案例。XYZ系统由时序逻辑语言XYZ/E及一组基于该语言的CASE工具集组成。“XYZ系统是将时序逻辑和软件工程有机结合而成的整体,时序逻辑语言XYZ/E是XYZ系统的核心,它既是一个时序逻辑系统,又是一种程序语言。”[1]42
在时序逻辑语言XYZ/E和C语言的赋值语句那里,出现“一表达式一范畴多语义”的情况,这里显示出动态逻辑的思想;另一方面,计算机程序C语言的赋值语句直接就是量化动态逻辑的研究对象,可以对此进行更加精细的刻画;XYZ/E之后出现的动态逻辑主要关注程序语言的动态特征,然而XYZ/E的基本构件,即单元的表述既有动态的特征也兼具静态的性质,可以设想扩大标准动态逻辑的表达能力,全面刻画XYZ/E的兼容功能;XYZ/E的子语言XYZ/BE所描述的并发通讯进程语义的组合性问题是:踏步语句的静态组合和非踏步语句的动态组合,静态组合原则已有一般性的概括表述,尚需要给出动态组合原则的一般逻辑表述;XYZ/E是建立在时序逻辑基础上的程序语言,时序逻辑的语义是静态的,但XYZ/E却可表现可执行命令式编程语言的动态特征——状态转换的控制机制,况且XYZ/E依据的一阶时序逻辑还是一种扩展的多体的时序逻辑,可以设想更精准的方案,来确立XYZ/E的逻辑基础。
XYZ的基础和核心是基于时序逻辑的程序语言XYZ/E。计算机程序语言的任务是刻画机器状态转换的控制机制,而状态转换机制则通过赋值语句体现出来,XYZ/E用时序逻辑的语义刻画赋值语句的动态特征。
XYZ/E的赋值语句表述,如:求阶乘0!,1!,…,k!的和,即s=SUM(i=0,…,k)(i!)。[1]53XYZ/E的表述是:
古希腊辩证法思想家赫拉克利特的名言:
一个人不能两次踏进同一条河流
XYZ/E的赋值语句:
时序逻辑算子$O的作用使得左边的j和右边的j不能赋予同一个数值(否则将导致矛盾),但其类型(范畴)却是一样的,其类型都是e。被赋予的两个不同的数值就是两个j的不同语义所指(见下图红色符号串)。具体分析推演如下:
上例可见,可以创立受限的描述个例的CCG函项应用规则:
对XYZ/E中类似的赋值语句进行研究,可以看出动态视角的CCG研究的必要性。组合范畴语法CCG的自然语言研究,采纳结合语用语境的经验主义方法,遵循“一词多范畴多语义”和“多词一范畴多语义”的原则构建CCG处理自然语言的词库。CCG的研究角度也适合于计算机程序语言的研究。在时序逻辑语言XYZ/E和C语言的赋值语句那里,出现“一表达式一范畴多语义”的情况,这里显示出动态逻辑的思想。因此,可以把CCG分析方式应用于时序逻辑语言XYZ/E,尝试构建具有动态逻辑思想的CCG研究模式,提出基于个案个例的CCG函项组合的新规则,这是一种新的CCG研究方式,即动态CCG。
上例看到C语言的赋值语句:
CCG对自然语言的分析,参照语用语境的情况是:一词多范畴。按照CCG的方式对C语言的赋值语句进行分析,(在没有时序算子$O的条件下)参照不同语境,左边的i和右边的i不能赋予同一个数值,但其类型(范畴)却是一样的,其类型都是e。被赋予的两个不同的数值就是两个i的不同语义所指。
对程序语言赋值语句的分析结果是:一变项一类型(范畴),但一类型多语义,最终是:一变项多语义。变项的语义随语境而改变,这也体现出动态的逻辑思想,如量化动态逻辑QDL关于赋值等式的语义定义针对的就是这种情况:
这里“x”是被赋值变项,“t”是赋值词项,它可以是包含变项而经过函子运算而产生的项,例如“x+1”。这里赋值语句的动态特征通过赋值函项a到b的扩展体现出来,b对“x”的赋值可能不同于a。就上例而言,如a把个体2赋给“x+1”中的“x”,b给“x”赋的值就是个体3。
动态逻辑是上个世纪90年代才出现的逻辑新品种,直接受计算机程序语言动态特征的影响,结合当今上千种程序语言的多样特征,动态逻辑可以进一步拓展。
在唐院士构造的XYZ/E中:基本构件(单元)的一般表述兼顾动静,既体现了程序的动态语义,还显示了程序的静态语义。XYZ/E的基本构件,即单元的一般表述为:
XYZ/E的动态描述:从Ai到Ai+1机器的状态转换 变项的赋值更新
XYZ/E的静态描述: 从Bi到Bi+1静态的逻辑合取 没有变项的赋值更新
当单元中的nF2,m=0时,单元中时序算子*限制的诸条件元之间体现的是动态的程序语义。例证:求阶乘0!,1!,…,k!的和,即s=SUM(i=0,…,k)(i!)。用纯粹可执行语言的风格表述,即是:
就变项i而言,从A1到A2、A3和A6,被赋予的值不断更新变化;就变项j而言,从A1到A3、A4和A5,被赋予的值也不断更新变化。总之,A1---A6的合取表现的是动态的程序语义。
当n=1,mF1时,单元中的WHERE部分各合取支之间体现的是一种静态的逻辑语义。
沿用上述,其表述为:
WHERE后是单元的约束部分,由三个条件句的合取构成,合取支之间没有变项的赋值更新,因而是一种静态的合取。最后一个条件句是“阶乘和”的数学归纳定义,根据定义,可依次获得:1!=0!×1,2!=1!×2,3!=2! × 3,……。
当nF2,mF1时,单元中既有*限制部分中诸条件元之间体现的动态思想,也有WHERE部分各合取支之间体现的静态思想,即整个单元是动态和静态的融合。其价值有:
用混合的形式来表示中间程度的抽象性。表述为:
其动态合取和静态合取的说明同上。
动态谓词逻辑DPL对逻辑连接词尤其是对合取连接词的定义如下:[3]
由上可知,否定、析取和蕴涵连接词的定义都是静态的,a=a,不存在从赋值a到赋值a的更新。而合取连接词的定义却是动态的,a并非等同c,从赋值a由于赋值b的关联更新到赋值c,因为合取支φ中的变项赋值可能不同于合取支ψ中的变项赋值,犹如XYZ/E单元中从Ai到Ai+1的赋值更新。量化动态逻辑QDL中对合取连接词也有类似的动态处理。
XYZ/E之后出现的动态逻辑主要关注程序语言的动态特征,比如DPL和QDL等动态逻辑刻画的是计算机程序语言的动态机制,其合取连接词的语义定义是动态的,但XYZ/E的单元表述中既有动态的合取,在其受限部分那里还有静态的合取。DPL和QDL等动态逻辑对蕴涵连接词的定义是静态的,但XYZ/E中的条件元后件中可能出现时序算子,就是说这样的条件元的语义可能是动态的。因此,可以考虑扩大标准动态逻辑的表达能力或构建新的动态逻辑来表述XYZ/E的单元中关于合取和蕴涵的动静混合的语义,从而全面刻画XYZ/E的兼容功能。
XYZ/BE中处理并发通讯进程时:当可同步的进程P1和P2中的同步语句α1和α2有一个是踏步语句时,P1,P2的并发[P1||P2]中的是静态组合的产物;当可同步的进程P1和P2中的同步语句α1和α2都不是踏步语句时,P1,P2的并发[P1||P2]中的是动态组合的产物。[1]229-230踏步语句是一种等待指令,就是等待某个条件成立,它才会继续,不然就在原地等待。关于踏步语句和同步语句的定义参见唐稚松2002。[1]227-228
例证:用XYZ/BE表示出两进程:
P1中的红色条件元和P2中的红色条件元动态组合成[P1||P2]中蓝色条件元,P1中的蓝色条件元和P2中的蓝色条件元动态组合成[P1||P2]中蓝色条件元。P1中的其他条件元和P2中的其他条件元保持不变直接延续到[P1||P2]中去,这些组合是通常的静态组合。
静态组合的定义:设有复合表达式的句法运算F(α1,…, αn),复合表达式的语义G(α1′,…, αn′)意味由α1′,…, αn′定义的组合语义。
例证:MG(蒙太格语法)中的量化复合表达式F(α)=every α,这里对应的语义运算G(α′)=λP∀x[α′(x)→P(x)]
组合前的表达式α′仍然出现在组合后的表达式中,保持不变。
动态组合就不一样了。P1蓝色条件元和P2蓝色条件元中的动作部分的动态组合:
这里获得了[P1||P2]蓝色条件元的动作部分中的$O j=k,组合前的$Oc?(j)和c!(k)已不在组合后的表达式中出现,组合改变了原有表达式,这就是动态的组合。我们需要对这类个案个例的程序并发组合进行搜集,期望获得规律性的动态组合表述。
总之,XYZ/E的子语言XYZ/BE所描述的并发通讯进程语义的组合性问题是:踏步语句的静态组合和非踏步语句的动态组合,静态组合原则已有一般性的概括表述,怎样概括动态组合原则的一般表述?值得研究。
XYZ/E是建立在时序逻辑基础上的程序语言,时序逻辑的语义是静态的,而XYZ/E所关注的是计算机程序中状态转换的控制机制,它可表现可执行命令式编程语言的动态特征——状态转换的控制机制,这显示出动态的精神,可以设想更精准的方案,来确立XYZ/E的逻辑基础。
XYZ/E定义了10个时序算子,比通常时间逻辑定义的算子要多,多出来的算子必要性在哪里?可以尝试对XYZ/E依据的时序逻辑进行改造,使其语义直接显示动态的观念,据此构建的动态时序逻辑显得更加精致。况且XYZ/E依据的一阶时序逻辑还是一种扩展的多体的时序逻辑,从逻辑系统的精准性角度调整XYZ/E的时序逻辑,是有进一步的研究空间。
从逻辑理论出发,譬如采用组合范畴语法CCG的范畴逻辑分析方式,去剖析计算机程序语言的特性,分析XYZ/E表现出的状态转换的控制机制。具体而言,依据范畴逻辑原理上建立的CCG,把对自然语言的句法构造和语义组合进行处理的套路,搬到计算机程序语言的领域:确定原子表达式和初始算子符号的范畴类型,确定对应的语义所指;再依据通常范畴类型运算的规则对计算机程序语言的复合表达式乃至语句进行推演,在推演过程中结合计算机程序语言的实际特征,尤其要捕捉到XYZ/E非常独特的表述方式,透过时序算子的作用感受到动态的思想,这样反过来对CCG已有的推演规则进行修正或调整。进而探讨新的CCG理论。
对计算机程序语言XYZ/E进行详细和持续的观察和学习,进而上升到动态逻辑的理论高度。XYZ/E是上个世纪末由中国科学家唐稚松院士独创的计算机程序语言,唐院士非常关注该语言中的动态语义和静态语义,为了增强XYZ/E的表达力,接近可执行命令式程序语言的表述风格,并被广大计算机编程人员所接受,唐院士提出了XYZ/E的基本构件——单元的表述方式,单元能够兼容动态的程序语义和静态的程序语义。通常逻辑的研究范式往往分而治之,根据XYZ/E的实际情况,在逻辑领域对动态语义和静态语义进行融合表述,构建新的解释力更强大的动态静态交融的逻辑工具,这是基于XYZ/E这样的程序语言的实际情况实际特征进行的研究。
“大数据”的精神要求我们在处理问题时尽最大可能搜集相关数据例证。可以采用对有限范围的个案个例进行考证的方法,如通讯进程的并发程序具有很多复杂多样的例证,涉及的语义组合问题是计算机软件领域的著名难题,涉及许许多多计算机程序的技术细节。企图从理论层面系统解决这样的问题谈何容易!因此可以降低目标,从有限的个例出发,逐步推进求精,实现中等程度的抽象,对于众多难题解决一点是一点。
注释:
①著名学者唐稚松大学与研究生就读于清华大学哲学系,师从我国著名逻辑学家金岳霖先生学习逻辑学,先后进入中国科学院计算技术研究所和软件所工作,从事逻辑学与计算机科学的交叉研究,1991年当选中国科学院院士。