wikipedia词条 Lambda calculus翻译

starwing83

回复 8# captivated


    搞定，你整理吧= =里面错别字和低级语法错误顺便改一下，我提交的时候就看到一个地方重复了两次“简单的”，不过已经按了提交键，就不改了= =

OwnWaterloo

回复 7# captivated

有很多说服我不参与翻译的理由。

前面已经说过一个了， 我英文水平也就那样。 从高中开始英语就很少及格。 自己读还勉勉强强， 翻译我搞不定。
翻译出一陀便便既丢我自己的脸， 也误导他人。



翻译是件很蛋疼的事情。 例子太多了。
最近top language上有人在问"fork"该怎么翻译吧？ 而且持续了好多天， 让我又起了退订的冲动。。。
还有前段时间， 一个haskell的群里， 又在争论"side effect"该怎么翻译（具体引起很大争议的貌似不是这个词， 我忘了是哪个了， 不过side effect也讨论过， 而且也算是有争议的例子了）。
另外， 候捷老师也有很多例子。。。
还有一些我忘记在哪里出现的例子了， 大致就是不同的人争论原文里的一句话到底应该怎么翻译。 但我看他们提出的不同翻译都差不多啊？ 这些人到底在争论个毛？

也就是说翻译与精确本身就是冲突的， 100%精确的只有原文， 翻译都是被翻译的人嚼过再吐出，那能一样么？"翻译就是再创作"(by 狗气球)。
这其实都没有关系。
有关系的是很多人以为翻译是能做到精确的，是能够为fork, side effect, pointer, reference等找到一个最准确的中文对应词汇的。
更有甚者会认为只有他那套翻译才是最准确的，于是非要和其他人争个高低。我觉得这种事很浪费时间，fork本身就是最精确的，其他词汇在它面前谈精确完全是笑话。

—— 这段写得很乱，我也不知道该怎么说。
翻译就像"代码风格"那样的东西，本身就没有一个决定性的依据。
但很多人就是看不透，喜欢将自己的主观看法认为是客观真理。引起很多我觉得参与都是浪费时间的争论。



诶，一下子要很清晰有条理的总结出原因也不容易。。。
不过关于lambda calculus，倒是还有一个现成的 —— 我在haskell的一个群里就是这么说的 —— 不翻译的理由。要研究这种"小众"玩意，读英文是必须的。

中文资料太少太少，根本吃不饱。中文资料的程度也参差不齐。这点与资料少结合起来还会产生一个新的现象：没有比较的基准。
例如如果是一个比较大众化的东西，中文资料很多，读者可以通过多读来鉴别不同资料之间的优劣。 而这种小众玩意就做不到。 讲xxx的中文资料就那么几篇， 这些资料说得是否正确？ 根本不知道。
而且还因为小众， 错误都很难被人指出， 这东西就像重金属毒素一样， 越积越多。
总之， 小众的东西的中文资料没有一个好的生态环境， 很难健康发展。

至于能否通过贡献使得小众变为大众？ 恩， 对lambda calculus， 我觉得有生之年看不到。。。 这东西离实践的距离太远。。。

OwnWaterloo

回复 10# starwing83

水平有限是说英文。。。  当然haskell水平也有限。。。  还处于时而玩它时而被它玩的阶段，驾驭不了。。。

captivated

回复 12# OwnWaterloo

OwnWaterloo 发表于 2012-10-21 04:50
回复 7# captivated

有很多说服我不参与翻译的理由。

    嗯. 我几乎完全理解和赞同你所有的理由...   
    不过...

    说过一个了， 我英文水平也就那样。 从高中开始英语就很少及格。 自己读还勉勉强强， 翻译我搞不定。
翻译出一陀便便既丢我自己的脸， 也误导他人。

    放心, 我和许多CUer的英文水平就更...

    也就是说翻译与精确本身就是冲突的， 100%精确的只有原文， 翻译都是被翻译的人嚼过再吐出，那能一样么？"翻译就是再创作"(by 狗气球)。
这其实都没有关系。
   很多人以为翻译是能做到精确的，是能够为fork, side effect, pointer, reference等找到一个最准确的中文对应词汇的。
