可計(jì)算性邏輯中分支切換復(fù)用運(yùn)算研究.pdf

1、可計(jì)算性邏輯(Computability Logic)簡(jiǎn)稱CoL，是由Japaridze首先提出的，它將經(jīng)典邏輯中的真值理論發(fā)展成為可計(jì)算性的正式理論，是對(duì)經(jīng)典邏輯的發(fā)展。在CoL中，我們將可計(jì)算性的問題看成是由機(jī)器和環(huán)境兩種角色參加的博弈，問題的可計(jì)算性表示存在一個(gè)交互圖靈機(jī)總能在表示這個(gè)問題的博弈中取勝;邏輯運(yùn)算符代表可計(jì)算性問題上的運(yùn)算;邏輯公式的永真性表示是永遠(yuǎn)可計(jì)算的問題。
　　在對(duì)博弈和博弈運(yùn)算的研究中，博弈運(yùn)算的靜態(tài)

2、屬性是可計(jì)算性邏輯中最基礎(chǔ)也是非常重要的內(nèi)容。在CoL中，我們更多關(guān)注的是參加博弈的角色在博弈進(jìn)行過程中會(huì)做出什么動(dòng)作，采取什么策略實(shí)現(xiàn)在博弈中取勝，而不關(guān)注他們的博弈速度，這就是靜態(tài)博弈的含義。我們稱一個(gè)博弈A是靜態(tài)的，當(dāng)且僅當(dāng)對(duì)于博弈的角色（機(jī)器或者環(huán)境）(&)，博弈過程中產(chǎn)生的行程△和Γ，△是Γ的(&)-延遲，如果Γ是A中的一個(gè)使得(&)取勝的行程，那么△也是一個(gè)使得(&)取勝行程。因?yàn)樵贑oL中我們研究的博弈都是靜態(tài)博弈，所以，

3、每一個(gè)CoL中的運(yùn)算都需要具有靜態(tài)屬性。
　　CoL是經(jīng)典邏輯的擴(kuò)展，其運(yùn)算符的語(yǔ)義在CoL中與經(jīng)典邏輯的語(yǔ)義是一致的。目前，隨著CoL的發(fā)展，研究者們已經(jīng)提出了很多新的運(yùn)算符，其中分支切換（補(bǔ)）復(fù)用運(yùn)算((d)和(q))是目前最難也是最復(fù)雜的一種運(yùn)算。Japaridze已經(jīng)給出了關(guān)于該運(yùn)算的定義描述，但是沒有給出其靜態(tài)屬性證明。這個(gè)問題也成為了CoL中的open問題之一。所以，本文主要研究了以下三個(gè)問題:切換分支復(fù)用運(yùn)算的靜態(tài)屬

4、性證明、新的切換分支復(fù)用運(yùn)算的靜態(tài)屬性證明、新舊版本的切換分支復(fù)用運(yùn)算的等價(jià)性證明。
　　本文給出了正式的分支切換（補(bǔ)）復(fù)用運(yùn)算的定義，在該定義中，我們采用靜態(tài)博弈的(Lr,Wn)偶對(duì)完成了該運(yùn)算的定義;并且在定義的基礎(chǔ)上給出了該運(yùn)算的靜態(tài)性證明。證明過程中，我們首先給出了已知結(jié)點(diǎn)、外層已知結(jié)點(diǎn)的定義。根據(jù)證明的需要，我們使用了CoL中的行程延遲的概念。行程延遲是指在整個(gè)博弈過程中，參加博弈的機(jī)器或者環(huán)境會(huì)由于各種原因而導(dǎo)致在某個(gè)

