递归程序
计算机程序
问题如下。我们需要给予程序如阶乘函数的定义以语义function factorial(n:Nat):Nat ≡ if (n==0)then 1 else n*factorial(n-1)。 这个阶乘程序的意义应当是在自然数上一个函数,但是由于它的递归定义,如何以复合方式理解它是不明白的。
简介
在本节中我们概览作为指称语义的最初主题的函数式递归程序的语义。
在递归的语义中,域典型的是偏序,它可以被理解为已定义性(definedness)的次序。例如,在自然数上的偏函数的集合可以给出为如下次序:
给定偏函数 f 和 g,设“f≤g”意味着“在 f 定义的所有值之上 f 一致于 g”。 通常假定这个域的某个性质,比如链的极限的存在性(参见cpo)和一个底元素。偏函数的偏序有一个底元素,完全未定义函数。它还有链的最小上界。各种额外性质经常是合理的和有用的: 在域理论条目中有更详尽细节。
我们特别感兴趣于在域之间的“连续”函数。它们是保持次序结构和保持最小上界的函数。
在这种设置下,类型被指示为域,而域的元素粗略的捕获了类型的元素。给予带有自由变量的一个程序段的指称语义,依据它从它的环境类型的指称到它的类型的指称的连续函数。例如,段落 n*g(n-1) 有类型 Nat,它有两个自由变量: Nat 类型的n 和 Nat -> Nat 类型的 g。所以它的指称将是连续函数
。 在这个偏函数的次序下,可以如下这样给出阶乘程序的指称。首先,我们必须开发基本构造如 if-then-else, ==, 和乘法的指称。还必须开发函数抽象和应用的指称语义。程序段
其他信息
λ n:N. if (n==0)then 1 else n*g(n-1) 可以接着被给予作为在偏函数的域之间的连续函数的一个指称
。 阶乘程序的指称被定义为函数 F 的最小不动点。它因此是域 的一个元素。
这种不动点存在的原因是 F 是连续函数。一种版本的Tarski不动点定理声称在域上的连续函数有最小不动点。
证明不动点定理的一种方式给出了为什么以这种方式给出递归的语义合适的直觉认识,所有在域 D 的带有底元素 ⊥ 的连续函数 F:D→D 都有不动点,它给出自
⊔i∈NF(⊥)。 这里的符号 F 指示 F 的 i 次应用。符号“⊔”意味着“最小上界”。
把这个链的构件认为是“迭代”的有益的。在上述阶乘的情况下,我们有在偏函数的域上的函数 F。
F(⊥) 是完全未定义偏函数 N→N; F(⊥) 是定义在 0 上,得到 1,在其他地方未定义的函数; F(⊥) 是定义直到 4 的阶乘函数: F(⊥)(4) = 24。它对于大于 4 的参数是未定义的。 所以这个链的最小上界是完全定义的阶乘函数(它凑巧是全函数)。
参考资料
最新修订时间:2023-12-24 18:45
目录
概述
简介
参考资料