（计算机软件与理论专业论文）逻辑程序设计语言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 6 d e l 语言的推广以及深入研究，本文着眼于编译系统的设计与实 现，为g 6 d e l 语言建立了严格的数学基础，包括其语法和说明性语义理论，从而 为其深入研究和编译实现奠定了可靠的部分理论基础。 鉴于传统的一阶逻辑语言的局限性，本文首先对传统的一阶语言进行扩展， 引入类型，提出了类型一阶语言，完整地给出了类型一阶语言的语法定义，初步 建立了带类型的一阶逻辑理论。论文针对类型一阶语言中的h o r n 子集给出了 g 6 d e l 语言( 子集) 的语法部分。在此基础上，给出了解释或赋值的一般定义， 然后讨论在合理的解释下类型合式公式的真假值判别法，并由此建立起带类型的 一阶逻辑系统的模型。接着，利用类型一阶语言的h 模型探讨了g 6 d e l 程序的 形式化说明性语义，最终得出结论为最小h 模型m p 可以作为程序p 的形式语义， 其理由是m p 恰由作为p 的逻辑推论的那些基原子组成。 本文最后还给出了g 6 d e l 语言控制机制的一种实现算法，可以为该语言的完 全实现提供重要支持。 关键词：类型一阶逻辑；g 6 d e l 语言；说明性语义 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 c 、7 i ，i t l lp 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 fl a n g u a g eg 6 d e li s g r e a t l yi n c r e a s e d 谢mt 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 y c 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 e l o g i cp r o g r a m m i n gl a n g u a g e 、析t l lr 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 l e c o m p l e t e l yd 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 g l a n g u a g e ，t h em e t h o d sa n dt e c h n i q u e sc a nn o tt r a n s p l a n t a t i o n t h eb a s i ct h e o r y r e s e a r c hi sl a gb 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 l a n g u a g eg 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 ep r o m o t i o na n di n d e p t hr e s e a r c ho fl a n g u a g eg 6 d e l ，a s t r i c tm a t h e m a t i c a lb a s i so fl a n g u a g eg 6 d e li se s t a b l i s h e di nt h i sp a p e r , i n c l u d i n gi t s g r a m m a ra n dd e c l a r a t i v es e m a n t i ct h e o r y , w h i c hc a nl a yar e l i a b l et h e o r e t i c a lb a s i sf o r t h er e a l i z a t i o no ft h ec o m p i l e rs y s t e mo fl a n g u a g eg 6 d e l i nv i e wo ft h e l i m i t a t i o n so ft h et r a d i t i o n a lf i r s to r d e rl o g i cl a n g u a g e ，t h e t r a d i t i o n a ll a n g u a g eo ff i r s t o r d e ri se x p a n d e d ，a n dac o m p l e t ed e f i n i t i o no ft y p e d f i r s t - o r d e rl a n g u a g ei s g i v e n f i n a l l y , t h et h e o r y o ft y p e df i r s to r d e rl o g i ci s e s t a b l i s h e d ，a n dt h es y n t a xp a r to fl a n g u a g eg 6 d e li sg i v e nb yu s eo ft h eh o r ns u b s e t o ft y p e df i r s t - o r d e rl a n g u a g e o nt h i sb a s i s ，t h eg e n e r a ld e f i n i t i o no fe x p l a n a t i o no r a s s i g n m e n ti sg i v e n ，a n dt h e nt h et r u ev a l u ed i s c r i m i n a n c eo ft y p e dw e l l - f o r m e d f o r m u l ab a s e do nr e a s o n a b l ee x p l a n a t i o ni sd i s c u s s e d t h em o d e lo ft y p e df i r s to r d e r l o g i cs y s t e mi se s t a b l i s h e d ，a n dt h e nt h ed e c l a r a t i v es e m a n t i c so fg 6 d e lp r o g r a mi s d i s c u s s e dt h r o u g ht h eh m o d e lo ft y p e df i r s t - o r d e r l a n g u a g e a n du l t i m a t e l y c o n c l u d e dt h a tt h el e a s th m o d e lm pc a nb eu s e da st h ef o r m a ls e m a n t i c so fp r o g r a m pi ng 6 d e lo nt h eg r o u n d st h a tt h ec o m p o s i t i o no fm pi st h eb a s ea t o m sw h i c hi n f e r f r o mpi nl o g i c f i n a l l y , t h i sp a p e rp r o p o s e dt h ea l g o r i t h mt or e a l i z et h ec o n t r o l a b s t r a c t f a c i l i t yi ng 6 d e ll a n g u a g ew h i c hc a ns u p p o r tt h ef u l l yr e a l i z e do fg 6 d e ll a n g u a g e k e y w o r d s ：t y p e df i r s t o r d e rl o g i c ；g 6 d e ll a n g u a g e ；d e c l a r a t i v es e m a n t i c s 厦门大学学位论文原创性声明 本人呈交的学位论文是本人在导师指导下，独立完成的研究成 果。本人在论文写作中参考其他个人或集体已经发表的研究成果，均 在文中以适当方式明确标明，并符合法律规范和厦门大学研究生学 术活动规范( 试行) 。 另外，该学位论文为() 课题( 组) 的研究成果，获得() 课题( 组) 经费或实验室的 资助，在() 实验室完成。( 请在以上括号内填写课 题或课题组负责人或实验室名称，未有此项声明内容的，可以不作特 别声明。) 伤 争曰了 v 以 日 ) 一 釉声 绺，月0 r o 人 手 叭仁栅卅 厦门大学学位论文著作权使用声明 本人同意厦门大学根据中华人民共和国学位条例暂行实施办 法等规定保留和使用此学位论文，并向主管部门或其指定机构送交 学位论文( 包括纸质版和电子版) ，允许学位论文进入厦门大学图书 馆及其数据库被查阅、借阅。本人同意厦门大学将学位论文加入全国 博士、硕士学位论文共建单位数据库进行检索，将学位论文的标题和 摘要汇编出版，采用影印、缩印或者其它方式合理复制学位论文。 本学位论文属于： () 1 经厦门大学保密委员会审查核定的保密学位论文， 于年月日解密，解密后适用上述授权。 () 2 不保密，适用上述授权。 ( 请在以上相应括号内打“”或填上相应内容。保密学位论文 应是已经厦门大学保密委员会审定过的学位论文，未经厦门大学保密 委员会审定的学位论文均为公开学位论文。此声明栏不填写的，默认 为公开学位论文，均适用上述授权。) 声明人。签名，：高彳知 砒降钐月知 第一章绪论 第一章绪论 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 语言建立了严格的数学基础，侧重其语法和说明性语义理 论，从而为今后深入研究和实现编译系统奠定了可靠的部分理论基础。本章首先 对逻辑程序设计及g 6 d e l 语言的研究现状作简单的介绍。 1 1 逻辑程序设计 逻辑程序设计是计算机科学和人工智能研究的一个重要领域。逻辑程序设计 源于自动理论证明，其中运用了演绎的思想。逻辑程序设计语言的产生是长期以 来逻辑学与计算机科学紧密结合发展的结果。m c c a r t h y 最早提出了用基于逻辑 的语言来表达知识。在机器定理证明的研究中，r o b i n s o n 提出了消解原理 ( r e s o l u t i o np r i n c i p l e ) ，随后又出现了一些对它的改进，包括：l o v e l a n d 提出的 线性消解以及k o w a l s k i 等提出的s l 消解。以上述研究为背景，k o w a l s k i 提出了 逻辑程序设计的思想【4 】。 1 1 1 逻辑程序设计思想概述 对于传统的程序设计来说，算法的逻辑意义往往被程序复杂的控制成分所掩 盖，使程序的正确性难以得到证明；而且通常的高级程序设计语言属于过程性语 言，需要在程序执行前详细规定运行步骤。k o w a l s k i 对传统的算法或对用通常高 级语言编写的程序提出了一个著名的分析公式，即算法= 逻辑+ 控制。k o w a l s k i 的基本思想是要从根本上改变程序设计的方法：用户只需要编写程序的逻辑部分 ( 逻辑程序设计之名由此而来) ，而系统中的解释程序则实施控制部分的职能。 这种将逻辑与控制分开的方法具有下列的优点： 可以在控制部分设计之前不断改进逻辑程序。 可以改进控制部分而无需变动逻辑程序本身。 逻辑程序设计语言g o d e l 的说明性语义 可以从程序说明中生成逻辑程序，加以验证和变换，而无需考虑其控制 部分。 只需在逻辑程序中规定目标和实现这些目标的现有条件，也就是只需告 诉系统做什么( w h a t t od o ) ，至于如何执行也就是说怎样做0 - l o wt od o ) ，则由系 统的控制部分，即解释程序处理解决。 换言之，理想的逻辑程序设计是纯粹的说明程序设计【6 】。 逻辑程序设计试图减少软件说明与可执行描述间的差距，最终目标是能直接 运行软件说明，而无需对低级过程说明细化。逻辑程序设计可简单地描述为程序 员先给出与求解问题相关的事实和性质，然后提问；程序员不用具体给出利用信 息的过程，系统就可以利用程序员提供的信息自动解决问题。逻辑程序设计的全 部工作可简化成形式说明和求证目标请求。对每一个请求，系统根据其知识库通 过推理来证明目标的成立。 在问题求解过程中，无论是用命令式语言，或是用逻辑式语言，都需要程序 员的创造性工作。命令式语言使人们更注重如何用基本操作构造出问题求解的程 序，而逻辑式语言则使人们更专心于问题本身。换句话说，逻辑程序设计迫使我 们集中较多的精力于软件开发的需求分析阶段，并把创造性用于这个关键阶段 【3 】。虽然目前的逻辑程序设计语言的执行效率还无法同传统程序设计语言的执 行效率相比，不过付出效率的代价来减少程序员进行程序设计的负担还是值得 的。 1 1 2 逻辑程序设计语言 顾名思义，逻辑程序设计语言意为将逻辑系统( 具体说是一阶谓词逻辑) 用 作计算机程序设计语言。因此纯逻辑程序设计语言应在逻辑系统的框架之下工 作，本文就是在尽量不超出逻辑框架范围的情况下来介绍逻辑程序设计语言【2 j 。 现行逻辑程序的基本语句属于一阶谓词演算的一个子集，h o m 子句集。h o r n 子句的一般形式为：彳一b la ab 蚪，其中4 、b l ( 1 f 玎) 都是原子公式，分别 代表结论和前提的形式。前提部分是各原子的合取式，构成子句体，结论部分最 多只有一个原子，称为子旬头。由此可将h o r n 子旬分成两个基本类型： 有头h o r n 子句( 用来代表一条规则) ，例如： 2 第一章绪论 g r a n d f a t h e r ( x ，z ) f a t h e r ( x ，力a f a t h e r0 ，z ) 代表：x 是y 的父亲且y 是z 的父亲，则x 是z 的祖父。有头无体的h o r n 子句是 一断言( 用来代表一个事实) 。例如，f a t h e r ( a ，6 ) 代表：a 是b 的父亲；f a t h e r ( b ， 代表：b 是c 的父亲。 无头h o r n 子句，称为目标语句( 用来代表结论的否定式) ，例! t 1 1 - - g r a n d f a t h e r ( a ，c ) 代表：a 不是c 的祖父。逻辑学家a l 仔e dh o r n 对这类子句性质作了详尽的研究， h o r n 子句即因此得名。从问题归约的角度看，可将h o r n 子句解释为一过程，它 将问题( 目标m 归约为若干子问题( 子目标) ，每一子问题b ，( 1 f ，z ) 又可解释 为对其他过程( h o r n 子句) 的调用。有头无尾的h o r n 子句则代表一个已知其解的 基元问题。过程调用实际上是使构成子句体的一个原子( 子目标) 与某一子句头 匹配，这就是运用归结原理中的合一的过程。因此逻辑程序的执行过程也就可以 看成是定理证明过程，其中解释程序起定理证明器或问题求解器的作用。 h o r n 子句的过程调用l ，恐，玩) 可按任意次序进行，适合于并行处 理。h o r n 子句可作过程性的解释也可作陈述性的解释，运用比较方便。因此， 以h o r n 子句为基础的逻辑程序设计受到人们的重视。逻辑程序设计思想在应用 上的最早实现应该是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 语言最大的缺陷。因为编程语言中的类型可以结构化程序所操纵的数据并保证其 正确的使用。虽然p r o l o g 中可以定义记录等各种不同的类型；而且p r o l o g 提供 了列表的表示法，通过算术标识符和算术比较关系，又提供了对数字类型的有限 支持。然而，p r o l o g 不支持检测数据类型，它不检查查询是否按预期的使用程序。 由于没有类型检查，类型错误很容易发生却很难被找出。例如，尽管a p p e n d 3 逻辑程序设计语言g o d e l 的说明性语义 程序本意上是用来连接两个列表的，但它也可以被用于非列表参数： 一a p p e n d ( a ，b 】，坟c ) ，x ) x = bb if i c ) 】 虽然f i e ) 并不是一个列表参数，这个程序也不会报错。实际上几乎每个p r o l o g 程 序都可以被误用。而由于缺少数据类型检查，一些实现上对于效率的改进也无法 实施，各种各样的运行错误也无法阻止。 为了满足软件研究和应用的需要，在近二三十年以来人们对p r o l o g 语言做 了许多扩充和改进，出现了并行逻辑程序设计语言、对象式逻辑程序设计语言9 1 和模糊逻辑程序设计语言等新的逻辑程序设计语言。这些新的语言都在不同程度 上增强了传统逻辑程序设计的内在表达能力并提高了实现效率，但是它们都没有 彻底解决p r o l o g 语言中缺乏类型的问题，而类型逻辑程序设计语言g 6 d e l 的出 现则可以比较好的解决这个问题。 1 1 3 逻辑程序设计的语义研究现状 近二三十年来，人们对逻辑程序设计做了许多扩充和改进，增强了其内在表 达能力、知识组织能力及实现效率，产生了对象式逻辑程序设计、归纳逻辑程序 设计和模糊逻辑程序设计等研究课题。对逻辑程序设计进行研究的核心问题是逻 辑程序的语义【4 】，具体地说，对逻辑程序语义的研究主要反映在以下几个方面： ( 1 ) 经过二三十年的发展，传统的逻辑程序已经有了一些经典的语义。新的研究 试图进一步扩充逻辑程序的语法并定义相应的语义。例如在程序中增加多种形式 的否定，引入面向对象的思想，这些扩充可以进一步提高程序的表达能力。然而， 对于类型逻辑程序设计的语义方面的研究仍然没有取得突破性进展。 ( 2 ) 研究各种语义的性质以及不同语义之间的相互关系。这类研究有助于更深刻 的理解逻辑程序的语义，同时也对扩展和实现语义有所推动。逻辑程序的语义主 要包括说明性语义和过程性语义。说明性语义指出程序中各个子旬以及目标子句 的含义，用于指导程序员编写程序；并且能够给出程序的一个模型，从而说明性 地给出程序的意义。过程性语义以说明性语义为基础，指出程序的运行机制并给 出一个证明过程从而得到程序所能推导出的逻辑结论。 ( 3 ) 研究各种语义的实现。对于复杂度高的语义提供一个高效的算法，或者提供 4 第一章绪论 一些实用的扩展，例如为规则增加权重、为了刻画信息的不完全性提出的析取语 义【1 0 1 等。 1 2g 6 d e l 语言 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 语言存在的缺陷作了诸多改进，引入 了类型系统，增加了新的语言成分，这些都使得g 6 d e l 语言成为一种功能更加强 大的高效的说明性逻辑程序设计语言【l 】。 1 2 1g 6 d e l 语言简介 g 6 d e l 语言的主要特点是引入了参数型多态多类类型系统，增加了延迟计算 等新的语言成分，具有灵活的计算规则和剪枝操作，支持模块化程序设计和元程 序设计，并以系统模块的形式提供丰富的抽象数据类型以支持通用程序设计，对 其适当扩展可支持面向对象程序设计。g 6 d e l 语言的类型系统是一个强类型系统。 类型的引入便于知识表示，因为知识的预期解释在大多数逻辑程序设计应用中是 被类型化的，类型信息有利于发现程序中的错误，提高程序的开发效率，也使得 g 6 d e l 语言具有很强的可表达性能力和实用性。 g 6 d e l 程序的语言说明中约定了每个常量、函数、命题以及谓词的类型，而 变量的类型则是由上下文匹配、推导得到。我们以下面的模块m 为例介绍g 6 d e l 程序中的多态多类类型系统。 m o d u l em b a s e d a y , p e r s o n 模块说明 类型说明 5 逻辑程序设计语言g o d e l 的说明性语义 c o n s t r u c t o rl i s t 1 类型构造子说明 c o n s t a n t n i l ：l i s t ( a ) ； 说明常量n i l 是一个空表 m o n d a y , t u e s d a y , w e d n e s d a y , t h u r s d a y , s u n d a y ：d a y ； f r e d ，m a r y , j a m e s ：p e r s o n f u n c t i o n c o n s ：a * l i s t ( a ) - - - l i s t ( a ) 函数说明 p r e d i c a t e a p p e n d ：l i s t ( a ) * l i s t ( a ) * l i s t ( a ) 谓词说明 p r e d i c a t e g r a n d f a t h e r , f a t h e r ：p e r s o n * p e r s o n g r a n d f a t h e r ( ) 【，z ) 一f a t h e r ( x , y ) af a t h e r ( y , z ) 语句 f a t h e r ( j a m e s ，f r e d ) a p p e n d ( n i l ，kx ) 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 ) 首先，我们讨论它的多类类型。在语言说明中基类( b a s e ) 说明和构造子 ( c o n s t r u c t o r ) 说明决定了程序中使用的类型。若仅说明基类而没有说明 构造子，则所有基类的集合就是程序中可定义的类型集合；若至少说明了一个构 造子，则由基类和构造子出发，得到的基本项( g r o u n dt e r m ) 构成了程序中构造 类型的集合。依一阶逻辑理论，该类型集合是可数无限集。例如，模块m 中说 明了基类类型d a y 和p e r s o n ，说明了一元类型构造子l i s t ，故该模块的类型集合 为： d a y ，p e r s o n ，l i s t ( d a y ) ，l i s t ( p e r s o n ) ，l i s t ( l i s t ( d a y ) ， 。这是一个可数 无限集合，而程序中实际需要的类型只是其中一个有限子集，但这并不影响程序 的语义。其次，讨论它的多态类型。g 6 d e l 语言的多态类型是通过引入类型变量 来实现的。显然，如果一个谓词或函数能表达和处理多种类型，将给程序员带来 很大的方便。一个含有类型变量的多态符号( 函数或谓词) 可以看成类型集合中 所有不同类型的多个符号的集合。例如，模块m 中的谓词说明a p p e n d ，它的3 个参数的类型都为l i s t ( a ) ，其中a 就是类型变量，a 可以取该模块中的任一类型， 这使得a p p e n d 可以对l i s t ( d a y ) ，l i s t ( p e r s o n ) ，l i s t ( l i s t ( d a y ) ) 等类型进行操作， 体现了多态性。 g 6 d e l 语言在引入新的逻辑程序设计语言成分的同时，使该语言具有比 p r o l o g 更优的程序说明性程序语义，而良好的概念化、结构性说明性程序语义对 逻辑程序至为重要。首先，它减轻了程序员的负担，使他们在程序设计时只需 6 第一章绪论 考虑把问题及其相关的知识、逻辑关系定义好，告诉计算机系统“要计算什么 ， 而不必关心“如何计算”，真正的在说明性程序设计方向上又迈进了一步；其次， 当前大多数实用的逻辑程序设计语言都是从p r o l o g 语言演变而来，运用了许多 非说明性的语言成分和非逻辑成分，如c u t 、r e t r a c t 等，而g 6 d e l 在这一方面有 了较大的进步，大大地减少了对非逻辑性成分的依赖，缩小了在逻辑程序设计 中理论与现实之间的差距，有利于逻辑程序的理论分析；而程序设计语言理论 研究表明，具有良好的说明性语义的程序更容易实现并行。 1 2 2 研究g s d e l 语言的意义 g 6 d e l 语言的研究对以下相关领域有较大意义： ( 1 ) 分布式人工智能程序设计。由于g 6 d e l 语言具有良好的数据类型、知识 表示形式与逻辑推理机制，具有一阶理论的支持，可以大大降低工作的复杂程度； ( 2 ) 程序转换、程序分析、调试及有关元程序研究。和p r o l o g 语言相比， g 6 d e l 为这些任务提供了方便，具有更强的说明能力，并且提供了元程序设计的 专门支持，使得说明性调试程序等先进软件工程工具成为可能； ( 3 ) 逻辑程序设计语言的并行实现。g 6 d e l 语言的说明性特征使得语言的并 行实现较为容易，而p r o l o g 语言的非逻辑机制则给并行实现带来困难； ( 4 ) 逻辑程序设计教学。g 6 d e l 和常用语言如m o d u l a 2 一样具有类型和模 块系统，同时，g 6 d e l 摒弃了p r o l o g 中易于混淆的非逻辑谓词，代之以说明性 成分，比p r o l o g 更适合用于扩展语言并用于程序设计的教学，而且，从逻辑程 序设计语言易于过渡到数据库查询语言、形式化规格说明语言； ( 5 ) 逻辑程序设计的理论研究。逻辑程序设计理论和逻辑程序设计语言的非 说明性的语义之间存在着较大的鸿沟，g 6 d e l 语言则缩小了两者在语义上的差 距。 1 2 3g s d e l 语言的研究现状 逻辑程序设计语言的重要性早已为人们所熟知，但g o d e l 语言作为新型逻辑 程序设计语言，它为人们所熟悉和认同需要一定的时间和实践，尤其需要合适的 编译程序和开发环境支持，正如v i s u a lp r o l o g 等一系列解释程序和编译程序在 7 逻辑程序设计语言g o d e l 的说明性语义 p r o l o g 语言的发展以及为人们接受的过程中所起到的重要作用一样。目前， g 6 d e l 语言的研究尚停留在实验阶段，b r i s t o l 大学的研究小组已经开发了单机上 的编译实验程序b r i s t o lg r d e l 。该编译程序用s i c s t u sp r o l o g 实现，并将 s i c s t u sp r o l o g 作为目标语言，但它的执行效率较低且只能在l i n u x 环境下运行， 不具有通用性，而且仅仅实现了g r d e l 语言的一个子梨5 1 。 为了能够完全实现g r d e l 语言，首先需要为其建立严格的数学基础，包括其 语法和语义理论，从而为其实现奠定可靠的理论基础。本文主要研究g r d e l 程序 的说明性语义，对于g r d e l 程序的过程性语义由本课题组其他同学完成。相信随 着类型逻辑程序设计理论的不断完善以及g r d e l 语言编译系统实现技术的逐步 成熟，g r d e l 语言将会受到更多的关注。 1 3 本文的主要工作及篇章结构 本文的研究工作包含两个部分。一部分是提出了类型一阶语言的基本理论， 并在这个基础上给出了g r d e l 语言的语法和g 6 d e l 程序的说明性语义，为g r d e l 语言的编译系统的实现奠定了理论基础。另一部分是讨论了g r d e l 语言控制机制 的研究与实现；控制机制作为g 6 d e l 语言的编译系统中的核心部分，它的实现是 编译系统能够正常运行的基础。 本文一共分为五章。第一章，简要地介绍了逻辑程序设计的基本思想以及 g r d e l 语言：第二章，给出类型一阶逻辑的基本理论以及g 6 d e l 语言的语法；第 三章，建立了带类型的一阶谓词逻辑的模型，并以此为基础，给出g r d e l 程序的 说明性语义；第四章，给出了g r d e l 语言控制机制的一种实现算法，为该语言的 完全实现提供支持；第五章，总结了本文的主要工作，并提出下一步需要解决的 问题和工作设想。 8 第二章类型一阶逻辑与g s d e l 语言的语法 第二章类型一阶逻辑与g i i d e l 语言的语法 作为一种逻辑程序设计语言，研究与开发g 6 d e l ，首先需要为其建立严格的 数学基础，包括其语法和语义理论基础。从p r o l o g 语言和g 6 d e l 语言的关系看， g 6 d e l 的数学基础应该是多态多类的一阶逻辑，而且，g 6 d e l 语言的语法与多态 多类一阶逻辑的类型合式公式之间有着密切的联系，g 6 d e l 语言的语义应该与多 态多类一阶逻辑的模型之间有着密切的联系，于是，发展带类型的一阶逻辑理论 成为一种选择。从另一个角度考察问题，也可以从中发现渊源。一阶逻辑建立的 时候，人们并未考虑将其扩展到多态多类的一阶逻辑。后来，由于计算理论的发 展和形式语义学研究的需要，人们选择了带类型的n 演算来建立语义学理论，由 此形成了后来的类型理论。而实际上，从计算模型的角度看问题，一阶逻辑与k 演算在计算能力上是等价的，于是，可以猜测，带类型的一阶逻辑与带类型的n 演算在计算能力上也应该是等价的。不过，由于两类计算模型在形式上不同，各 自应该有其适用的范围。这样，从计算模型的角度，也有必要发展带类型的一阶 逻辑理论。 2 1 类型一阶语言 为了将来更好地定义g 6 d e l 语言的语法和建立带类型的一阶逻辑的需要，我 们先对带类型的一阶逻辑( 以下简称类型一阶语言) 中出现的一些符号作如下约 定： ( 1 ) 基类型和类型符 由现实世界中的某些( 有穷或无穷) 个体组成的集合称为类型。特别，在 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 语言中，可以通过构造子来定义构造类型。构造子可在程序中定义 9 逻辑程序设计语言g 6 d e l 的说明性语义 和使用，用户可以根据自己的需要，自定义各种类型。如果c s t 是一个1 1 元构造 子，研，r n 是类型，那么e s t n ( 研，葡) 是一个构造类型。例如，l i s t 是一 个1 元构造子，它可以用来构造表类型，如l i s t ( i n t e g e r ) 是一个构造类型，用 来表示整数列表。因此，在g 6 d e l 语言中，基类型属于简单类型，构造类型属于 复杂类型，还有一种类型称为结构类型。结构类型是形如死f n 专f 的类型， 它表示把类型及，蜀规定的一组带类型的对象映射到类型f 规定的类型之对 象的一种抽象的类型结构。结构类型通常用来描述n 元关系或者函数的类型，具 有提示n 元关系和函数中参数的类型和映像结果之对象的类型的作用，具有类似 于属性文法中语义表达式的作用。 我们规定： 构造类型c 。n ( q ，) 和c 2 n ( 研，) 等同或相同，记为 c 。n ( 订，神= c 2 n ( 研一，o r m ) 若n = m ，c 。和c 。是相同的n 元构造子且刁= d i ，1 i n 。 结构类型日葡专f 和o r l x 专o r 等同或相同，记为 死葡争f2 0 1 a m o r 若n = m ，四= a i 且f = o r 。 在不需要特别区分时，简单类型、复杂类型和结构类型统称为类型。 类型符是用来表示类型的抽象的形式符号，是语法层面的概念。类型符在解 释或赋值下只能对应具体的类型。通常，我们用正体希腊字母t ，o ( 可以带下标) 来表示类型符。类型符在语义解释下只能对应为基类型、或构造类型、或结构类 型。类似地，也可以有简单类型符、复杂类型符( 或构造类型符) 、结构类型符。 例2 1 我们以下面的g 6 d e l 程序为例对相关的类型作分析。 c o n s t r u c t o rl i s t 1 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 i s t ( i n t e g e r ) 一l i s 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 有二个参量，它们的类型分别是基类型 1 0 第二章类型一阶逻辑与g s d e l 语言的语法 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 】。谓词a p p e n d 类型声明为： l is t ( 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 ) - - 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 ) 类型集与类型符集 类型集是由类型构成的集合，类型符集是由类型符构成的集合。构成构造类 型( 项) 的每个构造子有一个非负整数表示其参数的个数，其中，0 元构造子的 构造类型就是基类型。 由所有基类型组成的集合称为语言的基本类型集。从基本类型集出发，联合 通过构造子定义的所有类型构成的集合称为( 语言的) 扩展类型集合。 定义2 1 由下面各种符号组成的集合称为类型一阶语言的字母表： ( 1 ) 类型符：t ，o ( 可以带下标) 为表示类型的抽象的形式符号。 ( 2 ) 个体符：二元组d = 表示个体符，用于表达具有某 种类型的个体的形式符号。个体词是用来表示个体的形式符号。通常，个体词用 a ，b ，c ( 可以带下标) 表示，用d ( 可以带下标) 来表示个体符。用个体符形 式上表达个体时，每个个体符都须带有一个类型符，说明个体词所要表达的个体 均有其类型符规定的某种类型。于是，d = 表示具有百类型的个体的形式符 号。 ( 3 ) 约束变元符：二元组w = 表示约束变元符，用 于表达具有某种类型的约束变元的形式符号。通常，约束变元用x ，y ，z ( 可以 带下标) 表示。用约束变元符形式上表达约束变元时，每个约束变元符都须带有 一个类型符，说明约束变元所要表达的变元有其类型符规定的某种类型。于是， w = x ，p 表示具有t 类型的约束变元的形式符号。 当w 为无类型的约束变元符时，w 可以用w = 表示。通常，对于类 型不确定的自由变元符，我们用 ( 可以带下标) 表示。 ( 4 ) 函数符：e = 表示函数符，用于表达具有某种类型的 函数的形式符号。通常，函数词用正体英文字母f ，g ，h ( 可以带下标) 表示，n 逻辑程序设计语言g s d e l 的说明性语义 元函数词可以通过在函数词的右上角添加上标1 1 来表示。函数符中的函数词为1 1 元函数词时，这个函数符也称为n 元函数符。n 元函数符也可以在函数符的右上 角添加上标n 来表示。用函数符形式上表达函数时，每个函数符都须带有一个类 型符，说明函数词所要表达的函数有其类型符规定的某种类型。于是，a 元函数 符e “= f “，百l x1 ：n 寸伊表示具有类型定义为t 1 专t 的n 元函数的形 式符号。 ( 5 ) 谓词符：r = 表示谓词符，用于表达具有布尔值 ( b o o l e a n ) 类型的n 元谓词的形式符号。n 元谓词是用来表达n 元关系的形式符 号。通常，谓词用f ，g ，h ( 可以带下标) 表示，n 元谓词可以通过在谓词的右 上角添加上标n 来表示。谓词符中的谓词为n 元谓词时，这个谓词符也称为n 元 谓词符。n 元谓