5、行程中出現(xiàn)一些運(yùn)算步的延遲。本文給出了一個(gè)引理證明，證明了對(duì)于一個(gè)已知的靜態(tài)博弈A,如果在(d)A的某一個(gè)行程△中由機(jī)器或者環(huán)境做出了一個(gè)非法的步，而且△是Γ的一個(gè)延遲，那么Γ也是(d)A一個(gè)非法步。在(d)和(q)的靜態(tài)屬性證明中，我們使用該引理的結(jié)論，簡(jiǎn)化了△和Γ在出現(xiàn)非法步時(shí)的分析，從而完成了分支切換復(fù)用運(yùn)算的靜態(tài)屬性證明。
　　由于(d)和(q)運(yùn)算定義的復(fù)雜性，使得基于(d)和(q)的推導(dǎo)演繹系統(tǒng)以及應(yīng)用系統(tǒng)的研究非常遲

6、緩，這也影響了整個(gè)CoL研究的進(jìn)程。所以，我們需要改進(jìn)傳統(tǒng)的(d)和(q)定義，試圖尋找更簡(jiǎn)單的定義。本文提出了一個(gè)新的簡(jiǎn)單的(d)和(q)定義，為了區(qū)分之前的傳統(tǒng)定義，我們稱傳統(tǒng)的定義為緊湊版，新的定義稱為寬松版。采用(d)T，(q)T分別表示(d)和(q)的緊湊版，使用(d)L，(q)L分別表示(d)和(q)的寬松版。寬松版的分支切換復(fù)用運(yùn)算定義采用位串表示方法，改變了緊湊版定義中對(duì)結(jié)點(diǎn)的依賴。本文根據(jù)定義也完成了寬松版的靜態(tài)屬性證

7、明。在證明中，我們發(fā)現(xiàn)使用寬松版定義的分支切換復(fù)用運(yùn)算需要考慮的情況明顯減少，利于后續(xù)基于該運(yùn)算的研究。
　　本文介紹了兩個(gè)版本的分支切換復(fù)用運(yùn)算，為了在后續(xù)的基于分支切換復(fù)用運(yùn)算推演系統(tǒng)和應(yīng)用研究中使用寬松版的分支切換復(fù)用運(yùn)算，我們需要給出兩種版本運(yùn)算的等價(jià)性證明。論文中，我們?cè)O(shè)計(jì)了兩個(gè)交互算法證明了兩種版本運(yùn)算的等價(jià)性。由于CoL是基于博弈的交互計(jì)算，所以，我們使用了基于交互計(jì)算的圖靈機(jī)模型-易交互計(jì)算模型(Easy-Play

8、Machine)。通過該交互計(jì)算模型，我們給出了在CoL中可計(jì)算性問題求解步驟、行程和步的產(chǎn)生過程。運(yùn)算等價(jià)性證明的第一個(gè)算法是指存在一個(gè)EPMε1在博弈(d)TA→(d)LA即(q)T(→)A∨(d)LA中取勝。我們根據(jù)博弈設(shè)計(jì)了一個(gè)取勝策略，使得ε1存在并且能夠取勝。第二個(gè)算法中，我們?cè)O(shè)計(jì)了一個(gè)EPMε2，使得它能在博弈(q)L(→)A∨(d)TA中取勝。我們也設(shè)計(jì)了一個(gè)取勝策略，證明這樣的ε2存在。
　　本文的主要研究工作和

9、創(chuàng)新點(diǎn):
　　一、正式的分支切換復(fù)用運(yùn)算的定義和靜態(tài)屬性證明
　　1.我們給出了基于(Lr,Wn)偶對(duì)表示形式的分支切換（補(bǔ)）復(fù)用運(yùn)算的定義。該定義主要是基于樹形結(jié)構(gòu)的思想，重點(diǎn)針對(duì)分支切換復(fù)用運(yùn)算的分支運(yùn)算和切換運(yùn)算進(jìn)行描述。所以，我們將分支運(yùn)算中已知結(jié)點(diǎn)的概念進(jìn)行了重新的定義，細(xì)化給出了外層已知結(jié)點(diǎn)的定義。定義了完成分支運(yùn)算的結(jié)點(diǎn)只能是外層已知結(jié)點(diǎn);完成切換運(yùn)算的可以是任何已知結(jié)點(diǎn)。本文在行程延遲概念的基礎(chǔ)上，給出了靜態(tài)

