R-演算中若干问题的研究

《R-演算中若干问题的研究》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、R■演算中若干问题的研究吴佳森宋方敏(南京大学软件新技术国家重点实验室南京210093)(南京大学计算机科学与技术系南京210()93)(w.picrric@gmail・com)StudyonR-CalcuiusWuJiasenandSongFangmin(StaleKeyLaboratoryforNovelSoftwareTechnology(NanjingUniversity)9Nanjing210093)(DepartmentofComputerScienceandTechnologyNanjing21

2、0093)AbstractTheR-calculus,proposedbyprofessorLiWei,isarevisioncalculusforformaltheories.ItplaysakeyroleinOPENandGUINAlogic.Itcanbeconsideredasatooltocutouttheprerequisitesofcontradictionwhenatheoryconflictswithsomefacts,henceresultinginaconsistentsub-theory.Inordertogiveapur

3、elysyntacticcalculus-wcmakeadeepexplorationoftheconceptunecessaryprerequisite^wandcharacterizeitinthreedifferentways.Furthermore

4、lyconsistentsubset.ThethirdoneisaninductiveformalizationofR-prerequisite.Bycomparingtheseways,weclaimthateachwayhasitsownadvantagesanddisadvantages.Wechosethelastoneasourapproachtoderiveasoundandrelativelycompletecalculus?namelyR‘・whichcouldbeabettersystemfororiginalpurpose.T

5、helowerboundandupperboundofR-tcrminatcdsetsarcproposed.Andwcprovethatderivingmaximallyconsistentsubsetsofcontradictionisnotonlynon-recursivebutevennotrecursiveenumerable,whichindicatesthatanypurelysyntacticsystemarenotabletobebothsoundandcomplete.KeywordsR-calculus；R-tcrminat

6、cdsets；maximallyconsistentsubsets；recursiveenumerable；soundandcomplete；Rz-calculus摘要李未教授提出了R-演算系统，它是形式理论的修正演算系统•是()PEN过程模式和GUINA1±程模式的基础.R演算在这2种过程模式中的核心作用是，当一个形式理论与事实产生矛盾时•找出矛盾的必要前提•从而获得一个协调的子理论.通过3种不同的方法细致刻画R-演算的基本概念“必要前提''，第1种方法来自R-演算，第2种方法基于极大协调子集与极小非协调子集的，最后一种方法是对于R-必要前提的

7、归纳定义.通过比较这3种方法，指出各自的优缺点•并从第3种方法推演出一个可靠并且相对完全的系统.在比较这3种方法的同时，还细致地探讨了R-终止式的上下界以及极大协调子集的不可枚举性.其中极大协调的不可枚举性在一定程度上表明了不存在一种同时满足可靠并且完全的系统.关键词R-演算；R-终止集；极大协调子集；递归可枚举性；可靠性与完全性；皮-演算中图法分类号0141?TP311.5收稿日期：2010-11-30,修回日期：2011-05-16基金项目：江苏省自然科学基金项目(BK2010374)；软件开发环境国家重点实验室开放课题早金项U(BUAA-S

8、KLSDE-09KF-02)李未教授提出了R-演算系统"］,它是形式理论的修正演算系统，是OPEN过程模式和GUINA过程模式［2七的基