基于類型一階邏輯系統(tǒng)的邏輯程序設計語言語義描述方法的研究.pdf

1、邏輯程序設計是一種說明性程序設計方式，它將程序的邏輯和控制分開，程序員只需考慮邏輯描述部分，控制部分則完全交付語言的編譯或解釋系統(tǒng)完成，這使得人們能在較高的抽象層面上進行程序設計。這一思想需要借助合適的邏輯程序設計語言來展現(xiàn)其優(yōu)勢。Prolog是最具影響的邏輯程序設計語言，它以一階謂詞邏輯的Horn子句邏輯為基礎，其簡單的文法、獨特的說明性適合用于表達人工智能領(lǐng)域中的問題求解，曾經(jīng)受到了人工智能研究和應用開發(fā)者的重視。但Prolog設計

2、相對簡單，未能吸取程序設計語言研究中的諸多先進成果，在使用過程中暴露出了種種不足，尤其是缺乏類型、不支持模塊等，難以適應現(xiàn)代大規(guī)模程序開發(fā)的需要。
　　 G(o)del是繼Prolog之后出現(xiàn)的新型邏輯程序設計語言，它建立在多態(tài)多類的一階邏輯基礎之上，摒棄了Prolog語言中的非邏輯成分，引入多態(tài)多類、模塊化、延遲計算、剪枝操作等諸多新語言成分，是一種高效、先進的說明性邏輯程序設計語言。著眼于G(o)del編譯器的實現(xiàn)和促進該語

3、言的推廣以及深入研究，本文作者在研究小組的探索研究工作中，對基于類型一階邏輯理論的邏輯程序設計語言G(o)del的語義描述方式進行了研究。本文的工作建立在一階邏輯程序的語義模型基礎上，對傳統(tǒng)的一階謂詞邏輯語言進行擴展，引入多態(tài)類型，建立多態(tài)類型一階語言系統(tǒng)的語法和語義理論基礎，用于描述G(o)del程序的說明性和過程性語義，并用于指導G(o)del語言的編譯實現(xiàn)和深入應用開發(fā)。
　　 論文的主要工作和貢獻如下：
　　 首

4、先，參與提出和發(fā)展了多態(tài)類型一階語言，完整地給出了多態(tài)類型一階語言的語法定義，建立了帶類型的一階邏輯理論及其推理規(guī)則；
　　 其次，獨立針對類型一階語言的Horn子集定義了G(o)del語言核心部分的語法，在此基礎上，給出了解釋（或稱賦值）的一般定義，討論了在合理的解釋下類型合式公式的真值判別法，并由此建立帶類型的一階邏輯系統(tǒng)的模型；
　　 第三，利用類型一階語言的Herbrand模型探討了Godel程序的形式化說明性語

5、義，最終得出結(jié)論為最小Herbrand模型MP可以作為程序P的形式語義，其理由是MP恰由作為P的邏輯推論的那些類型基原子組成；
　　 第四，定義由基類型、構(gòu)造類型、結(jié)構(gòu)類型和類型變元組成的類型系統(tǒng)的定型規(guī)則，討論了類型的偏序關(guān)系、相容性關(guān)系，主要解決如何將邏輯程序中的個體符、約束變元符、謂詞符、類型項、類型合式公式和類型命題形式等指派為不同的實體類型對象，給出了對不同類型的對象進行類型檢查與類型推斷的一組算法：
　　 第

6、五，引入了一組定義描述G(o)del中的commt剪枝算子的過程語義，闡述了剪枝算子和支持延遲計算的計算規(guī)則之間的關(guān)系，并給出了剪枝算子的實現(xiàn)方法：
　　 最后，基于類型的合一算法和SLD反駁一消解法，設計邏輯程序求解目標的計算規(guī)則和搜索策略，也就是邏輯程序設計語言的控制機制，從而描述了G(o)del程序的過程性語義。
　　 類型一階邏輯系統(tǒng)為描述邏輯程序的說明性和過程性語義奠定了理論基礎，隨著語言編譯系統(tǒng)逐步完善，G(