更有甚者会认为只有他那套翻译才是最准确的，于是非要和其他人争个高低。我觉得这种事很浪费时间，fork本身就是最精确的，其他词汇在它面前谈精确完全是笑话。

    没错, "翻译就是再创作"这句话准确无比. --是的, 有的术语没有中文对应. 即使翻译了, 也无法传达 -- 其结果是, 这个术语需要各种解释和背景 -- 而这各种解释和背景就... -- 对, 这就是需要你而不是我翻译的原因, 因为我个人非常信任你的水准.

    不过关于lambda calculus，倒是还有一个现成的 —— 我在haskell的一个群里就是这么说的 —— 不翻译的理由。要研究这种"小众"玩意，读英文是必须的。

    中文资料太少太少，根本吃不饱。中文资料的程度也参差不齐。这点与资料少结合起来还会产生一个新的现象：没有比较的基准。例如如果是一个比较大众化的东西，中文资料很多，读者可以通过多读来鉴别不同资料之间的优劣。 而这种小众玩意就做不到。 讲xxx的中文资料就那么几篇， 这些资料说得是否正确？ 根本不知道。
    而且还因为小众， 错误都很难被人指出， 这东西就像重金属毒素一样， 越积越多。
    总之， 小众的东西的中文资料没有一个好的生态环境， 很难健康发展。
    至于能否通过贡献使得小众变为大众？ 恩， 对lambda calculus， 我觉得有生之年看不到。。。 这东西离实践的距离太远。。。

    没错. 就这个wikipedia的链接中, 简单地就发现很多相关链接. 其相关链接之相关链接, 又之相关链接, 其内容之多, 涉及之广, 浩如烟海, 如果把这些相关链接全部导出来 -- 它就是wikipedia本身. 所以我非常理解你的 -- 不翻译的理由.

    care的人自然会care, 而且自然会知道如何去care -- 而英文不应该是care这个的障碍. 所以它确实是小众的. 我能说这个是你的基本看法吗

    当然不可能做到把wikipedia在这个帖子中都呈现出来, 但是, 对于本帖所要涉及的, 却并非如此复杂. 从本帖本身的要求来说, 只是需要对本帖再创作. 而这种再创作, 你和starwing83都几乎是最佳人选. 我觉得, 一个正面的回应是应该的.
    对于整个生态, 则不是本帖和你我需要关心的事情 -- care的人自会去care -- 这确实会引出一个悖论 -- 那干嘛要翻译这个?
    喔. 那么先把这个悖论放到一边如何? 把这个引子做出来如何? 如果我说人生其实99.9999...%都是在做无意义的事情 -- "每个保安都是一个哲学家, 因为他天天都在问, 你从哪里来, 你要到何处去, 你是什么人..." -- 你说呢? -- 那么随便干点无意义的事情又如何? 假使这种事情是你认为无意义的 -- 但是也许别的人认为它有意思 -- 至于别的, 先不关心如何?

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

    “大漠孤烟直，长河落日圆”是好诗好句吗？是。这能翻译成英文吗？不能。
    假使一个以英文为母语的人，多久才能领会这佳句？

    Lambda calculus以及许许多多... 这种东西就像鉴赏佳句一样的(这比喻真的不确切. 我以前看NFA to DFA的子集构造, 对其中的形式描述深恶痛绝. 这种东西真的和佳句神马的相去甚远...), 一开始佳句是模糊的, 然后佳句为什么佳句开始清晰, 最终佳句仍旧只是佳句 -- 有人总是先领会佳句, 然后佳句被传诵, 然后佳句变成了佳句.
======================

captivated

回复 13# OwnWaterloo


    得了. OwnWaterloo大侠, 请勿再推辞. 所谓不情之请, 这种事情既然干了就要干到底, 一句话, 拜托了

    PS, 什么是坑, 这就是坑啊...

    不过, 坑我挖了开头却要各位大侠来填  致上歉意先, 有请填坑...

linux_c_py_php

很好, 造福人类.

