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

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

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

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

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

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

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