新书推介:《语义网技术体系》
作者:瞿裕忠,胡伟,程龚
   XML论坛     W3CHINA.ORG讨论区     计算机科学论坛     SOAChina论坛     Blog     开放翻译计划     新浪微博  
 
  • 首页
  • 登录
  • 注册
  • 软件下载
  • 资料下载
  • 核心成员
  • 帮助
  •   Add to Google

    >> It is the theory that decides what can be observed. - Albert Einstein
    [返回] 中文XML论坛 - 专业的XML技术讨论区计算机理论与工程『 理论计算机科学 』 → 可计算理论简介(转) 查看新帖用户列表

      发表一个新主题  发表一个新投票  回复主题  (订阅本版) 您是本帖的第 6815 个阅读者浏览上一篇主题  刷新本主题   树形显示贴子 浏览下一篇主题
     * 贴子主题: 可计算理论简介(转) 举报  打印  推荐  IE收藏夹 
       本主题类别:     
     pr0phet 帅哥哟,离线,有人找我吗?射手座1981-12-8
      
      
      等级:大一(猛啃高等数学)
      文章:5
      积分:142
      门派:IEEE.ORG.CN
      注册:2007/6/25

    姓名:(无权查看)
    城市:(无权查看)
    院校:(无权查看)
    给pr0phet发送一个短消息 把pr0phet加入好友 查看pr0phet的个人资料 搜索pr0phet在『 理论计算机科学 』的所有贴子 点击这里发送电邮给pr0phet 引用回复这个贴子 回复这个贴子 查看pr0phet的博客楼主
    发贴心情 可计算理论简介(转)

          在60年代的中国,如果一个大学生不懂工农业常识,例如混淆了韭菜麦子,可能会受到讥笑。本来,闻道有先后,树业有专工。要求一个领域的人理解另一个领域的知识是有些过分。在今天,如果一个计算机科学的硕士或博士不知道什么是不可判定问题,什么是停机问题,为什么停机问题不可解,什么是NP=?P问题,也有可能会受到讥笑。因为这些问题对于计算机科学而言,太基本、太重要了,它们都属于一门称为可计算理论的学科。是计算机科学研究人员应具备的修养型知识。


        可计算理论是关于计算机械本身的数学理论。20世纪前,计算机械总是”算计”别的对象,很少”算计”自己。20世纪 30年代,为了要解决一个基础问题,即是否有存在不可判定问题,数理逻辑 学家提出了几种不同的(后来证明是彼此等价的)关于算法的定义,从而建立了可计算性理论。
    科学家令计算机械 自己”算计”自己,奇迹出现了。图灵用对角线方法,把图灵机自己编码,搅进其自己的计算对象中,证明了停机问题不可解。在一定程度上说明了计算机(程序)的能力有限性。

        30年代前期,K.哥德尔和S.C.克林尼等人创立了递归函数论, 将数论函数的算法可计算性描述为递归性。30年代中期, A.M.图灵和E.L.波斯特彼此独立地提出了理想计算机的 概念,将问题的算法可解性描述为在具有严格定义的理想计算机上的可解性。30年代发展起来的算法理论,对 在40年代后期出现的存储程序型计算机的设计思想是有影响的。图灵提出的理想计算机(称为图灵机)中的一 种通用机就是存储程序型的。

        可计算理论主要内容有:自动机论与形式语言理论;程序理论(包括程序正确性证明、程 序验证等);形式语义学;算法分析和计算复杂性理 论。自动机理论和形式语言理论是50年 代发展起来的。前者的历史还可以上溯到30年代,因为图灵机就是一类自动机(无限自动机)。50年代以来一些 学者开始考虑与现实的计算机更相似的理想计算机,J. 诺伊曼在50年代初提出了有自繁殖功能的计算机的概念。

    王浩在50年代中期提出了一种图灵机的变种,这是一种 比原来的图灵机更接近现实机器的机器。他还提出一种 存储带上的内容不能清除的机器,并证明这种机器是与图灵机等价的。

        60年代前期,又有人提出具有随机存取 存储器的计算机(简称RAM)以及多带图灵机等。 形式语言理论 导源于数理语言学中的乔姆斯基理 论。在这种理论中,形式语言分为四种:①0型语言;②1 型语言;③2型语言;④3型语言。相应地存在着0型、1型、 2 型、3型四种形式文法。1型语言又名上下文有关语言, 2型语言又名上下文无关语言,3型语言又名正则语言。其中2型语言最受人注意。60年代中期,还发现了这四类 语言与四类自动机之间的对应关系(见表形式语言与自 动机的关系) 在上表中,左边所列的语言恰好是右边与之对应的自动机所能识别的语言(见形式语言理论)。 程序设计理论 包括程序正确性证明和程序验证, 它的一些基本概念和方法是40年代后期诺伊曼和图灵等 人提出的。诺伊曼等在一篇论文中提出借助于证明来验证程序正确性的方法。

        J.T.施瓦兹和 M.戴维斯70年代后期提出了一种他们称之为"正确程序 技术"的软件技术。这种方法是先选定成千种基本程序模块,并借助已知的各种验证方法(包括程序正确性证 明)来保证这些基本程序的正确性。然后再提出一组能 保持正确性的程序组合规则。这样,就可以通过不断的 组合,生成各种各样的程序。

        有人指出,程序正确性证明技术所发展出来的"循 环不变式",即一个程序中的某一循环的入口或出口点 上所附的谓词,有些文献中称作"归纳断言",可以用来供程序研究用。也就是说,不像过去那样,对一个给 定的程序找出其若干个循环不变式,然后借助这些不变 式来证明这个程序的正确性;而是在编制这个程序之前, 根据对这一程序的要求,找出若干个循环不变式,然后根据这些不变式来生成这个程序。 自动程序设计的概念也是从40年代提出的。

        1969年又有人独立地提出了这一想法。 程序语言的形式语法的研究,从50年代中期起有了较大的发展。而形式语义的研究自60年代以来虽有不少 研究工作者从事这方面的工作,提出几种不同的语义理 论,主要是操作语义学、指称语义学或称数学语义学、 公理语义学和代数语义学,但仍没有一种公认在软件技术中够用的形式语义学,因而需要提出一种更适于用到 实际计算中的新的语义学。 在程序正确性证明和形式语义学中应用的程序逻辑, 是60年代末发展起来的。

        这是谓词逻辑的一种扩充。原来的谓词逻辑中是没有时间概念的,所考虑的推理关系 是在同一时间里的关系。程序是一种过程,一个程序的 输入谓词与输出谓词之间的逻辑关系就不是同一时间里 的关系。因此,在有关程序性质的推理中,原来的谓词逻辑不够用,需要有一种新的逻辑。 60年代末,E.恩格勒等人创立了算法逻辑。C.A.R. 霍尔也创立了一种程序逻辑。这种逻辑是在原来的逻辑上增加一个程序算子而得到的。

        算法分析和计算复杂性理论 关于算法的复杂性的 研究。关于这一领域的名称曾有争论。一般认为,各类具体算法的复杂性的研究称作算法分析,而一般算法复 杂性的研究称作计算复杂性理论。计算复杂性理论原是 可计算理论的一支,是以各种可计算函数(即递归函数) 的计算复杂性(在早期称作"计算难度")为其研究对象的。可计算性分为理论可计算性和实际可计算性两种。 作为可计算性理论一支的计算复杂性理论,是以前者的 复杂程度为其研究对象的;而作为计算机科学一个领域 的复杂性理论,则是以后者的复杂程度为其研究对象的。

        这一分支的基本问题是要弄清楚实际可计算函数类的结构和一些性质。实际可计算性是一个直观的概念。 如何对这一概念进行精确的描述,是一个并不容易的问 题。60年代中期以来,有关的研究工作者一般是以计算时间多项式有界的函数作为实际可计算的函数。这实际 上是一个论题,而不是一个可以在数学中加以证明或否 证的命题。有人指出,在有关的多项式次数较高时,很难说是实际可计算的。

        另一个带根本性的问题是:确定性机器与非确定性机器的解题能力的比较问题。人们早已知道,确定性图 灵机与非确定性图灵机的解题能力是相等的。因为非确 定性机器虽比确定性机器效率高,而如果计算时间没有 限制,则确定性机器总可以用穷举的方法来模拟非确定性机器。因此,二者的解题能力是一样的。但在计算时 间多项式有界时,二者的解题能力是否相等,这就是有 名的P=? NP问题。 关于计算和算法(包括程序)的研究,对串行计算的性质研究较多,而对并行计算性质的研究则还很不够 (特别是对异步的并行计算更是如此)。因此,关于并 行计算的研究很可能将成为计算机理论的研究重点。                

        对于一个判定问题,如果能够编出一个程序,以域 中任意元素作为输入,当相应的个别问题的解答是肯定 的时候, 的执行将终止并输出"是",否则 的执行不 终止,就称该判定问题为半可判定的。可判定的问题总是半可判定的。集合是递归可枚举集的充分必要条件为 对应的判定问题是半可判定的。 图灵在1936年证明,图灵机的停机问题是不可判定 的,即不存在一个图灵机能够判定任意图灵机对于任意输入是否停机。图灵机的停机问题是半可判定的。图灵 机的停机问题是很重要的,由它可以推出计算机科学、 数学、逻辑学中的许多问题是不可判定的。


       收藏   分享  
    顶(0)
      




    ----------------------------------------------
    Standing on Shoulders of Giants

    点击查看用户来源及管理<br>发贴IP:*.*.*.* 2007/6/29 18:17:00
     
     jxjjhk 帅哥哟,离线,有人找我吗?
      
      
      等级:大一新生
      文章:2
      积分:64
      门派:XML.ORG.CN
      注册:2007/6/30

    姓名:(无权查看)
    城市:(无权查看)
    院校:(无权查看)
    给jxjjhk发送一个短消息 把jxjjhk加入好友 查看jxjjhk的个人资料 搜索jxjjhk在『 理论计算机科学 』的所有贴子 引用回复这个贴子 回复这个贴子 查看jxjjhk的博客2
    发贴心情 
    语言生涩难懂
    没有例子
    点击查看用户来源及管理<br>发贴IP:*.*.*.* 2007/6/30 10:34:00
     
     GoogleAdSense
      
      
      等级:大一新生
      文章:1
      积分:50
      门派:无门无派
      院校:未填写
      注册:2007-01-01
    给Google AdSense发送一个短消息 把Google AdSense加入好友 查看Google AdSense的个人资料 搜索Google AdSense在『 理论计算机科学 』的所有贴子 访问Google AdSense的主页 引用回复这个贴子 回复这个贴子 查看Google AdSense的博客广告
    2024/6/17 19:01:21

    本主题贴数2,分页: [1]

    管理选项修改tag | 锁定 | 解锁 | 提升 | 删除 | 移动 | 固顶 | 总固顶 | 奖励 | 惩罚 | 发布公告
    W3C Contributing Supporter! W 3 C h i n a ( since 2003 ) 旗 下 站 点
    苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》
    62.500ms