captivated

        首先感谢starwing83的工作

        接下来是madao(LZ自取外号, 即ma ru de da me na o ssan, 以后就用这个了, 嗯, 嗯)在starwing83原翻译上整理的中英文对照版.

        第二小节是 Informal description, 亦即关于lambda calculus的非形式化描述. 一般来说, 介绍某个稍微比较复杂的东西和系统的时候, 都会先给出非形式化的描述, 然后给出形式化的描述. 因此有必要稍微澄清一下, 究竟什么是形式化的, 什么是非形式化的.

         一般来说, 建立一个系统的方式, 是先有定义和公理, 然后根据定义和公理, 推导各种引理和定理, 然后 -- 一个系统就建立起来了. 比如欧氏几何, 通过有限的公理和公设, 去证明《几何原本》中的所有"真命题". 这估计是人类史上最早的形式化地建立系统的例子,  这个系统的基础是有限的公理和公设, 然后整个系统就是 -- 欧几里得几何, 也即几何原本. 那么欧氏几何就是形式化的.
        由于近代符号逻辑的发展, 形式化(formal methods)一般被纳入符号逻辑/命题逻辑/数理逻辑的数学分支中去了. 不过要注意, 形式化只是一种思考方式, 也就是说形式化方法的本质就像前述说欧氏几何的建立一样. 只不过, 由于数学家们认为, 将这种思考方式符号化从某种程度上有助于思考本身(布尔代数奠基人, 其有一本书的名字就是《The Laws of Thought》). 于是, 在数学上看来, 形式化地建立一个系统需要:

        Formal systems in mathematics consist of the following elements:
        A finite set of symbols (i.e. the alphabet), that can be used for constructing formulas (i.e. finite strings of symbols).
        A grammar, which tells how well-formed formulas (abbreviated wff) are constructed out of the symbols in the alphabet. It is usually required that there be a decision procedure for deciding whether a formula is well formed or not.
        A set of axioms or axiom schemata: each axiom must be a wff.
        A set of inference rules.
        即:
        1. 一组有限的符号集合, 集合中的符号用来构建公式. [比如, 令命题p表示"3 + 2 = 5", p就是一个符号, 代表一个命题. 比如, 对两个命题的合取一般表示为 p ^ q, 即, p成立而且q也成立, 就像C语言中, &&对两个表达式取逻辑乘一样. 对两个命题的析取一般表示为p v q, 即p成立, 或者q成立, 或者二者皆成立]
        2. 语法规则, 就是根据符号集合(亦称字母表)构建合式公式(原文中的well-formed formulas, 一般数理逻辑中译为合式公式)的规则. [合式公式是由命题常项、命题变项、联结词、括号等组成的符号串, 但不是由这些符号任意组成的符号串都是合式公式]. 语法规则用于判断一个公式是不是合式公式.
        3. 一组公理或者公设. 公理和公设必须是合式公式.
        4. 一组推理规则.[三段论神马的].

        即, 形式化方法的本质仍然是: 根据基本的公理和公设, 加上一组推理规则, 然后... 建立整个系统. 就是这个意思. 形式化的方式和别的方式的本质区别在于, 是不是具有有限的基本模型抽象, 然后根据这些基本模型抽象推导出/建立整个系统模型. 对于形式化的方式来说, 由于这种形式化的方式保证了逻辑上的严格性, 在系统日益复杂的情况下, 有可能思考需要回到某个定义本身开始. 因此这种方式被广泛地应用.
====================================

        那么非形式化的方式就是直观地描述. 一上来就给人一套数学形式化描述的东西, 然后让人根据这个东西去推导什么的, 谁都会发疯的. 于是一般在介绍一个形式化的定义/概念之前, 都会先给一大段非形式化的描述, 让人建立起直观的理解, 最后将其形式化地定义下来, 最终就是一个形式化了的系统.

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

captivated

本L是2.1小节的整理版.

2. Informal description 非形式化描述
   2.1 Motivation  基本原理
   
==============================

2.1 Motivation  基本原理

Recursive functions are a fundamental concept within computer science and mathematics. The λ-calculus provides simple semantics for computation, enabling properties of computation to be studied formally.
递归函数是计算机科学和数学中的基础概念。lambda演算提供了对计算的简单描述，以方便对计算涉及到的各种特性进行形式化地研究。

Consider the following two examples. The identity function
考虑下面的两个例子。identity函数[starwing83: 可以翻译为恒等函数，方括号内为译者注，下同]：

1. id(x) = x

复制代码

takes a single input, x, and immediately returns x (i.e. the identity does nothing with its input), whereas the function:
接受单个输入—— x，并立即返回x（也就是说，identity函数没有对输入进行任何处理），第二个例子：

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

复制代码

takes a pair of inputs,  x and y and returns the sum of their squares, x * x + y * y. Using these two examples, we can make some useful observations that motivate the major ideas in lambda calculus.
接受两个输入，x 和 y，并返回他们的平方和，即 x * x + y * y。通过这两个例子，我们可以观察到lambda演算中的的主要思想和原理。

The first observation is that functions need not be explicitly named. That is, the function can be rewritten in anonymous form as
第一个推断是函数并不需要被命名，也就是说，上面的函数可以写成匿名的形式：

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

复制代码