10、屬性證明。借助于引理的結(jié)果，我們只需要分析兩個(gè)具有延遲關(guān)系的行程。即一個(gè)靜態(tài)博弈A，如果一個(gè)行程Γ是(d)A中的一個(gè)(&)取勝行程，那么其(&)-延遲行程△也是(d)A中的(&)取勝行程。從而證明了(d)是靜態(tài)的。
　　二、新的分支切換復(fù)用運(yùn)算的定義和靜態(tài)屬性證明
　　2.我們根據(jù)傳統(tǒng)的分支切換（補(bǔ)）復(fù)用運(yùn)算定義，采用基于位串的表示方法，給出了一個(gè)新的簡(jiǎn)單版本定義。該定義打破了已知結(jié)點(diǎn)的考慮和限制，定義中直接不需要考慮分支運(yùn)

11、算，簡(jiǎn)化了整個(gè)運(yùn)算。完成運(yùn)算定義之后，我們同樣給出了新的分支切換復(fù)用運(yùn)算的靜態(tài)屬性證明。在整個(gè)證明過程中，我們發(fā)現(xiàn)需要考慮和處理的情況明顯減少，利于基于分支切換復(fù)用運(yùn)算的一些演繹系統(tǒng)和應(yīng)用系統(tǒng)的提出。
　　三、兩種版本運(yùn)算等價(jià)性證明
　　3.博弈的交互計(jì)算特點(diǎn)需要提出新的交互計(jì)算模型的概念，根據(jù)應(yīng)用場(chǎng)合不同，論文介紹了難交互計(jì)算模型和易交互計(jì)算模型，通過這兩種計(jì)算模型，我們可以理解博弈的進(jìn)行過程、步和行程的產(chǎn)生過程。在論文中

12、，我們選用對(duì)于機(jī)器來(lái)說(shuō)更簡(jiǎn)單的易交互計(jì)算模型。事實(shí)上，兩種計(jì)算模型在計(jì)算能力上是等價(jià)的。
　　4.運(yùn)算的等價(jià)性證明，是指在CoL中設(shè)計(jì)基于易交互計(jì)算模型的算法，使得機(jī)器在博弈運(yùn)算中取勝。論文中設(shè)計(jì)了兩個(gè)算法。在第一個(gè)算法中，我們證明存在一個(gè)EPMε1在博弈(q)T(→)A∨(d)LA中取勝。第二個(gè)算法，我們證明了存在一個(gè)EPMε2，使得ε2在博弈(q)L(→)A∨(d)TA中存在取勝策略。從而實(shí)現(xiàn)了運(yùn)算的等價(jià)性證明。
　　本

13、文的進(jìn)一步工作主要包括以下幾個(gè)方面:1.我們計(jì)劃設(shè)計(jì)基于寬松版分支切換（補(bǔ)）復(fù)用運(yùn)算的推理系統(tǒng)。包括給出推理系統(tǒng)的推導(dǎo)原則、新的系統(tǒng)的可靠性和完整性證明。我們計(jì)劃參考Japaridze提出的CL1-CL15的相關(guān)證明方法，設(shè)計(jì)新的CLx推理系統(tǒng)。2.實(shí)現(xiàn)基于分支切換（補(bǔ)）復(fù)用運(yùn)算的應(yīng)用系統(tǒng)。設(shè)計(jì)與實(shí)現(xiàn)CoL的應(yīng)用系統(tǒng)，實(shí)現(xiàn)真正的人機(jī)交互運(yùn)算。為CoL走向具體應(yīng)用來(lái)設(shè)計(jì)平臺(tái)和界面。我們已經(jīng)設(shè)計(jì)和實(shí)現(xiàn)完成了CL1的交互計(jì)算應(yīng)用，這可以為我們