wikipedia词条 Lambda calculus翻译

captivated

RT.
=============================

维基百科链接:
http://en.wikipedia.org/wiki/Lambda_calculus
=============================

特邀嘉宾, OwnWaterloo, starwing83
@OwnWaterloo
@starwing83
以及征召各路大虾中...

@幻の上帝(似乎最近很少上CU这版了)

这也许是一个比较无聊的举动(各位不是都像我这样贤德蛋疼)... 而且内容对各位来说也不是什么有意思的东西. LZ发起这个的本意是个人觉得这个对我和一些菜鸟也许有用, 因此烦劳各位大虾驾临于此.

由于翻译是件苦力活, -- 英文读起来就那么回事但用中文表达却觉得别扭或者可能造成误导的情况下尤其如此. 更有甚者, 需要背景知识, -- 嗯, 这个也是要求CUer各路大侠驾临的原因之一.

对于缺乏FP编程背景而且英文又菜的C版CUer(我为其中之一)来说, 各位大侠的贡献一定会被铭记于此. 如若本帖能够如意完结, 必要求版主将其加入精彩类(额... 也许这也是从未发过精彩贴的LZ本人的私心? )

由于对清晰性有一定要求, 请各位大侠遵照下面的约定, 谢谢

=============================

要求:
---------------------------------------------
1. 按照wikipedia目录内容顺序翻译.
    翻译的时候, 在最前面列出是第几小节, 比如, 2.2.1节, Lambda terms什么的. 另外翻译时请讲原文一并贴出.
    另外在翻译之前, 请查看前面的帖子, 看看是不是前面已经有人回帖翻译过了. 如已经翻译过, 可对其内容不明晰之处提出讨论. 所有的翻译都可以回帖讨论, 本人最终将回帖整理出一个清晰完整版. 如下是wikipedia上的内容顺序(See also之后不用了):

Contents
1 Lambda calculus in history of mathematics
2 Informal description
    2.1 Motivation
    2.2 The lambda calculus
            2.2.1 Lambda terms
            2.2.2 Alpha equivalence
            2.2.3 Free variables
            2.2.4 Capture-avoiding substitutions
            2.2.5 Beta reduction
3 Formal definition
    3.1 Definition
    3.2 Notation
    3.3 Free and bound variables
4 Reduction
    4.1 α-conversion
            4.1.1 Substitution
    4.2 β-reduction
    4.3 η-conversion
5 Normal forms and confluence
6 Encoding datatypes
    6.1 Arithmetic in lambda calculus
    6.2 Logic and predicates
    6.3 Pairs
    6.4 Recursion and fixed points
    6.5 Standard terms
7 Typed lambda calculi
8 Computable functions and lambda calculus
9 Undecidability of equivalence
10 Lambda calculus and programming languages
    10.1 Anonymous functions
    10.2 Reduction strategies
    10.3 A note about complexity
    10.4 Parallelism and concurrency
11 Semantics
12 See also
13 References
14 Further reading
15 External links

---------------------------------------------
2. 如要翻译整个小节, 但是要用多个回帖, 比如, 提出要翻译完整6.1节, 但回帖要分多次的情况, 请每个回帖都标注是哪个小节先. 此后看见此小节翻译的人回帖就请暂不再在此小节上纠结了 -- 但是仍可讨论并提出一个认为更加简单明晰的版本.

---------------------------------------------
3. 总的来说, LZ本意是按内容顺序一节一节翻译下来. 当对某节的内容认为可以了, 我回帖启用新节的翻译和新的征召, 要翻译接下来一小节的回帖接受, 然后开始新小节翻译.

---------------------------------------------
4. 如翻译过程中, 作者体现自己的理解, 并加以背景知识的评注, 如此更好. 要求是: The stupider, The Simpler, The Better. 当然, 对某些小节, 本来形式化的描述/定义就是让人蛋疼的事情, 那么形式化的描述/定义则要求精确不偏离原意为好.

=============================


LZ先献丑, 翻译该词条前言.
=============================
Lambda calculus(lambda 演算)

Lambda calculus (also written as λ-calculus or called "the lambda calculus" is a formal system in mathematical logic for expressing computation by way of variable binding and substitution. It was first formulated by Alonzo Church as a way to formalize mathematics through the notion of functions, in contrast to the field of set theory. Although not very successful in that respect, the lambda calculus found early successes in the area of computability theory, such as a negative answer to Hilbert's Entscheidungsproblem.

Lambda演算(也写作λ-calculus)是一个数学逻辑上的形式系统, 通过变量绑定和替换表达计算. 它首先由丘奇提出, 使用函数的观点, 作为数学形式化的一种方式(另一种数学形式化的方式是集合理论). 尽管在这方面(作为数学形式化的手段)不是很成功, 但是Lambda演算是早期在可计算理论上取得成功的案例 -- 比如它给出了希尔伯特可判定性问题的否定答案.

Because of the importance of the notion of variable binding and substitution, there is not just one system of lambda calculus. Historically, the most important system was the untyped lambda calculus. In the untyped lambda calculus, function application has no restrictions (so the notion of the domain of a function is not built into the system). In the Church–Turing Thesis, the untyped lambda calculus is claimed to be capable of computing all effectively calculable functions. The typed lambda calculus is a variety that restricts function application, so that functions can only be applied if they are capable of accepting the given input's "type" of data.

由于变量绑定和替换这种观念的重要性, 存在着不止一种Lambda演算系统.
历史上, 最重要的系统是无类型Lambda演算系统. 在无类型Lambda演算系统中, 函数的[作用/作用域](function application?)没有限制(因此, 函数的定义域(domain)?没有内建于这种系统之中). 在丘奇-图灵论题中, 无类型Lambda演算宣称具有所有计算能力(只要输入是可计算的).
具类型Lambda演算是限制了函数作用(function application)的一种变种, 因此这种函数只能接受"给定类型"的数据.
-----------
[请各位对这段提出评注. 我感觉没有翻译准确. 对于untyped lambda calculus和typed lambda calculus, 有请各位大大进一步阐明, 谢谢]

Today, the lambda calculus has applications in many different areas in mathematics, philosophy, and computer science. It is still used in the area of computability theory, although Turing machines are arguably the preferred model for computation. Lambda calculus has played an important role in the development of the theory of programming languages. The most prominent counterparts to lambda calculus in computer science are functional programming languages, which essentially implement the calculus (augmented with some constants and datatypes). Beyond programming languages, the lambda calculus also has many applications in proof theory. A major example of this is the Curry–Howard correspondence, which gives a correspondence between different systems of typed lambda calculus and systems of formal logic.

现在, Lambda演算被应用到许多不同的领域, 比如数学, 哲学, 以及计算机科学. 它也被用于可计算理论的领域, 尽管图灵机(有争议地)被认为是更受欢迎的可计算模型. Lambda演算在程序设计语言理论的发展中也扮演着重要的角色. 在计算机科学中, 与Lambda演算相匹配的最突出的是函数式编程语言, 这种语言范式基本上(在计算机中)实现了Lambda演算(一般这种语言相对于"纯粹的"Lambda演算来说, 增加了些常量和数据类型). 除程序设计语言之外, 在形式证明理论中也可见到Lambda演算的身影. 一个主要的例子是柯里-霍华德同构(or 柯里-霍华德对应), 其给出了类型Lambda演算系统和形式逻辑系统的对应关系.

=============================


下一节征召翻译ing：

1 Lambda calculus in history of mathematics

=============================

captivated

=============================
接受征召:
1 Lambda calculus in history of mathematics

=============================

1. Lambda calculus in history of mathematics

The lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.[1][2] The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.

lambda演算在20世纪30年代由数学家Alonzo Church提出, 作为研究/调查数学基础理论的一部分. 1935年, Stephen Kleene(此人似乎是正则表达式L* -- Kleene闭包的命名由来)和J. B. Rosser提出了Kleene-Rosser悖论, 表明丘奇的原始的lambda演算系统存在逻辑上的不一致性.

Subsequently, in 1936 Church isolated and published just the portion relevant to computation, what is now called the untyped lambda calculus.[3] In 1940, he also introduced a computationally weaker, but logically consistent system, known as the simply typed lambda calculus.[4]

然后, 1936年, 丘奇分离了原始的Lambda演算系统, 只将原系统中和计算相关的部分发布. 这就是现在称之为untyped lambda calculus的东东. 1940年, 他又提出了一个在计算能力上较弱, 但是逻辑一致的系统, 称之为typed lambda calculus.

=============================
正文中的引用:
[1].^ A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).
丘奇, 《一组关于逻辑基础的假定/前提》, 数学年刊, 序列号2, 33:346-366

[2].^ For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
完整历史, 参看Cardon和Hindley的《lambda演算和组合逻辑的历史》.

[3].^ A. Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, Volume 58, No. 2. (April 1936), pp. 345-363.
丘奇, 《一个初等数论中的unsolvable problem》, 美国数学期刊, 卷58, ...

[4].^ A. Church, "A Formulation of the Simple Theory of Types", Journal of Symbolic Logic, Volume 5 (1940).
丘奇, 《简单类型理论的一个构想》, 符号逻辑期刊, 卷5.

=============================


下一节征召翻译ing:

2. Informal description
    2.1 Motivation
=============================

starwing83

下一节好多图……咋办？

算了，我不管原文了，直接上最终的翻译，谁如果帮我整理一下就更好了。

非形式化的描述
==============

基本原理
--------

    递归函数是计算机科学和数学中的基础概念。lambda演算提供了对计算的简单描述，以方便对计算本身涉及到的原理性的特性镜进行正式的研究。

    考虑下面的两个例子。identity函数[可以翻译为恒等函数，方括号内为译者注，下同]：

        id(x) = x

    接受单个输入——x，并立即返回x（也就是说，identity函数没有对输出进行任何处理），第二个例子：

        sqsum(x, y) = x*x + y*y

    接受两个输入，x和y，并返回他们的平方和，即x*x + y*y。通过这两个例子，我们可以观察到lambda演算中的的主要思想和原理。

    第一个推断是函数并不需要被命名，也就是说，上面的函数可以写成匿名的形式：

        (x, y) -> x*x + y*y

    （读作：x，y序对被映射到x*y + y*y），同样的，identity函数也可以被写成匿名的形式 x -> x，表明函数的参数被简单地映射为它自己。[这就是lambda演算的主体：函数的匿名性]

    第二个推断是对函数参数名字的选择很大程度上是不重要的，也就是说：

        x -> x 和
        y -> y

    代表相同的函数：identity函数。同样的：

        (x, y) -> x*x + y*y 和
        (u, v) -> u*u + v*v

    也表示同样的函数。[这就是lambda演算的第一规则：α-变换]

    最后一个[很重要的]推断是，任何需要两个参数的函数，比如上述sqsum函数，都可以被改写成一个接受单个参数，并返回另一个函数的函数，而那个被返回的函数负责接受另一个参数，比如：

        (x, y) -> x*x + y*y

    可以被改写为：
   
        x -> (y -> x*x + y*y)

    这样的一种变换被称为curry变换。也就是说，将接受多个参数的函数通过这种方式改写为可以通过连续用一个参数进行调用而完成功能的函数[即部分应用]。这个推断可以被推广为接受任意数量的参数。

    如果用参数序对(5,2)应用上面的sqsum函数，我们可以得到：

        ((x, y) -> x*x + y*y)(5, 2)
      = 5*5 + 2*2 = 29

    然而，如果利用curry变换，我们有：

        (x -> (y -> x*x + y*y))(5)(2)
      = (y -> 5*5 + y*y)(2)
      = 5*5 + 2*2 = 29

    我们可以注意到，序对形式的函数，和curry形式的函数都能够计算出同样的值。注意在第一次应用之后，x*x就成为一个常量[，不再参与后续的替换]了。

    [curry用来说明，即使lambda演算的函数仅仅能接受一个值，返回一个值，它也是足够强大的。]

    [还有一个原则没有被提到，即β-规约，它用于定义什么叫“函数应用”，这个概念类似于函数调用，但是有一些不同，这里解释一下，下面会有详细的说明。
    在其他语言里面，函数调用是什么呢？好像是个子程序，执行一些操作，然后返回一个值给你。也许你要的是那个操作，也许你要的就是那个返回的值。
    然而在lambda演算里面不是这样。没有操作，你有的只有lambda形式语言。在这种情形下，函数调用的意思是：调用前的表达式，是和调用后的表达式“等价”的，也就是说，你可以利用函数调用不断地简化你的表达式，比如说：

    (x -> (y -> x*x+y*y))(5)(2)

    这个表达式，看上去很有点复杂，怎么办呢？我们可以利用函数调用，我们认为函数调用前后的表达式是**等价**的，即上面的表达式，和5被“规约进lambda”后的形式：

    (y -> 5*5 + y*y)(2)

    这样的表达式，是等价的。这就是β-规约。利用β-规约，我们能够把我们的程序不断地变换，并观察变换前后所具有的性质。下面会说明，这种变化就是“计算”，这就是lambda演算能够被用来研究“计算”的最根本原因。可能是这个规约太过抽象，所以这里并没有进行讲解，你只要知道这里所谓的函数应用（也就是β-规约）其实都是说的你小学时做算术题时的一步一步的那个步骤（记得每步之前要写等号吧？）即可。]

lambda 演算
-----------

    lambda演算由一个被称为“lambda形式语言”的语言，和一套等价置换规则组成（这套理论本身也能被形式化地理解[和定义][这套规则就两个，α-变换和β-规约，下面会详细解释，这里非形式化的说说，其实就是换参数的名字，和如何进行函数调用（即应用）]）。

    因为对函数命名本身可以提供方便性。lambda演算中允许对函数进行对lambda形式语言本身来说无意义的命名。同时，因为所有接受多个参数的函数都可以通过curry转换变成接受单个参数等价函数，所以接受多个参数的函数对lambda演算来说同样也是没意义的[所以不被支持]。最后，因为对参数的命名本身也是很大程度上是不重要的，因此对lambda形式语言的等价判断也需要一种称为“α-变换”的规则进行处理。[为嘛还是没提到β-规约捏……了解了β-规约，才知道到底lambda演算有什么意义。]

lambda 形式语言
---------------

    lambda形式语言的语法很简单。下面的三条规则就可以描述它：

        - 一个lambda形式可以是一个变量，如x。[单个变量x是lambda形式。]
        - 如果t是一个lambda形式，并且x是一个变量，那么λx . t 也是一个lambda形式（这被称为一个lambda抽象）。[lambda抽象是lambda形式，另外不知道为什么这里没有提到，lambda抽象是右结合的，即λx.λy.x+y是λx.(λy.x+y)。]
        - 如果t和s都是lambda形式，那么t s也是一个lambda形式（这被称为一次应用）。[lambda应用是lambda形式。]
        [- 如果t是lambda形式，那么(t)也是lambda形式——即你可以为了方便起见添加括号。]

    除此以外的形式都不是lambda形式。不过也可以利用括号来防止lambda形式的二义性。比如说λx . (( λx . x ) x) 和 (λx . (λx . x)) x是不同的两个形式。

    直观来说，一个lambda抽象λx.t本身代表一个接受单个参数的匿名函数。并且λ被称为“在t中绑定变量x”，一次应用 t s 代表将输入 s 当作参数应用到 t 中。在lambda演算中，函数是“第一类值”，所以函数本身可以用作其它函数的输入，函数也可以作为其它函数的输出而被返回。

    比如说，λx.x代表identity函数：x->x，而(λx.x)y代表用y应用identity函数。另一方面，λx.y代表“常函数”x -> y[即输入对结果没有任何影响]。无论用什么参数应用这个函数，它始终返回的是y。需要注意到的是，在lambda演算中，函数应用被认为是“左结合”的，也就是说s t x是指(s t) x。

    lambda形式语言本身并没有多大的用处。使它拥有实际价值的是在lambda形式语言基础上所定义的“相等性判定”和“规约”，这些规则[就两个]会在下面定义。

α-变换
---------

    可以在lambda形式语言的基础上进行定义的最基本的一种相等性判定就是α-变换了。它来自于一种直觉，即在一个lambda抽象中，对一个被绑定的变量名的选择是不重要的。也就是说，λx.x和λy.y这两个形式在α-变换下是等价的，他们代表相同的identity函数。

    [这里要说明一下，α-变换本身只是一种对形式的理解。对形式语言来说，语义是不存在的，即语言仅仅是自己所表现的那种无意义的东西，lambda形式语言根本不知道自己表达的是什么，而只有人们在这个基础上，对lambda形式语言的各种语法给予自己直觉上的“解释”，才会让lambda形式语言有意义。如果我们认为一个lambda抽象就是一个（数学意义上的）函数的话，那么α-变换原则就是很自然的了，将lambda形式语言“解释”为函数和函数应用，是α-变换存在的基本前提。]

    [接上段]注意x和y在α-变换下并不是等价的。因为他们并没有被绑定到一个lambda抽象当中。[通过这个原则，]在很多的论文中，都会对lambda形式语进行α-变换。

    下面的定义对定义β-规约来说是很重要的。

自由变量
--------

    自由变量是这么一种形式，他们并没有被一个lambda抽象所绑定。也就是说，形式“x”中的自由变量就是x，而形式λx.t中的自由变量就是t中除了被绑定掉的x以外的其他自由变量。而t s中的自由变量就是t中的自由变量和s中的自由变量的并集。

    比如说，identity函数λx.x没有自由变量，而λx.y函数有一个自由变量，即y。

未绑定替换
----------

    使用自由变量的定义，我们现在可以定义一种“未绑定替换”。假设t，s和r都是lambda形式，并且x和y是变量。我们写t[x := r]代表在t中，将t里所有的自由变量x替换成形式r。也就是说：

      - x[ x := r ] = r；
      - y[ x := r ] = y 前提是 x 和 y 不等价；
      - (t s)[ x := r ] = (t[ x := r ])(s[ x := r ])；
      - (λx.t)[x := r] = λx.t；
      - (λy.t)[x := r] = λy.(t[x := r])，前提是x和y不等价，且y不是r中的自由变量。（也就是说，对r来说，y是新引入的变量[不存在或者已经被绑定]。）

    比如说，(λx.x)[y:=y] = λx.(x[y:=y]) = λx.x，且：

        ((λx.y)x)[x:=y] = ((λx.y)[x:=y])(x[x:=y]) = (λx.y)y。

    是否是新引入的变量的前提（即要求y不是r的自由变量）是很重要的，它确保了替换不会改变函数的意义。比如说，假设我们应用另一个没有引入变量判定的规则，那么(λx.y)[y:=x] = λx.(y[y:=x]) = λx.x，通过这个规则，常函数λx.y变成恒等函数λx.x了。

    如果我们发现的确有冲突的名字，那么我们可以通过一次简单的α-变换来简单地引入一个新的变量名。比如说，换回我们正确的替换规则，在(λy.x)[x:=y]中，lambda抽象可以通过引入一个新的变量z来变换成满足要求的形式，这样：(λz.x)[x:=y] = λz.(x[x:=y]) = λz.y，函数的意义在替换之后没有改变。

β-规约
--------

    β-规约意味着，一个函数应用(λx.t)s可以被规约为t[x:=s]（我们将(λx.t)s -> t[x:s]作为“(λx.t)s被β-规约大t[x:=s]”的简化写法）。比如说，对于每个s，我们有：(λx.x)s -> x[x:s] = s，这说明λx.x的确是恒等的。同样的，(λx.y)s -> y[x:=s] = y，说明λx.y的确是个常函数。

    lambda演算可以被认为是一种理想化的函数式编程语言。如同Haskell或Standard ML一样。从这一点看，β-规约对应了一个计算步骤，而在无类型的lambda演算中，规约并不要求会终止[说白了，就是对lambda演算来说，无限递归是允许的]。比如说，考虑下面的形式(λx.xx)(λx.xx)，这里，我们有(λx.x x)(λx.x x) -> (x x)[x:=λx.x x] = (x[x:=λx.x x])(x[x:=λx.x x]) = (λx.x x)(λx.x x)。也就是说，这个形式在单次β-变换中，会规约到自身。所以规约将永不会有终止的机会。

    无类型的lambda演算的另一个问题是它无法区分不同类型的数据。比如说，我们也许希望一个函数仅仅处理数字，然而，在无类型的lambda演算中，我们无法阻止我们的函数去处理真假、字符串等等其他类型的值。[注意在数学意义上的lambda演算中是没有数字，真假，字符串这么一说的，只有两个东西：变量和抽象，即所有的符号就只有λ，.，变量和()括号，如果要进行数字推理，我们需要用着几样东西来表达数字，一种方式是丘奇演算——同样是丘奇那个老头子提出来的一种变态玩意儿。]


    [本节完结。]

UPDATE: 整理了一下术语。
UPDATE：完结。

[下面是

3 Formal definitions，剩下的事儿俺不管鸟。]

captivated

回复 3# starwing83


    能用代码贴出来的就用代码贴出来. 不能的... 贴图?...

    lambda符号是可以直接copy的. 类似于alpha, beta也可以copy. 比较麻烦的是 "属于/不属于" 这种符号. 这个好像原链接中是图, 没法copy. 不过论坛应该可以显示的, 实在不行就在帖子前面声明用一个(选择一个比较好的吧)可显示的符号代替~. 看了下, 原链接中必须要贴图的情况似乎不多. 基本上, 能清楚表达意思即可.

    请教下untyped lambda calculus 和typed lambda calculus先.

    starwing83大虾, 话说如此星辰如此夜, 你还没睡? 哈哈(PS, 接下来的有劳了)

starwing83

回复 4# captivated


    不管了，我直接翻译，你帮我整理好了。

untyped是原始的，用于数学研究的lambda演算，因为数学上是没有类型可言的，在计算机中，你可以认为这就是“动态类型语言”。计算机上，大部分的lisp以及方言都是这种。

typed是“静态类型的lambda演算”，就是C/C++那种，类型不对就出错那种。这种据说是有类型限制，所以实用起来比较安全，Haskell就属于这种。

我继续翻译，翻译完了就编辑那个帖子，停下来的主要目的是不知道capture-avoiding怎么翻译……反正第二节非形式化描述是我的，剩下的你们自己看着办……

OwnWaterloo

翻译这事。。。 个人水平有限，就不参与了。。。

captivated

回复 6# OwnWaterloo


    starwing83接受了整个第二小节 非形式化描述 我接下来将他的回复整理一下.

   OwnWaterloo视情况接下来的小节接受一个吧. 确实是比较麻烦的事情, 不过既然都特别邀请你了, 总感觉你不整一段说不过去   所以请正视我的请求吧

    就本人认识, 你知识广博程度亦属罕见. 相较于原文来说, 也许你的评注更有意思

    总之, just for fun么~

captivated

回复 5# starwing83


    ok. 等你翻译完第二节我再整理. TKS

captivated

回复 6# OwnWaterloo


    想把第三小节 形式化描述 和第四小节 规约 先派给你... 如何? 要是觉得麻烦, 可以像starwing83那样, 先翻好, 我来整理.

    后面的小节也有请一直参与~

starwing83

回复 6# OwnWaterloo


    少来啦，Haskell大牛，你要是水平有限我们就都是原始人了……整一节玩玩呗，反正又不用你整理= =