(read as “the pair of  x and y is mapped to x * x + y * y”). Similarly, id(x) = x can be rewritten in anonymous form as x -> x, where the input is simply mapped to itself.
（读作：x，y序对被映射到x*y + y*y），同样的，identity函数也可以被写成匿名的形式x -> x. 表明函数的参数被简单地映射为它自己。[starwing83: 这就是lambda演算的主体：函数的匿名性]

The second observation is that the specific choice of name for a function's arguments is largely irrelevant. That is,
第二个推断是对函数参数名字的选择很大程度上是不重要的，也就是说：

1. x -> x

复制代码

and

1. y -> y

复制代码

express the same function: the identity. Similarly,
代表相同的函数：identity函数。同样的：

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

复制代码

and

1. (u, v) -> u * u + v * v

复制代码

also express the same function.
也表示同样的函数。[starwing83: 这就是lambda演算的第一规则：α-变换]

Finally, any function that requires two inputs, for instance the aforementioned sqsum function, can be reworked into an equivalent function that accepts a single input, and as output returns another function, that in turn accepts a single input. For example,
最后一个[很重要的]推断是，任何需要两个参数的函数，比如上述sqsum函数，都可以被改写成一个接受单个参数，并返回另一个函数的函数，而那个被返回的函数负责接受另一个参数，[madao: 这段翻译非常nice, 避免了歧义]比如：

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

复制代码

can be reworked into
可以被改写为：

1. x -> (y -> x * x + y * y)

复制代码

This transformation is called currying, i.e. transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument (partial application). It can be generalized to functions accepting an arbitrary number of arguments.
这样的一种变换被称为curry变换[madao: 亦称柯里化]。也就是说，将接受多个参数的函数通过这种方式改写为可以通过连续用一个参数进行调用而完成功能的函数[starwing83: 即部分应用]。这个推断可以被推广为接受任意数量的参数。

Applying the above function to the arguments (5, 2), we have:
如果对参数序对(5,2)应用上面的sqsum函数，我们可以得到：

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

复制代码

However, using currying, we have:
然而，如果利用curry变换，我们有：

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

复制代码

and we see the uncurried and curried forms compute the same result. Notice that x * x became a constant after the first argument assignment.
我们可以注意到，序对形式的函数，和curry形式的函数都能够计算出同样的值。注意在第一次应用之后，x * x就成为一个常量[starwing83: ，不再参与后续的替换]了。


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

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

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

复制代码

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

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

复制代码

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

captivated

本F是2.2 the lambda calculus 前言的编辑整理版.

2 Informal description
    2.1 Motivation
    2.2 The lambda calculus

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

2.2 The lambda calculus     lambda演算
----------------------------------------------

The lambda calculus consists of a language of lambda terms along with an equational theory (which can also be understood operationally).
lambda演算由一个被称为“lambda形式语言”[madao: lambda terms]的语言，和一套等价置换规则组成（这套理论本身也能被形式化地理解[starwing83: 和定义][starwing83: 这套规则就两个，α-变换和β-规约，下面会详细解释，这里非形式化的说说，其实就是换参数的名字，和如何进行函数调用（即应用）]）。

Since the names of functions are largely a convenience, the lambda calculus has no means of naming a function. Furthermore, since all functions accepting more than one input can be transformed into equivalent functions accepting a single input (via Currying), the lambda calculus has no means for creating a function that accepts more than one argument. Finally, since the names of arguments are largely irrelevant, the naive notion of equality on lambda terms is alpha-equivalence (see below), which codifies this principle.
因为对函数命名本身可以提供方便性。lambda演算中允许对函数进行对lambda形式语言本身来说无意义的命名。同时，因为所有接受多个参数的函数都可以通过curry转换变成接受单个参数等价函数，所以接受多个参数的函数对lambda演算来说同样也是没意义的[starwing83: 所以不被支持]。最后，因为对参数的命名本身也是很大程度上是不重要的，因此对lambda形式语言的等价判断也需要一种称为“α-变换”的规则进行处理。[starwing83: 为嘛还是没提到β-规约捏……了解了β-规约，才知道到底lambda演算有什么意义。]
=============================

captivated

本F是 2.2.1 lambda terms 的编辑整理版.

2 Informal description
    2.1 Motivation
    2.2 The lambda calculus
            2.2.1 Lambda terms
==================================

2.2.1 Lambda terms       Lambda形式语言
-----------------------------------------------------

