勇敢心资源网

当前位置:首页 > 百科 / 正文

递归程式

(2020-05-13 12:07:59) 百科
递归程式

递归程式

问题如下。我们需要给予程式如阶乘函式的定义以语义function factorial(n:Nat):Nat ≡ if (n==0)then 1 else n*factorial(n-1)。 这个阶乘程式的意义应当是在自然数上一个函式,但是由于它的递归定义,如何以複合方式理解它是不明白的。

基本介绍

  • 中文名:递归程式
  • 外文名:definedness
  • 解释:最初主题的函式式递归程式的语义
  • 原因:存在的原因是 F 是连续函式

简介

在本节中我们概览作为指称语义的最初主题的函式式递归程式的语义。
在递归的语义中,域典型的是偏序,它可以被理解为已定义性(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 指示 Fi 次套用。符号“⊔”意味着“最小上界”。
把这个链的构件认为是“叠代”的有益的。在上述阶乘的情况下,我们有在偏函式的域上的函式 F
F(⊥) 是完全未定义偏函式 N→NF(⊥) 是定义在 0 上,得到 1,在其他地方未定义的函式; F(⊥) 是定义直到 4 的阶乘函式: F(⊥)(4) = 24。它对于大于 4 的参数是未定义的。 所以这个链的最小上界是完全定义的阶乘函式(它凑巧是全函式)。
声明:此文信息来源于网络,登载此文只为提供信息参考,并不用于任何商业目的。如有侵权,请及时联系我们:baisebaisebaise@yeah.net
搜索
随机推荐

勇敢心资源网|豫ICP备19027550号