`
utensil
  • 浏览: 152420 次
  • 性别: Icon_minigender_1
  • 来自: 深圳
社区版块
存档分类
最新评论

Alonzo Church的λ演算(摘自彭罗斯《皇帝新脑》)

阅读更多

 

可计算性的概念是一个非常重要和美丽的数学观念。它又是相当近代的,具有这样基本性质的事体进入数学的王国是本世纪三十年代的事。这个观念已经渗透到数学的所有领域中去(虽然这一点确实是真的,但是大多数数学家通常不去忧虑可计算性的问题)。该观念的威力有一部分来自于这一个事实,即数学中一些定义得很好的运算实际上不是 可计算的(例如图灵机的停机问题;第四章还可以看到其他例子)。因为如果不存在这种不可计算的事体,则可计算性的概念便没有多少数学的兴趣。数学家毕竟喜欢困惑的东西。让他们决定某些数学运算是否为可计算的可能是非常迷人的困惑。因为那个 困惑的一般解答本身是不可计算的,这一点尤其迷人!

有一件事要弄清楚。可计算性是一个真正“绝对的”数学概念。它是一种抽象的观念,它完全超越按照我们描述的“图灵机”的任何特别实现之外。正如我在以前所评论的,我们不必对表征图灵的天才而特别的手段的“磁带”和“内态”等等赋予任何特别的意义。还有表达可计算性观念的其他方法,历史上最早的是美国逻辑学家阿伦佐·撤屈在斯蒂芬·C·克利涅协助下提出的杰出的“拉姆达计算法”。撤屈的步骤和图灵的完全不同,并且更为抽象得多。事实上,在撤屈陈述他观念的形式中,在它们和任何可以称作“机械的”东西之间只有一点明显的连接。撤屈步骤背后的关键观念在其最本质上的确是抽象的 ,实际上撤屈把这步骤称为“抽象化”的一个数学运算。

不仅是因为撤屈方案强调可计算性是一个独立于计算机器的任何特别概念的数学观念,而且它阐明了在数学中抽象观念的威力,所以我感到值得花一点时间来简要地描述它。对数学观念不熟悉或者对这件事本身不感好奇的读者,在这一阶段可以跳到下一章去,这不会对论证的过程产生多少损失。尽管如此,这样的读者若愿意和我多忍受一阵会得到好处,并且能见证撤屈方案的某些魔术般的经济性(参见撤屈1941)。

人们在此方案中关心的是,譬如由以下表示的对象的“宇宙”

a,b,c,d,…,z,a′,b′,…,z′,a′′,b′′,…,a′′′,…,a′′′′,…

其中每一元素代表一个数学运算或函数 。(带撇字母的原因简单地是,无限地提供以表示这种函数的符号。)这些函数的“自变量”,即它们所作用的东西,是同一类型的其他东西,也就是函数。此外,一个这种函数作用于另一个函数的结果(或“值”)仍是一个函数。(在撤屈的系统中的确具有美妙的概念经济性。)这样,当我们写

a=bc

时,我们是指函数b作用于函数c的结果为另一函数a。要在这个方案中表达两个或更多变量的函数的观念并没有困难。如果我们希望把f认为两个变量,譬如讲p和q的函数,我们可以简单地写

(fp)q

(这是函数fp作用于q的结果)。对于三变量函数我们考虑

((fp)q)r,

等等。

让我们引进抽象化 的有力的运算。为此我们使用希腊字母λ(拉姆达),而且有它后面紧跟着的是代表一个撤屈函数的一个字母,譬如讲x,我们把它当成“哑变量”。任何发生于紧跟在这后面的方括号内的表达式中的变量x是仅仅被当作一个“口”,可以往里面代入任何跟在整个表达式后的任何东西。这样,如果我们写

λx.〔fx〕,

我们是说,当它作用到譬如讲函数a上时,就产生结果fa。那就是

(λx.〔fx〕)a=fa。

换言之,λx.〔fx〕简单地就是函数f,即

λx.〔fx〕=f。

这里只用一点思维就够了。数学的一个美妙在于,初看起来是如此卖弄学识的、琐碎的东西,也是人们非常容易完全失去要点的东西。让我们考虑从中学数学取来的一个熟悉的例子。我们取函数f为对一个角度取正弦的三角运算,这样抽象的函数“sin”被定义为

λx.〔sinx〕=sin。

(不必为何以“函数”x可当作一个角度而忧虑。我们很快就会看到数可被当成函数的某种方法;而一个角度只是一个数。)迄今为止的一切的确是相当无聊的。让我们设想,记号“sin”还没被发明,但是我们熟悉sinx的级数展开表达式

然后我们可以定义

请注意,我们甚至可以更简单地定义,譬如讲“六分之一立方”的运算,它并没有标准的“函数”记号

而且发现,例如

从撤屈的基本函数运算简单地构造的表达式对于现在的讨论更为贴切,例如

λf.〔f(fx)〕。

这是一个函数,当它作用于另一函数,譬如讲g时,产生g两次递归地作用于x上的函数,也就是

(λf.〔f(fx)〕)g=g(gx)。

我们也可以首先“抽象化走”x以得到

λf.〔λx.〔f(fx)〕〕,

此式可以缩写成

λfx〔f(fx)〕。

这是当作用于g时产生“g被递归两次”的函数。事实上,这正是撤屈将其和自然数2相等同的函数。

2=λfx.〔f(fx)〕,

这样,(2g)y=g(gy)。他类似地定义:

3=λfx.〔f(f(fx))〕,4

=λfx〔f(f(f(fx))〕,等等,

以及

1=λfx.〔fx〕,0=λfx,〔x〕。

撤屈的“2”真的更像“两次”,它的“3”是“三次”等等。这样3在一个函数f上的作用,也就是3f是“把f递归三次”的运算。因此,3f在y上的作用是(3f)y=f(f(f(y)))。

让我们看看,一个非常简单的算术运算,也就是如何把1加到一个数上的运算在撤屈方案中表达出来。定义

S=λabc.〔b((ab)c)〕。

为了阐明S的确简单地把1加到用撤屈记号表示的一个数上,让我们做这样的检验:

S3=λabc.〔b((ab)c)〕3=λbc.〔b((3b)c)〕=λbc.〔b(b(b(bc)))〕=4,

这是由于(3b)c=b(b(bc))。很清楚,这可同样好地适用于任何其他自然数。(事实上λabc.〔(ab)(bc)〕可以和S一样好地做到。)

把一个数乘二又如何呢?这种加倍可由

D=λabc.〔(ab)((ab)c)〕

获得,它可再次由作用于3上而得到验证:

D=λabc.〔(ab)((ab)c)〕3=λabc.〔(3b)((3b)c)〕

=λabc.〔(3b)(b(b(bc)))〕=λabc.〔b(b(b(b(b(bc)))))〕=6。

事实上,加法、乘法和升幂的基本算术运算可分别定义为

A=λfgxy.〔((fx)(gx))y〕,

M=λfgx.〔f(gx)〕,

P=λfg.〔fg〕。

读者也许介意使自己或他人信服,我们的确有如下结果:

(Am)n=m+n,(Mm)n=M×n,(Pm)n=n m

这儿m是n是撤屈的两个自然数的函数,m+n是它们和的相应函数,等等。最后那个公式是最令人惊异的。让我们仅仅检验其m=2,n=3的情形:

(p2)3=((λfg.〔fg〕)2)3=(λg.〔2g〕)3

=(λg.〔λfx.〔f(fx)〕g〕)3

=λgx.〔g(gx)〕3=λx.〔3(3x)〕

=λx.〔λfy.〔f(f(fy))〕(3x)〕

=λxy.〔(3x)((3x)((3x)y))〕

=λxy.〔(3x)((3x)(x(x(xy)))))〕

=λxy.〔(3x)(x(x(x(x(xy)))))〕

=λxy.〔x(x(x(x(x(x(x(x(xy))))))))〕

=9=3 2

减法和除法不是这么容易定义的(我们的确需要某种当m比n小时“m-n”以及当m不能被n整除时“m÷n”的惯例。事实上,二十世纪三十年代早期克利涅发现如何在撤屈的方案中表达减法运算被认为是这一学科的重要里程碑!后来接着又有其他的运算。最后,撤屈和图灵在1937年独立地指出,不管什么样的可计算的(或算法的)运算(现在在图灵机的意义上)都可以按照撤屈的一种表达式获得(而且反之亦然)。

这是一个真正惊人的事实,它被用来强调可计算性思想的基本客观性以及数学特征。初看起来,撤屈的可计算性概念和计算机器没有什么关系。然而,它和实际计算具有某些基本关系。尤其是,有力而灵活的电脑LISP语言以一种根本的方式参与到撤屈计算法的基本结构中来。

正如我早先指出的,还有其他定义可计算性概念的方法。波斯特的计算机器的概念和图灵的非常接近,并且几乎是同时独立提出的。近世还有更有用的可计算性(递归性)的定义,这是J·赫伯拉德和哥德尔提出的。H·B·邱雷在1929年,以及M·轩芬克勒在1924年稍早些时候提出了不同的方法,撤屈计算法就是部分地由此发展而来(参见甘迪1988)。现在研究可计算性的手段(诸如在(卡特兰1980)中描述的一台无限记录机器 )在细节上和图灵原先的相差甚多,而且它们更实用得多。然而,不管采用那种不同的手段,可计算性的概念 仍然相同。

正如许多其他的数学观念,尤其是更美丽的、更基本的那些,可计算性的观念似乎自身具有某种柏拉图的实在性 。在下面两章,我们应该探讨的正是数学概念的柏拉图实在性的这个神秘问题。

 

分享到:
评论

相关推荐

    mikrokosmos:(λ)教育性λ演算解释器

    λ演算是计算机科学中的一个基础理论,由Alonzo Church在20世纪30年代提出,用于研究函数计算的本质。λ演算的核心是λ表达式,它是一种表示函数的方法,通过抽象和应用操作来模拟计算过程。mikrokosmos是一个基于...

    Introduction to Lambda Calculus

    它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世纪三十年代引入,Church 运用 lambda 演算在 1936 年给出 判定性问题 (Entscheidungsproblem) 的一个否定的答案。这种演算可以用来清晰地定义什么是一个可计算...

    Python-一个lambda演算的解释器实现

    Lambda演算是数学逻辑中的一个重要概念,由Alonzo Church在20世纪30年代提出,它是一种无类型的函数计算模型,为后来的函数式编程语言奠定了理论基础。在Python中,我们可以用相对简单的代码实现一个Lambda演算的...

    function program

    λ演算由Alonzo Church创建,它是一个简洁而强大的形式系统,用于表达计算。它基于函数抽象和应用的概念,并且能够表达所有可计算的函数。在函数式编程的语境下,λ演算提供了一个强大的理论基础,使得我们可以通过...

    calculus:具有实际封装的新数据类型。 创建智能构造函数,私有和不可变字段,求和类型以及许多其他有趣的东西。 受Alonzo Church启发

    受阿隆佐教堂(Alonzo Church)的启发。 由Lambda微积分提供技术支持。安装可以通过将calculus添加到mix.exs中的依赖项列表中来安装该软件包: def deps do [ { :calculus , " ~> 0.3 " } ]end自述! 这个相当长的...

    函数式编程概要

    λ演算是由美国逻辑学家阿尔弗雷德·丘奇(Alonzo Church)提出的,它是现代函数式编程语言的基础之一。 #### 四、λ演算简介 λ演算是一种形式化的数学理论,用于研究函数抽象和应用的形式化表示方法。它的语法非常...

    lambda演算学习

    该理论由美国逻辑学家阿隆佐·邱奇(Alonzo Church)在1930年代提出,并在其著作《Lambda-Conversion》中进行了详细介绍。Lambda演算不仅是现代计算机科学的基础之一,也是函数式编程语言的理论基础。 #### 二、...

    PHP中的Lambda演算解释器。-PHP开发

    Lambda演算Lambda演算是一种非常小的编程语言,由Alonzo Church于1936年发明。 它的功能等效于PHP中的Turing Machine lambda-php Lambda演算解释器。 Lambda演算Lambda演算是一种非常小的编程语言,由Alonzo Church...

    JavaScript版lamdba演算

    Lambda演算是数学家Alonzo Church在20世纪30年代提出的一种抽象计算理论,它是函数编程的基础,并对现代计算机科学产生了深远影响。Lambda演算的核心概念是λ(lambda)表达式,它允许我们定义匿名函数并进行函数的...

    Orangeboard Lambda Calculus Interpreter-开源

    λ演算是计算机科学中一种抽象的计算模型,由数学家Alonzo Church在20世纪30年代提出,它是函数编程语言的基础,并对理论计算机科学产生了深远影响。 λ演算的核心概念是λ表达式,它是一种表示函数的符号形式。在...

    An Introduction to Functional Programming Through Lambda Calculus

    λ演算由Alonzo Church发明,是理论计算机科学领域的一个核心概念。书中以纯λ演算为基础,逐步引入了函数定义、布尔值、整数、递归、类型、字符、列表和字符串等语法层,构建起一个较为高级的函数式表达形式。本书...

    lambda-talk:一群功能

    1. **λ演算**:λ演算是由Alonzo Church开发的一种形式系统,用于表达计算过程。它以λ符号表示函数定义,通过应用函数到参数上进行计算。λ表达式是λ演算的基本构建块,可以用来表示任何可计算的函数。 2. **...

    Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions

    2. 丘奇(Alonzo Church):他提出了λ演算,这是一种函数定义和计算的抽象形式,后来被证明等价于图灵机。丘奇的λ演算为计算理论提供了理论基础,并且定义了所谓的“丘奇论点”,它主张所有可计算函数都可以用λ...

    ILD-LambdaCalculus

    在编程领域,λ演算是函数式编程的核心理论基础,它由Alonzo Church在20世纪30年代提出,为理解计算的本质提供了一种数学模型。"ILD-λ演算"可能指的是ILisp(Interactive Lisp)或者某种基于λ演算的解释器或编译器...

    gradual-racket:逐渐类型化的 lambda 演算作为一种球拍语言

    λ演算是函数式编程的核心理论,由Alonzo Church在20世纪30年代提出。它是一个简单的形式系统,只包含λ抽象(定义函数)、应用(执行函数)和变量。λ演算的精髓在于它的表达能力,它可以模拟任何计算过程,包括...

    A Tutorial Introduction to the Lambda Calculus

    Lambda演算是一种形式化的计算模型,由美国逻辑学家阿隆佐·丘奇(Alonzo Church)在20世纪30年代提出。它最初是为了研究有效可计算函数的数学性质而开发的。经过数十年的发展,Lambda演算已成为函数式编程语言的强大...

    Alonzo:Alonzo是CS10的有用(略显时髦)的机器人。 他也是我们的吉祥物

    ![Alonzo-Icon] [icon] [![构建状态] [travis-icon... Alonzo的全名当然是[Alonzo Church] [ac-wiki],它是lambda演算的发明者! 他是CS10班级的吉祥物,还有Snap ! 和BJC。 当前功能 警告:这可能并非始终是最新的

    js-church-encoding:JavaScript中的教堂编码实现

    λ演算是由Alonzo Church提出的,它是一种基于函数的计算模型,只有两种基本操作:函数定义(λ表达式)和函数应用。在λ演算中,一切都是函数,包括数值。教堂编码就是在这个基础上,用λ函数来表示各种数据类型。 ...

    程序理论与实践

    Lambda演算由Alonzo Church在1941年创立,与图灵机一起被认为是计算理论的基石之一。 #### 2. Lambda演算的基本概念 Lambda演算的形式系统主要包括两部分:合法表达式的形式系统和变换规则的形式系统。这些规则...

Global site tag (gtag.js) - Google Analytics