The syntax of lambda terms is particularly simple. There are three ways in which to obtain them:
lambda形式语言的语法很简单。下面的三条规则就可以描述它：

@ a lambda term may be a variable, x;
@ 一个lambda形式可以是一个变量，如x。[starwing83: 单个变量 x 是lambda形式。]

@ if t is a lambda term, and x is a variable, then λx . t is a lambda term (called a lambda abstraction);
@ 如果 t 是一个lambda形式，并且 x 是一个变量，那么 λx . t 也是一个lambda形式（这被称为一个lambda抽象）。[starwing83: lambda抽象是lambda形式，另外不知道为什么这里没有提到，lambda抽象是右结合的，即λx.λy.x + y是λx.(λy.x + y)。]

@ if t and s are lambda terms, then ts is a lambda term (called an application).
@ 如果 t 和 s 都是lambda形式，那么 ts 也是一个lambda形式（这被称为一次应用）。[starwing83: lambda应用是lambda形式。][starwing83: @如果 t 是lambda形式，那么 (t) 也是lambda形式——即你可以为了方便起见添加括号。][madao: lambda应用是左结合的。]

Nothing else is a lambda term, though bracketing may be used and may be needed to disambiguate terms. For example, λx . (( λx . x ) x)  and  (λx . (λx . x)) x  denote different terms.
除此以外的形式都不是lambda形式。不过也可以利用括号来防止lambda形式的二义性。比如说λx . (( λx . x ) x) 和 (λx . (λx . x)) x是不同的两个形式。

Intuitively, a lambda abstraction λx.t represents an anonymous function that takes a single input, and the λ is said to bind x in t, and an application ts represents the application of input s to some function t. In the lambda calculus, functions are taken to be 'first class values', so functions may be used as the inputs to other functions, and functions may return functions as their outputs.
直观来说，一个lambda抽象 λx.t 本身代表一个接受单个参数的匿名函数。并且 λ 被称为“在 t 中绑定变量 x ”，一次应用 ts 代表将输入 s 当作参数应用到 t 中。在lambda演算中，函数是“第一类值”[madao: 'first class values']，所以函数本身可以用作其它函数的输入，函数也可以作为其它函数的输出而被返回。

&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&
[madao: http://en.wikipedia.org/wiki/First-class_object
In programming language design, a first-class citizen (also object, entity, or value), in the context of a particular programming language, is an entity that can be constructed at run-time, passed as a parameter, returned from a subroutine, or assigned into a variable. In computer science the term reification is used when referring to the process (technique, mechanism) of making something a first-class object.
The term was coined by Christopher Strachey in the context of “functions as first-class citizens” in the mid-1960s.
程序设计语言中, "一等公民(对象, 实体, 值)", 在指定的程序设计语言中, 是指其可以在运行期被构建, 可以当做参数来传递, 可以从一个子例程返回, 可以赋值给一个变量. 在计算机科学中术语"reification"是指, 使某种东西成为"一等公民"的(技术or机制). 该术语在20世纪60年代中期由Christopher Strachey在其"函数作为一等公民"一文中引入.]
[madao: 在C语言中, 函数不是一等公民. C语言中变量/对象是一等公民. 因为C语言中函数中不能返回函数(虽然你可以返回一个函数指针), 并且C语言中, 函数也不能在运行期被构造出来, 所有的函数在编译期结束即构造完毕. 这里, 已经可以发现一些lambda calculus, 以及实现了lambda calculus的Functional Programming范式语言和命令式编程范式的C语言的一些不同之处.]
&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&

For example, λx.x represents the identity function, x->x, and (λx.x)y represents the identity function applied to y. Further, λx.y represents the constant function x -> y, the function that always returns y, no matter the input. It should be noted that in lambda calculus, function application is regarded as left-associative, so that stx means (st)x.
比如说，λx.x 代表identity函数：x->x，而 (λx.x)y 代表对 y 应用identity函数。另一方面，λx.y 代表“常函数”x -> y [starwing83: 即输入对结果没有任何影响]。无论用什么参数应用这个函数，它始终返回的是 y 。需要注意到的是，在lambda演算中，函数应用被认为是“左结合”的，也就是说 stx 是指 (st)x。

Lambda terms on their own aren't particularly interesting. What makes them interesting are the various notions of 'equivalence' and 'reduction' that can be defined over them.
lambda形式语言本身并没有多大的用处。使它拥有实际价值的是在lambda形式语言基础上所定义的“相等性判定”和“规约”，这些规则[starwing83: 就两个]会在下面定义。

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