（计算机软件与理论专业论文）逻辑程序设计语言godel的形式化过程性语义.pdf

摘要 摘要 g 6 d e l 语言是继p r o l o g 语言之后出现的逻辑程序设计语言，它建立在多态 多类的一阶逻辑基础之上，摒弃了p r o l o g 语言中的非逻辑成分，集成了许多语 言的有效成分和优点，引入了类型系统，这使得它成为一种高效的说明性逻辑程 序设计语言。然而，时至今日，g 6 d e l 语言编译系统的开发研究仍然进展缓慢， 主要原因是多态多类的类型系统、模块化结构、延迟计算、剪枝操作等多种新语 言成分和机制的引入，使逻辑程序设计语言g 6 d e l 的复杂程度大大提高，而面向 过程程序设计语言的编译方法和技术完全不同于具有递归性、说明性特点的逻辑 程序设计语言，先前关于p r o l o g 语言的编译方法和技术不能简单移植和照搬， 而理论基础研究的滞后直接导致系统研究和开发进展缓慢，迄今尚无新的进展和 系统开发成果报道。 为了促进g s d e l 语言的推广以及深入研究，本人所在的课题组基于类型一阶 逻辑h o r n 子集提出了g 6 d e l 语言一整套理论基础，本文在g 6 d e l 语言的语法和 形式化说明性语义基础上，着眼于编译系统的设计与实现，为g 6 d e l 语言建立了 严格的形式化过程性语义。 本文首先介绍了g 6 d e l 语言的语法基础，接着详细阐述了基于类型一阶逻辑 h o r n 子集的过程性语义，引入了较为完整的基类型，构造类型，结构类型间的 偏序关系，讨论了类型相容性关系，类型推断与类型约束算法，以及基于类型约 束的合一算法和s l d 反驳消解法。然后，全面介绍了g 6 d e l 语言程序设计的各 个模块。最后，在原g 6 d e l 语言系统模型的基础上完善了该系统的设计思想。相 信在相关理论的支持和指导下，随着后续工作的逐步开展，以及g 6 d e l 语言编译 系统实现技术的逐步成熟，g 6 d e l 语言将会受到更多的关注。 关键词：g s d e l 语言；过程性语义；类型系统 a b s t r a c t a b s t r a c t g 6 d e li sad e c l a r a t i v el o g i cp r o g r a m m i n gl a n g u a g es u c c e e d e dt op r o l o g i ti s b a s e do nm a n y - s o r t e df i r s to r d e rl o g i cw i t hp a r a m e t r i cp o l y m o r p h i s m ，d i s c a r d st h e f e a t u r e so fp r o l o gw h i c ha r en o n - l o g i c a l ，i n t r o d u c e st y p es y s t e m ，i n t e g r a t e st h em e r i t o fm a n yl a n g u a g e s ，a d d ss o m en e wl a n g u a g ec o m p o n e n t sw h i c hl e ti tb ee f f i c i e n t d e c l a r a t i v ep r o g r a m m i n gl a n g u a g e h o w e v e r , t h ec o m p l e x i t yo fg 6 d e li s g r e a t l y i n c r e a s e d 埘t l lt h ei n t r o d u c t i o no ft y p es y s t e m ，m o d u l a rs t r u c t u r e ，d e l a yc a l c u l a t i o n ， p r u n i n go p e r a t i o n b e c a u s et h em e t h o d sa n dt e c h n i q u e si nc o m p i l e ro ft h el o g i c p r o g r a m m i n gl a n g u a g ew i t hr e c u r s i v ea n dd e s c r i p t i v ec h a r a c t e r i s t i c sa r ec o m p l e t e l y d i f f e r e n tf r o mt h a tu s e di nt h ec o m p i l e ro fp r o c e s s - o r i e n t e dp r o g r a m m i n gl a n g u a g e ， t h em e t h o d sa n d t e c h n i q u e so ft h el a t t e rc a l ln o tt r a n s p l a n t a t i o n s i n c et h eb a s i ct h e o r y r e s e a r c hl a g sb e h i n d ，s ot h er e s e a r c ha n dd e v e l o p m e n to ft h ec o m p i l e rs y s t e mo f g 6 d e li ss t i l li ns l o wp r o g r e s s i no r d e rt of a c i l i t a t et h es p r e a da n di n - d e p t hr e s e a r c ho fg 6 d e l ，o u rp r o j e c tg r o u p b r o u g h tf o r w a r das e to ft h e o r e t i c a lf o u n d a t i o nb a s e do nh o r ns u b s e to ft y p e d f i r s t o r d e rl o g i c t h i sp a p e re m p h a s i z e ds t r i c tf o r m a l i z e dp r o c e d u r a ls e m a n t i co f g 6 d e lb a s e do ng r a m m a ra n df o r m a l i z e dd e c l a r a t i v es e m a n t i co ft h el a n g u a g ew h i c h c a n l a yar e l i a b l et h e o r e t i c a lb a s i sf o rt h er e a l i z a t i o no ft b ec o m p i l e rs y s t e mo fg 6 d e l t h i sp a p e ri n t r o d u c e dg r a m m a ro fg 6 d e li nt h ef i r s t p a r t ，a n dd e s c r i b e d f o r m a l i z e dp r o c e d u r a ls e m a n t i cb a s e do nt y p e df i r s t - o r d e rl o g i c d e t a i l e d l yi nt h e s e c o n dp a r t ，w h i c hd i s c u s s e dg r o u n dt y p e ，c o n s t r u c t i v e t y p ea n ds t r u c t r a lt y p e ， b r o u g h ti nt y p ec o m p a t i b i l i t y , t y p ed e d u c t i v ea l g o r i t h ma n dt y p ec o n s t r a i n ta l g o t i t h m ， u n i f i c a t i o na l g o r i t h mb a s e do nt h et h e o r ya n ds l dr e s o l u t i o nr e f u t a t i o n t h e n ，i nt h e f o l l o w i n gp a r t ，e a c hm o d u l eo fg 6 d e lp r o g r a m m i n gd e s i g nw e r ei n t r o d u c e d f i n a l l y , o nt h eb a s i so fo r i g i n a lg o d e ls y s t e mm o d e l ，w ep e r f e c t e dt h ed e s i g nm e t h o d o l o g yo f t h es y s t e mb a s e do nt y p es y s t e m u n d e rt h es u p p o r ta n dd i r e c t i o no fr e l a t i v et h e o r i e s ， w i t hm o r ef o l l o w i n gt a s k sb e i n gc a r r i e do u ta n dt h ep r o g r e s s i v e l ym a t u r a t i o no ft h e g o d e lc o m p i l e rs y s t e mr e a l i z i n gt e c h n o l o g y , g 6 d e l l a n g u a g ew i l l c a t c hm o r e a t t e n t i o n k e yw o r d ：p r o g r a m m i n gl a n g u a g eg o d e l ；p r o c e d u a ls e m a n t i c ；t y p es y s t e m 厦门大学学位论文原创性声明 本人呈交的学位论文是本人在导师指导下，独立完成的研究成 果。本人在论文写作中参考其他个人或集体已经发表的研究成果，均 在文中以适当方式明确标明，并符合法律规范和厦门大学研究生学 术活动规范( 试行) 。 另外，该学位论文为() 课题( 组) 的研究成果，获得() 课题( 组) 经费或实验室的 资助，在() 实验室完成。( 请在以上括号内填写课 题或课题组负责人或实验室名称，未有此项声明内容的，可以不作特 别声明。) 声明人( 签名) ：品垂、 哆年z 月s 日 厦门大学学位论文著作权使用声明 本人同意厦门大学根据中华人民共和国学位条例暂行实施办 法等规定保留和使用此学位论文，并向主管部门或其指定机构送交 学位论文( 包括纸质版和电子版) ，允许学位论文进入厦门大学图书 馆及其数据库被查阅、借阅。本人同意厦门大学将学位论文加入全国 博士、硕士学位论文共建单位数据库进行检索，将学位论文的标题和 摘要汇编出版，采用影印、缩印或者其它方式合理复制学位论文。 本学位论文属于： () 1 经厦门大学保密委员会审查核定的保密学位论文， 于年月日解密，解密后适用上述授权。 ， ( ) 2 不保密，适用上述授权。 ( 请在以上相应括号内打“”或填上相应内容。保密学位论文 应是已经厦门大学保密委员会审定过的学位论文，未经厦门大学保密 委员会审定的学位论文均为公开学位论文。此声明栏不填写的，默认 为公开学位论文，均适用上述授权。) 声明人( 签名) ：品屯 哆年占月5 日 第一章绪论 第一章绪论 g 6 d e l 语言是继p r o l o g 之后出现的一个新型说明性通用逻辑程序设计语言，由 以英国b r i s t o l 大学j w l l o y d 和l e e d s 大学的p m h i l l 为代表的研究小组在九十 年代中期设计开发。g 6 d e l 语言除了借鉴了p r o l o g 和程序设计领域的最新成果，还 引入了类型系统、延迟计算和剪枝操作等诸多新的语言成分，同时将语言的理论 基础扩展到多态多类的一阶逻辑，本文重点研究讨论了在带类型一阶逻辑基础上 g 6 d e l 语言的形式化过程性语义，以及在该语义支撑下，基于类型系统的推理机的 实现原理以及设计思想。 1 1g i i d e l 语言简介 g 6 d e l 语言是一种新型通用逻辑程序设计语言，融入了诸多创新设计思想和新 语言成分。首先，它充分吸收了逻辑程序设计研究领域的最新成果，借鉴、继承 了p r o l o g 语言的诸多要素和成分，并从p r o l o g 语言的众多变型如i c - p r o l o g 、 n u p r o l o g 等以及m l 语言、m o d u l a - 2 语言引入新的语言设计思想和成分，如语言 的推导规则和模块化的设计理念等。其次，在表达能力上，g 6 d e l 语言不再局限于 基于一阶逻辑的h o m 子集，而是引入多态多类的类型系统，将语言建立在多态多 类的一阶逻辑基础之上，使语言具备了很强的描述能力，且易于进行程序开发和 实现。由于添加了类型，g 6 d e l 语言抛弃了传统人工智能语言基于字符匹配的盲目 搜索算法，大大提高了执行效率。第三，在控制策略上，g 6 d e l 语言引入了延迟和 剪枝机制。延迟和剪枝机制是对s l d 反驳消解法的补充，是在满足s l d 反驳消解 法正确性基础上提高程序执行效率的一种机制。剪枝操作建立在并发语言的 c o m m i t 机制之上，可用来对搜索树进行剪枝从而影响搜索的完全性，进而提高问 题求解效率。与此同时，剪枝操作也在一定程度上破坏了g 6 d e l 语言的说明性语 义，并可能剪除产生正确结果的分支，使得程序的输出结果不包括所有正确解。 延迟机制的引入解决了这一问题，并改变了传统人工智能语言最左文字优先的计 算规则，使g 6 d e l 语言具有更为灵活的计算规则，提高了语言的执行效率和正确 性，以及计算的可表达性。此外，g 6 d e l 语言的设计融入了一些程序设计方法和技 逻辑程序设计语言g 6 d e l 的形式化过程性语义 术，例如，通过支持抽象数据类型程序设计实现面向对象程序设计思想，进一步 发展并支持模块化程序设计，使其能够方便地进行大规模程序开发；元程序设计 思想也在g 6 d e l 语言中得到进一步发展，丰富了人工智能程序的说明性语义；同 时，动态元级程序设计使得源程序具备了“智能”的大脑。在该技术的支持下， 程序可以在执行的过程中根据需要增加和删除特定的语句，动态地控制执行流程， 从而具有更强的适应性和灵活性。 1 2g 6 d e l 语言的理论基础 传统的逻辑程序设计是基于一阶逻辑的h o m 子集理论。1 9 7 2 年，p r o l o g 语言 诞生，h o r n 子句逻辑语言在计算机科学中被作为一种描述或说明性的程序设计语 言用于问题求解【1 1 。h o r n 子句逻辑由于其在表达上的简单、准确特点而被广泛应 用于人工智能的研究。 h o r n 子句是下列三种子句之一： a 一称为无条件子句或单位子句； a bl ，b 2 ，b 。称为条件子句，a 称为头部或结论，bl ，b 2 ， b 。称为体或条件，每一个b i ( i s ) 称为一个子目标或一个条件； 一b l ，b 2 ，b 。称为目标子句，每一个b i ( i s ) 称为一个子目标。 由于h o m 子句的头部是单一的，因此利用h o m 子句做推理可以得到确定的 推理结论。不同的h o m 子句可以有完全相同的一组条件。因此，同样一组条件利 用不同的h o m 子句可以推理得到多个不同的结论。 逻辑程序设计思想在应用上的最早实现应该是p r o l o g 语言的出现。p r o l o g 语 言可以说是最传统的逻辑程序设计语言，它作为一种设计自然语言处理程序的编 程语言而发展起来并很快被公认。作为一个典型的逻辑程序设计语言，p r o l o g 具有 语法简单、清晰、可读性好等优点，有较强的可表达性。p r o l o g 语言比较适合于那 些涉及到模式识别、回溯式搜索、或者不完全信息的应用。如今，p r o l o g 语言仍被 用于描述算法、执行数据库查询、开发编译系统、构造专家系统等。 但是，p r o l o g 语言也存在不足之处，主要是其缺乏类型、执行效率不高、控制 机制不完善等，不足于支撑大型软件系统的开发。可以说，缺乏类型是p r o l o g 语 言最大的缺陷。因为编程语言中的类型可以结构化程序所操纵的数据并保证其正 2 第一章绪论 确的被使用。虽然p r o l o g 中可以定义记录等各种不同的类型，而且p r o l o g 也提供 了列表的表示法，通过算术标识符和算术比较关系，又提供了对数字类型的有限 支持。然而，p r o l o g 不支持检测数据类型，它不检查是否按预期的执行查询程序。 由于没有类型检查，类型错误很容易发生却很难被找出。 为了满足软件研究和应用的需要，在近二三十年以来人们对p r o l o g 语言做了 许多扩充和改进，出现了并行逻辑程序设计语言、对象式逻辑程序设计语言和模 糊逻辑程序设计语言等新的逻辑程序设计语言。这些新的语言都在不同程度上增 强了传统逻辑程序设计的内在表达能力并提高了实现效率，但是它们都没有彻底 解决p r o l o g 语言中缺乏类型的问题，自带类型的逻辑程序设计语言g 6 d e l 的出现 后，由于该语言建立在多态多类的一阶逻辑基础之上，并引入多态多类的类型系 统，因而较好的解决这个问题。 1 3g i j d e l 语言理论研究及系统实现现状 逻辑程序设计语言的重要性早已为人们所熟知，但g 6 d e l 语言作为新型逻辑 程序设计语言，自推出之后，其编译系统始终没有真正意义上的实现，b r i s t o l 大 学研究小组已经开发的单机上的编译实验程序b r i s t o lg o d e l 也仅实现了一个 很小的子集。究其原因，一是语言复杂，二是缺乏严格的理论基础，即缺乏用于 支撑该语言的类型阶逻辑。正如p r o l o g 语言的正确性和可靠性是建立在一阶谓 词逻辑的h o r n 子集的基础之上，为了能够完全实现g 6 d e l 语言，首先需要为其建 立严格的数学基础，包括其语法和语义理论，从而为其实现奠定可靠的理论基础。 厦门大学逻辑程序设计研究小组基于一阶谓词逻辑和类型系统给出了g 6 d e l 语言较为完善的理论基础，详细的阐述了语言的形式化的说明性及过程性语义。 基于该理论，对小组早期开发的g 6 d e l 语言编译系统雏形进行评测以及完善其设 计思想，预计不久的将来，在该理论指导下，后继系统的正确性和可靠性将有大 幅提高。 1 4 本文的主要工作及篇章结构 基于g 6 d e l 语言的语法规则，围绕着说明性语义，本文重点阐述了g 6 d e l 语言 的过程性语义，并提出基于类型系统的推理机改进设想和方案。 逻辑程序设计语言g o d e l 的形式化过程性语义 本文一共分为六章。第一章，对g 6 d e l 语言及其理论基础做了简要介绍，并阐 述了理论研究和系统实现现状；第二章，详细介绍了类型一阶语言相关概念以及 g 6 d e l 语言的语法；第三章是本文的重点，讨论了基于g 6 d e l 语言说明性语义上的 形式化过程性语义，给出了类型推断和类型约束算法；第四章，阐述了g o d e l 语 言的控制机制，详细介绍了推导规则，剪枝和延迟操作。第五章，介绍了g 6 d e l 语言编译系统的实现原理与设计思想。第六章对本文的主要工作进行了总结和讨 论，并提出下一步工作需要解决的问题和设想。 4 第二章g o d e l 语言的语法 第二章g i j d e l 语言的语法 自从p r o l o g 语言诞生以后，逻辑程序设计就一直成为新型程序设计语言研究 的方向之一。1 9 7 0 年代后期和1 9 8 0 年代初，在人们为p r o l o g 语言建立了h o r n 子 句理论的基础之后，如何对p r o l o g 进行扩展，将无类型的逻辑程序设计语言改造 成带类型的逻辑程序设计语言，同时建立新型逻辑程序设计语言的理论基础，扩 展逻辑程序设计的应用范围，就成为一个重要的研究课题。1 9 9 0 年中期，j w f l o y d 等人在系统总结前人工作的基础上，推出了新型逻辑程序设计语言g 6 d e l 。g 6 d e l 语言借鉴了p r o l o g 语言的诸多元素，并从p r o l o g 语言的众多变形如i c p r o l o g 、 n u p r o l o g 等以及m l 语言、m o d u l a - 2 语言等引入语法成分，试图改进p r o l o g 语 言中存在的不足并解决其中有争议的语义问题口1 。作为一种逻辑程序设计语言，研 究与开发g 6 d e l ，首先需要为其建立严格的数学基础，包括其语法和语义理论基础。 从p r o l o g 语言和g 6 d e l 语言的关系看，g 6 d e l 的数学基础应该是多态多类的一阶逻 辑，而且，g f d e l 语言的语法与多态多类一阶逻辑的类型合式公式之间有着密切的 联系，g 6 d e l 语言的语义应该与多态多类一阶逻辑的模型之间有着密切的联系，于 是，发展带类型的一阶逻辑理论成为一种选择。 从另一个角度考察问题j 也可以从中发现渊源。一阶逻辑建立的时候，最初 并未考虑将其扩展到多态多类的一阶逻辑。后来，由于计算理论的发展和形式语 义学研究的需要，人们选择了带类型的九演算来建立语义学理论，由此形成了类 型理论。而实际上，从计算模型的角度看问题，一阶逻辑与n 演算在计算能力上 是等价的，于是，可以猜测，带类型的一阶逻辑与带类型的九演算在计算能力上 也应该是等价的。不过，由于两类计算模型在形式上不同，各自应该有其适用的 范围。这样，从计算模型的角度，也有必要发展带类型的一阶逻辑理论阻1 。 2 1 类型符号 为了将来更好地定义g 6 d e l 语言的语法和建立带类型的一阶逻辑的需要，我 们先对带类型的一阶逻辑( 以下简称类型一阶语言) 中出现的一些符号作如下约 b 匕： ( 1 ) 基类型和类型符 逻辑程序设计语言g 6 d e l 的形式化过程性语义 由现实世界中的某些( 有穷或无穷) 个体组成的集合称为类型。特别，在g 6 d e l 语言中，用i n t e g e r ，r e a l ，s t r i n g ，b o o l e a n 表示基类型，也称为类型常元，其含义 与传统的高级程序设计语言中的基类型一致。基类型是事先约定，无须定义就可 直接使用的类型或类型符号。本文讨论的带类型的逻辑系统限定在类型一阶语言 范围内，故基类型是简单个体组成的集合。在不需要明确具体的类型时，我们也 常用斜体的乃仃( 可以带下标) 来表示类型常元或类型。 在g 6 d e l 语言中，可以通过构造子来定义构造类型。构造子可在程序中定义 和使用，用户可以根据自己的需要，自定义各种类型。如果c s t 是一个n 元构造子， n ，是类型，那么c s t “( 研，葡) 是一个构造类型。例如，l i s t 是一个1 元 构造子，它可以用来构造表类型，如l i s t ( i n t e g e r ) 是一个构造类型，用来表示整 数列表。因此，在g 6 d e l 语言中，基类型属于简单类型，构造类型属于复杂类型， 还有一种类型称为结构类型。结构类型是形如f i x x 一f 的类型，它表示把类 型r i ，规定的一组带类型的对象映射到类型f 规定的类型之对象的一种抽象 的结构类型。结构类型通常用来描述n 元关系或者函数的类型，具有提示n 元关 系和函数中参数的类型和映像结果之对象的类型的作用，具有类似于属性文法中 语义表达式的作用。 我们规定： 构造类型c 。“( n ，) 和c 2 n ( 研，) 等同或相同，记为 c 。“( q ，动= cn ( 研，) 若n = m ，c 和c 。是相同的n 元构造子且霸= 研，1 i n 。 结构类型f i x 一r 和c r l x xc l r m 一仃等同或相同，记为 z l x + f2 们o m 仃 若n = m ，霸= o i 且r = 盯。 在不需要特别区分时，简单类型、复杂类型和结构类型统称为类型。 类型符是用来表示类型的抽象的形式符号，是语法层面的概念。类型符在解 释或赋值下只能对应具体的类型。通常，我们用正体希腊字母百，6 ( 可以带下标) 来表示类型符。类型符在语义解释下只能对应为基类型、或构造类型、或结构类 型。 例我们以下面的g 6 d e l 程序为例对相关的类型作分析。 c o n s t r u c t o rl is t 1 6 第二章g o d e l 语言的语法 c o n s t a n t n i l ：l i s t ( i n t e g e r ) ；说明常量n i l 是一个空表 f u n c t i o n c o n s ：i n t e g e r * l is t ( i n t e g e r ) 一l is t ( i n t e g e r ) ； p r e d i c a t e a p p e n d ：l i s t ( i n t e g e r ) * l i s t ( i n t e g e r ) * l i s t ( i n t e g e r ) 一b o o l e a n a p p e n d ( n i l ，x ，x ) a p p e n d ( c o n s ( u ，x ) ，y ，c o n s ( u ，z ) ) 一a p p e n d ( x ，y ，z ) 在程序中定义了构造子l i s t ，所以l i s t ( i n t e g e r ) 是一个构造类型，用来表示整 数列表。连接函数c o n s 的类型声明为：i n t e g e r * l i s t ( i n t e g e r ) 一l i s t ( i n t e g e r ) ，这 是一个结构类型，它表示函数c o n s 有二个参量，它们的类型分别是基类型i n t e g e r 和构造类型l i s t ( i n t e g e r ) ，c o n s 函数值的类型也是构造类型l i s t ( i n t e g e r ) ；因此， 有c o n s ( 1 ， 2 ，3 】) = 1 , 2 ，3 1 。谓词a p p e n d 类型声明为： l i s t ( i n t e g e r ) 奉l i s t ( i n t e g e r ) 幸l i s t ( i n t e g e r ) 一b o o l e a n 这也是一个结构类型，它表示谓词a p p e n d 有三个参量，它们的类型都是构造类型 l i s t ( i n t e g e r ) 。可以看出，基类型和构造类型是结构类型的组成元素，结构类型主 要用来提示n 元关系和函数中参数的类型和映像结果之对象的类型。 ( 2 ) 类型集与类型符集 类型集是由类型构成的集合，类型符集是由类型符构成的集合。构成构造类 型( 项) 的每个构造子有一个非负整数表示其参数的个数，其中，o 元构造子的构 造类型就是基类型。 由所有基类型组成的集合称为语言的基本类型集。从基本类型集出发，联合 通过构造子定义的所有类型构成的集合称为( 语言的) 扩展类型集合。 g s d e l 语言中的基类型有：i n t e g e r ，r e a l ，s t r i n g ，b o o l e a n ，分别称为整型、 实型、字符串型和布尔型。1 元构造子有l i s t ，它用来构造表类型。类型构造子可 在程序中定义和使用。用户可以根据自己的需要，自定义各种类型。 2 2 类型一阶语言 定义2 1 由下面各种符号组成的集合称为类型一阶语言的字母表： ( 1 ) 类型符：t ，o ( 可以带下标) 为表示类型的抽象的形式符号。 ( 2 ) 个体符：二元组d = 表示个体符，用于表达具有某种 类型的个体的形式符号。个体词是用来表示个体的形式符号。通常，个体词用a ， 7 逻辑程序设计语言g 0 d e l 的形式化过程性语义 b ，c ( 可以带下标) 表示，用d ( 可以带下标) 来表示个体符。用个体符形式上表 达个体时，每个个体符都须带有一个类型符，说明个体词所要表达的个体均有其 类型符规定的某种类型。于是，d = 表示具有百类型的个体的形式符号。 ( 3 ) 约束变元符：二元组w = 表示约束变元符，用于 表达具有某种类型的约束变元的形式符号。通常，约束变元用x ，y ，z ( 可以带下 标) 表示。用约束变元符形式上表达约束变元时，每个约束变元符都须带有一个 类型符，说明约束变元所要表达的变元有其类型符规定的某种类型。于是，w = x ， p 表示具有t 类型的约束变元的形式符号。 当w 为无类型的约束变元符时，w 可以用w = 表示。通常，对于确切 的无类型的自由变元符，我们用w = 或者 ( 可以带下标) 表示。 ( 4 ) 函数符：e = 表示函数符，用于表达具有某种类型的 函数的形式符号。通常，函数词用正体英文字母f ，g ，h ( 可以带下标) 表示，n 元函数词可以通过在函数词的右上角添加上标n 来表示。函数符中的函数词为n 元函数词时，这个函数符也称为i 1 元函数符。i 1 元函数符也可以在函数符的右上角 添加上标n 来表示。用函数符形式上表达函数时，每个函数符都须带有一个类型 符，说明函数词所要表达的函数有其类型符规定的某种类型。带类型的n 元函数 也称为类型i 1 元函数或简称类型函数。于是，n 元函数符e “= 表示具有类型定义为t l h t 的n 元函数的形式符号。 ( 5 ) 谓词符：r = 表示谓词符，用于表达具有布尔值( b o o l e a n ) 类型的n 元谓词的形式符号。n 元谓词是用来表达n 元关系的形式符号。通常，谓 词用f ，g ，h ( 可以带下标) 表示，n 元谓词可以通过在谓词的右上角添加上标n 来表示。谓词符中的谓词为n 元谓词时，这个谓词符也称为n 元谓词符。n 元谓词 符也可以通过在谓词符的右上角添加上标n 来表示。用谓词符形式上表达n 元关 系时，每个谓词符都须带有一个类型符，而且这个类型符必须将来在解释下与基 类型b o o l e a n 保持一致，说明谓词所要表达的n 元关系有其类型符规定的与基类型 b o o l e a n 一致的类型。带类型的n 元关系也称为类型n 元关系或简称类型关系。 于是，n 元谓词符r “= 表示具有类型符定义为百l t n t 的n 元关系的形式符号。显然，1 1 元谓词符r “= 中的类型符 t 必须是与基类型b o o l e a n 保持一致的类型符。 8 第二章g o d e l 语言的语法 虽然我们尚未用形式化的方式引入解释这一概念，但非形式化的说明不会影 响读者对解释大致含义的理解。在数理逻辑中，所谓解释就是在一个事先指定的 论域范围内，将语法层面上逻辑公式中的各种形式符号对应到论域上的实在对象， 或表达论域上实在对象选择方法的数学表示形式。 所谓两个类型符t 和。在解释下保持一致，是指它们在解释下于下列情况之一 保持一致： 如果t 和。都是简单类型符，那么，将来它们在解释下对应于相同的类型； 如果t 是简单类型符，o 是具有f l x i n 一钳i 形式的结构类型符，那么， t 和t n + l 在解释下对应于相同的类型； 如果c 是具有1 7 1 x1 ；n t n + l 形式的结构类型符，o 是简单类型符，那么， 百n + l 和a 在解释下对应于相同的类型； 如果，c 是具有t l xt n 一钸l 形式的结构类型符，o 是具有o l o n o n + l 形式的结构类型符，那么，“l 和a n + l 在解释下对应于相同的类型。 我们知道，0 元谓词就是命题词，故0 元谓词符是具有b o o l e a n 类型的命题符， 也就是命题词。当我们用p ，q ，r ( 可以带下标) 表示命题词时，可以用o = ，或 ，或 ( 可以带下标) 表达命题符。 如今，经典逻辑中命题词的表示省略了类型符，其值在解释下被约定为真( t ) 或假( f ) 。 ( 6 ) 逻辑连接符或逻辑连接词：1 ( 否定) ， ( 合取) ，v ( 析取) ，一( 蕴含) ， 付( 等值) 逻辑连接符一共五个，扩展一个，实际上是带类型的形式符号，即 1 ，p ( 否 定符) ， ( 合取符) ， ( 析取符) ， ( 蕴含符) ， ( 等值符) 和 ( 左蕴含符) ，其中，1 、 、v 、一、付、 一分别为否定词、合取词、析取词、蕴含词、等值词、左蕴含词。由于逻辑连接符 中的类型符t 在解释下一定是b o o l e a n 类型，而事实上，逻辑连接符借助逻辑连 接词的概念其类型是固定不变的，在使用中不会引起混淆，故逻辑连接符和逻辑 连接词实际上没有区别。这些逻辑连接符的涵义与阶逻辑和p r o l o g 语言中相同 的逻辑连接词的涵义一致。 ( 7 ) 量符或量词：全称量符v w 和存在量符3 w 。其中，v 和了分别称为全称量 符符号和存在量符符号，w = x ，p 为约束变元符，它们的含义与一阶逻辑中量 9 逻辑程序设计语言g 6 d e l 的形式化过程性语义 词的含义基本一致，不同之处在于对论域中个体的约束具有类型的特征，即当w = x ，p 时，v w 或v x ，p 表示论域中全体具有类型符t 规定的类型的个体， 3 w 或3 x ，p 表示论域中存在具有类型符下规定的类型的个体。 我们还进一步约定，用大写英文字母( 可以加下标) q 表示量符( 词) 符号v 或j 。当量符中的约束变元符为无类型的q w = 或q 时，量符的 含义类似于经典逻辑中的量词，但实际作用有所不同。因为，当量符参与运算时， 有时候其约束变元符的类型处于“待定 状态，由此为未来表示多态多类提供了 方便。 在实际应用中，量符中的变元可能是带有类型的约束变元符，也可以是不带 类型的约束变元符。当量符中的变元是带类型的约束变元符时，其辖域中被约束 的变元符和变元将受到量符类型的约束。 ( 8 ) 分隔符：包括括号，逗号等。其中，括号必须满足配对使用的原则。 ( 9 ) 类型合式公式、类型命题形式、类型公式：我们沿用一阶逻辑中符号的 使用办法，通常用x ，y ，z ( 可以加下标) 表示任意的公式，用a ，b ，c ( 可以加 下标) 表示合式公式( 注意，此处的合式公式是在类型合式公式定义中出现的公 式，但没有包括该公式的类型) ，用r ，a ( 可以加下标) 表示类型合式公式的有 穷序列或汇集( 上下文清楚时，也可以用于表示类型合式公式的集合) 。我们使用 英文花体字母彳，留，留以二元组的形式如彳= 等来表示任意的类型公式， 即具有某种类型的任意的公式。合式公式是用来表示命题的形式符号，因此，类 型合式公式是用来表示具有b o o l e a n 类型的命题的抽象的形式符号。类型命题形 式是用来表示具有b o o l e a n 类型的命题函数的抽象的形式符号。 我们已经给出了个体符、约束变元符、函数符、谓词符、类型项和类型合式 公式、类型命题形式等，它们都是用带有类型符号的二元组的形式表示的，其中， 第一个分量称为公式部分，第二个分量成为类型部分。显然，公式部分的结构可 以参考一阶逻辑中对应概念的公式的结构，但含义有所不同。 为了方便今后的表达，我们引入三个算子f o r m u l a 、t y p e 和s t y p e 。对于具 有二元组结构的个体符、约束变元符、函数符、谓词符、类型项和类型合式公式 等，f o r m u l a 、t y p e 分别计算其公式部分和类型部分，而s t y p e 算子计算的结果是 1 0 第二章g o d e l 语言的语法 一个包含了在其中出现的全部类型的集合。例如，设彳= a ，1 ；1 t n 一仑，则 f o r m u l a ) = a ，t y p e ) = t i t n t ，s t y p e ) = 1 ；1 ，1 ；nt 。对其他二元 组结构的计算也是相同的。 定义2 2 类型项归纳定义如下： ( 1 ) 单独一个个体符或约束变元符是一个类型项。 ( 2 ) 若e = 是一个n 元函数符，f n 是一个n 元函数词， t i 分别是类型为1 ；i 的类型项，1 i n ，那么，t = f i - ( t l ，t 1 1 ) ，t l 一p 是一个类型为t l 百n 百的类型项。今后，我们也用t 来表示类型项。 不含约束变元符的类型项称为类型基项或类型闭项。 定义2 3 类型合式公式( 以下简记为t w f f ) 归纳定义如下： ( 1 ) f “( t l ，t 2 ，t n ) ，t l t n p 是一个类型为t l 1 ；n t 的t w f f ( 称为原子) ，其中，t i 是类型为q 的类型闭项，1 i n ，类型符t 是与基类型 b o o l e a n 保持一致的类型符。 ( 2 ) 若z = ，t l 一p 和= y ，t 叶l b p 是t w f r y 则 1z = 1 ，1 ：1 x 1 ；m p = 1 x ，1 ；1 一p ， x y = x ，1 ；1 x 1 ；m p y ，1 ；m + l x 1 ；n p = x y ，1 ；1 b 一伊， z v y = v = ， 。影一= 一 y ，t i n + l x 1 ；n 一仑= ( 扩展定义后) ， z o = 一 y ，百i n + l ，c n 一伊= x y ，1 ；1 百n p ， 。胁= x ，1 ；1 t m 一伊h y ，一c m + l t n p = x 付y ，百i t n p 也是t w i t ； 特别，若z = 和= 是t w f f ，则 13 2 = 1 x ，p ， 。鼽= x y ，伊， 。乳矽= x v y ，仑， 逻辑程序设计语言g o d e l 的形式化过程性语义 。肛= 一y ，仑( 扩展定义后) ， 。卜拶= x y ，p ， 。贮兮= x - - ) y ，1 7 ) 也是t w i t o ( 3 ) 若甄d ) = z ( d ) ，p 是t w f f ，个体符d = a ，痧在其中出现，约束变元符 w = x ，痧不在其中出现，则 v w 颞w ) = ( 或v x ，跚( x ，驴) = v x ，驴z ( ) 和 3 w j ( w ) = 3 w z ( w ) ，p ( 或j x ，潞( x ，驴) = 了 x ，驴z ( x ，驴) ，p ) 是 伽，其中，敏w ) 和数 ) 分别是用w 和 替换甄d ) 中d 的所有出现而 得的公式，z ( w ) 和z ( x ，痧) 是分别是用w 和 x ，驴替换z ( d ) c pd 的所有出现而得 的公式。 ( 4 ) 只有有限次地使用( 1 ) ( 3 ) 生成的公式才是t w f f o 不含约束变元符的原子称为基原子。 类型合式公式中是不包含自由变元符的。但是，有时候我们也需要考虑类型 一阶语言中含有自由变元符的合法的公式，于是，就有了类型命题形式的概念。 定义2 4 ( 类型命题形式) 如果不同的个体符d l ，d 2 ，d n 在类型合式公 式 中出现，不同的约束变元符w l ，w 2 ，w n 不在其中出 现，n a ( w l ，w 2 ，w n ) ，伊是n 元类型命题形式，其中，t y p e ( w i ) t y p e ( d i ) ， 或两者的类型部分在解释下保持一致。 今后，任何1 1 元类型命题形式统称为类型命题形式。 约束变元符w 是命题形式中未经约束的约束变元符，当且仅当w 在这个类型 命题形式中出现，但v w 和3 w 都不在其中出现。 由定义2 4 ，我们也可以用递归归纳定义的方式给出类型命题形式的定义，并 由此定义类型合式公式。 定义2 5 类型命题形式，归纳定义如下： ( 1 ) f “( t l ，t 2 ，t n ) ，t l t 。一p 是一个类型为t l t 。一t 的类型 命题形式( 类型原子命题形式) ，其中，t i 是类型为1 ；