域理论 :域理论

更新时间:2023-11-08 16:33

域理论是研究通常叫做域(domain)的特定种类偏序集合的数学分支。因此域理论可以被看作是序理论的分支。这个领域主要应用于计算机科学中,特别是针对函数式编程语言,用它来指定指称语义。域理论以非常一般化的方式形式化了逼近和收敛的直觉概念,并与拓扑学有密切联系。在计算机科学中指称语义的一个可作为替代的方式是度量空间。

特征

Dana Scott 在 1960 年代后期发起对域的研究的主要动机是为 lambda 演算找寻指称语义。在这种形式化中,认为“函数”通过在这个语言中的特定项指定。在纯粹语法方式下,可以得到从简单函数到接受其他函数作为它的输入参数的函数。再次只使用在这种形式化中的可获得的语法变换,可以获得所谓的不动点组合子(其中最著名的是 Y 组合子);通过定义,它们有如下性质,对于所有函数 f 都有。

公式介绍

要公式化这样一种指称语义,首先会尝试为 lambda 演算构造一个模型,在其中为每个 lambda 项关联上一个真正的(全)函数。这样一种模型将形式化作为纯语法系统的 lambda 演算和作为操纵具体的数学函数的符号系统的 lambda 演算之间的连接。不幸的是,这种模型不能存在,如果存在,它必须包含对应于组合子 Y 的一个真正的全函数,它是计算任意输入函数 f 的不动点的函数。不能给予 Y 这样的函数,因为某些函数(比如“后继函数”)没有不动点。这个对应于 Y 的真正函数至少必须是偏函数,对于某些输入必须是未定义的。

Scott 通过形式化"部分"或"不完全"信息的概念来表示仍未返回一个结果的计算来克服这个困难。通过对计算的每个域(比如自然数)考虑一个额外的元素,表示“未定义”输出,就是永不结束的计算的"结果"来建模。此外,计算的域被装备了一个“次序关系”,在其中"未定义结果"是最小元素。

为 lambda 演算找到模型的一个重要步骤是只考虑保证有最小不动点的那些函数(在这种偏序集合上)。这些函数的集合,与适当的排序一起,再次是这个理论意义上的一个"域"。而限制于所有可获得的函数的一个子集有另一个巨大的好处: 有可能获得包含它们自己的函数空间的域,就是得到应用于自身的函数。

除了这些需要的性质,域理论还允许吸引人的直觉释义。同上所述,计算的域总是部分有序的。这种排序表示信息或知识的层次。元素在这个次序上越高,它就更加明确和包含更多的信息。更低的元素表示不完全的知识或中间结果。

接着通过在这个域上重复的应用单调函数来精制出结果。到达一个不动点等价于完成一个计算。域为这些想法提供了优越的设施,因为可以保证单调函数的不动点的存在,并且在额外的限制下,可以从下面逼近。

免责声明
隐私政策
用户协议
目录 22
0{{catalogNumber[index]}}. {{item.title}}
{{item.title}}
友情链接: