wikipedia词条 Lambda calculus翻译

captivated

本F是 2.2.2 Alpha equivalence 的整理版

2 Informal description
    2.1 Motivation
    2.2 The lambda calculus
            2.2.1 Lambda terms
            2.2.2 Alpha equivalence

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

2.2.2 Alpha equivalence    α-变换/等价变换

---------------------------------------------------------------

A basic form of equivalence, definable on lambda terms, is alpha equivalence. It captures the intuition that the particular choice of a bound variable, in a lambda abstraction, doesn't (usually) matter. For instance, λx.x and λy.y are alpha-equivalent lambda terms, representing the same identity function. Note that the terms x and y aren't alpha-equivalent, because they are not bound in a lambda abstraction. In many presentations, it is usual to identify alpha-equivalent lambda terms.
可以在lambda形式语言的基础上进行定义的最基本的一种相等性判定就是α-变换了。它来自于一种直觉，即在一个lambda抽象中，对一个被绑定的变量名的选择是不重要的。也就是说，λx.x 和 λy.y 这两个形式在α-变换下是等价的，他们代表相同的identity函数。

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

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

The following definitions are necessary in order to be able to define beta reduction.
下面的定义对定义β-规约来说是很重要的。

captivated

本F是 2.2.3 Free variables 的编辑整理版

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.3 Free variables    自由变量

----------------------------------------------------------

The free variables of a term are those variables not bound by a lambda abstraction. That is, the free variables of x are just x; the free variables of λx.t are the free variables of t, with x removed, and the free variables of ts are the union of the free variables of t and s.
自由变量是这么一种形式，他们并没有被一个lambda抽象所绑定。也就是说，形式 x 中的自由变量就是 x，而形式 λx.t 中的自由变量就是 t 中除了被绑定掉的 x 以外的其他自由变量。而 ts 中的自由变量就是 t中的自由变量和s中的自由变量的并集。

For example, the lambda term representing the identity λx.x has no free variables, but the constant function λx.y has a single free variable, y.
比如说，identity函数λx.x没有自由变量，而λx.y函数有一个自由变量，即y。

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

captivated

本F是 2.2.4 Capture-avoiding substitutions 的编辑整理版

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.4 Capture-avoiding substitutions    未绑定替换[madao: capture-avoiding真的不好翻]

---------------------------------------------------------------

Using the definition of free variables, we may now define a capture-avoiding substitution. Suppose t, s and r are lambda terms and x and y are variables. We write t[x := r] for the substitution of r for x in t, in a capture-avoiding manner. That is:
使用自由变量的定义，我们现在可以定义一种“未绑定替换”。假设 t，s 和 r 都是lambda形式，并且 x 和 y 是变量。我们写 t[x := r] 代表在 t 中，将 t 里所有的自由变量 x 替换成形式 r 。也就是说：

@ x[x := r] = r;
@ y[x := r] = y;if x != y 前提是 x 和 y 不等价
@ (ts)[x := r] = (t[x := r])(s[x := r]);
@ (λx.t)[x := r] = λx.t;
@ (λy.t)[x := r] = λy.(t[x := r]); if x != y and y is not in the free variables of r(sometimes said y is fresh for r). 前提是 x 和 y 不等价，且 y 不是 r 中的自由变量。（也就是说，对 r 来说，y 是新引入的变量[不存在或者已经被绑定]。）

比如说，

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

复制代码

且：

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

复制代码

The freshness condition (requiring that y is not in the free variables of r) is crucial in order to ensure that substitution does not change the meaning of functions. For example, suppose we define another substitution action without the freshness condition. Then,
是否是新引入的变量的前提（即要求 y 不是 r 的自由变量）是很重要的，它确保了替换不会改变函数的意义。比如说，假设我们应用另一个没有引入变量判定的规则，那么

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

复制代码

and the constant function λx.y turns into the identity λx.x by substitution.
通过这个规则[madao: 没有引入变量判定]，常函数 λx.y 变成恒等函数 λx.x了。

If our freshness condition is not met, then we may simply alpha-rename with a suitably fresh variable. For example, switching back to our correct notion of substitution, in (λy.x)[x:=y] the lambda abstraction can be renamed with a fresh variable z, to obtain (λz.x)[x:=y] = λz.(x[x:=y]) = λz.y, and the meaning of the function is preserved by substitution.
如果我们发现的确有冲突的名字，那么我们可以通过一次简单的α-变换来简单地引入一个新的变量名。比如说，换回我们正确的替换规则，在 (λy.x)[x:=y] 中，lambda抽象可以通过引入一个新的变量 z 来变换成满足要求的形式，这样：(λz.x)[x:=y] = λz.(x[x:=y]) = λz.y，函数的意义在替换之后没有改变。

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

captivated

本F是 2.2.5 Beta reduction 的整理版.

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

=======================================
2.2.5 Beta reduction   β-规约

Beta reduction states that an application of the form (λx.t)s reduces to the term t[x := s] (we write (λx.t)s → t[x := s] as a convenient shorthand for “ (λx.t)s beta reduces to t[x := s] ”). For example, for every s we have (λx.x)s → x[x := s] = s, demonstrating that λx.x really is the identity. Similarly, (λx.y)s → y[x := s] = y, demonstrating that λx.y really is a constant function.
β-规约意味着，一个函数应用 (λ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 的确是个常函数。

The lambda calculus may be seen as an idealised functional programming language, like Haskell or Standard ML. Under this view, beta reduction corresponds to a computational step, and in the untyped lambda calculus, as presented here, reduction need not terminate. For instance, consider the term (λx.xx)(λx.xx) . Here, we have (λx.xx)(λx.xx) → (xx)[x := λx.xx] = (x[x := λx.xx])(x[x := λx.xx]) = (λx.xx)(λx.xx). That is, the term reduces to itself in a single beta reduction, and therefore reduction will never terminate.
lambda演算可以被认为是一种理想化的函数式编程语言。如同Haskell或Standard ML一样。从这一点看，β-规约对应了一个计算步骤，而在无类型的lambda演算中，规约并不要求会终止[starwing83: 说白了，就是对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) 。也就是说，这个形式在单次β-变换中，会规约到自身。所以规约将永不会有终止的机会。

Another problem with the untyped lambda calculus is the inability to distinguish between different kinds of data. For instance, we may want to write a function that only operates on numbers. However, in the untyped lambda calculus, there's no way to prevent our function from being applied to truth values, or strings, for instance.
无类型的lambda演算的另一个问题是它无法区分不同类型的数据。比如说，我们也许希望一个函数仅仅处理数字，然而，在无类型的lambda演算中，我们无法阻止我们的函数去处理真假、字符串等等其他类型的值。
[starwing83: 注意在数学意义上的lambda演算中是没有数字，真假，字符串这么一说的，只有两个东西：变量和抽象，即所有的符号就只有λ，.，变量和()括号，如果要进行数字推理，我们需要用着几样东西来表达数字，一种方式是丘奇演算——同样是丘奇那个老头子提出来的一种变态玩意儿。]

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

同时开始征召第三小节的翻译

captivated

翻译到第二节完结. 非常感谢starwing83的工作.

接下来征召第 3, 4两小节的翻译.

犯难了.... 大侠们快来填坑啊拜托啊.......

captivated

把第三小节翻了... 这个小节比较简单, 而且是重复的内容. 根本就不用翻... 说是形式化定义神马的, 和前面比起来也没形式化到哪里去... 要说嘛 可能是因为 λ本身就是形式化的吧啊喂...


3 Formal definition    形式化定义
    3.1 Definition
    3.2 Notation
    3.3 Free and bound variables

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

3.1 Definition  定义

---------------------------------------------------------

Lambda expressions are composed of
λ表达式有如下基本符号集.

    variables v1, v2, ..., vn, ...
    the abstraction symbols λ and .
    parentheses ( )
    变量, v1, v2, ..., vn, ...
    抽象符号, λ and .
    括号 ( )

The set of lambda expressions, Λ, can be defined inductively:
λ表达式的集合用 Λ 表示. 该集合可以归纳地定义如下:

    If x is a variable, then x ∈ Λ
    If x is a variable and M ∈ Λ, then (λx.M) ∈ Λ
    If M, N ∈ Λ, then (M N) ∈ Λ
    1. 如果 x 是一个变量, x ∈ Λ
    2. 如果 x 是一个变量而且 M ∈ Λ, 那么 (λx.M) ∈ Λ
    3. 如果 M, N ∈ Λ, 那么 (M N) ∈ Λ

Instances of rule 2 are known as abstractions and instances of rule 3 are known as applications.[5]
上面的归纳定义中, 第二条归纳定义的实例即 λ抽象, 第三条归纳定义的实例即 λ应用.


---------------------------------------------------------

3.2 Notation 标记方法

---------------------------------------------------------

To keep the notation of lambda expressions uncluttered, the following conventions are usually applied.
为保持 λ表达式标记清晰, 一般遵循如下标记惯例.

@ Outermost parentheses are dropped: M N instead of (M N)
@ Applications are assumed to be left associative: M N P may be written instead of ((M N) P)[6]
@ The body of an abstraction extends as far right as possible: λx.M N means λx.(M N) and not (λx.M) N
@ A sequence of abstractions is contracted: λx.λy.λz.N is abbreviated as λxyz.N[7][8]
@ 没必要把整个表达式外围括起来. 即, 写 M N, 不写 (M N)
@ λ应用是左结合的. 写 M N P 就行了, 没必要写 ((M N) P)
@ λ抽象一直扩展到表达式最右边. λx.M N 表示 λx.(M N), 而不是 (λx.M) N
@ λ抽象序列可以缩写. λx.λy.λz.N 可以缩写为 λxyz.N

---------------------------------------------------------

3.3 Free and bound variables    自由变量和绑定变量

---------------------------------------------------------

The abstraction operator, λ, is said to bind its variable wherever it occurs in the body of the abstraction. Variables that fall within the scope of a lambda are said to be bound. All other variables are called free. For example in the following expression y is a bound variable and x is free: λy.x x y. Also note that a variable binds to its "nearest" lambda. In the following expression one single occurrence of x is bound by the second lambda: λx.y (λx.z x)
λ是一个 λ抽象运算符. 这个运算符所做的运算就是, 将变量绑定到其于λ抽象体出现的位置上. 如是位于该 λ作用域内的变量都被绑定了. 没有位于该 λ作用域内的变量即自由变量. 如 λy.x x y, 在这个 λ表达式中 y 是被绑定的而 x 是自由的[madao: 这个 λ表达式就是 y -> x x y. 为什么, 参见3.2 Notation一节. 有童鞋就要问了, y -> x x y 这里面怎么没有(加减乘除之类的)运算啊? -- 谁说要运算了. λ就没说它要做什么运算啊. 人家明明白白告诉了么, λ这个运算符就是把里面的变量在其出现位置替换就完了, 这个替换动作就是λ运算].
还要注意的是, 变量绑定到"离它最近"的 λ. 比如, λx.y (λx.z x) 这个表达式, x 由第二个 λ 运算符绑定.

The set of free variables of a lambda expression, M, is denoted as FV(M) and is defined by recursion on the structure of the terms, as follows:
一个 λ表达式中的自由变量集合, M, 一般表示为 FV(M) 并且由如下结构形式递归地定义:

    FV(x) = {x}, where x is a variable
    FV(λx.M) = FV(M) \ {x}
    FV(M N) = FV(M) ∪ FV(N)[9]

An expression that contains no free variables is said to be closed. Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic.
我们称一个没有自由变量的 λ表达式是闭合的. 闭合的lambda表达式也就是人们所知的“组合子”，这个概念和组合子逻辑学中的概念“组合子项”等价。[madao: 感谢starwing83指正]
[madao: 顺便, 闭包, closure的原始概念就是说某个运算在某个集合上闭合(结果在集合内)的意思, 参见链接: http://www.codinglabs.org/html/c ... ional-language.html]

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

captivated

我勒个去... 征召啊征召... 木有人响应, madao没信心也木有兴趣做下去了啊. 难不成要搞一烂尾楼么.

前面还好办, 感觉后面有几小节真的要有那个那个才能整下来的啊.

开始征召第四小节的翻译... CUer, 天天灌水那么欢, 能帮madao把这灌完不啊...

starwing83

回复 26# captivated


    Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic.

闭合（而不是封闭）的lambda表达式也就是人们所知的“组合子”，这个概念和组合子逻辑学中的概念“组合子项”等价。

madaossan

回复 28# starwing83


    这是captivated的马甲. 应该只有这个马甲了...

    感谢指正, 已修改.

    starwing83大侠, 接下来的怎么办? 后面有几小节大体看了下, 感觉我搞不定. OwnWaterloo呢... 就期待你们盖完的说, 一个个都不理会... 这让我情何以堪. 要不第四小节拜托了先? 老样子, 你译, 我整理.

OwnWaterloo

看头像就懂了。。。
叔叔，做翻译这事对我来说一点都不funny，看我翻译的东西估计也不会funny。
真要funny。。。  要贡献什么。。。   我觉得还不如说说Lambda calculus这货可以做什么。


比如currying这种东西会对编程，api设计造成什么影响。

比如可以用函数编码struct(那list以及object自然不在话下)，boolean， 甚至还可以蛋疼的用来编码数字。。。
一个有且仅有匿名函数的语言就可以干很多事了， 如果再有宏， 就可以让这些事写得更像其他语言里一样。

至于实际意义。。。 没什么直接的实际意义。
但有间接的意义，比如那各种reduction strategies，对理解Haskell的lazy就很有帮助，对"再"理解其他语言里的if也有帮助，如果愿意的话。