查看原文
其他

【第1814期】函数式编程起源-Lambda演算(es2015描述)

Gloria 前端早读课 2019-12-23

前言

今日早读文章由酷家乐@Gloria翻译投稿分享。

正文从这开始~~

判定性问题和可计算性:

在形式化语言中,如何有效地接收并且验证一个命题的正确性?

简单来说,这是早在1928年提出的一个重要的数学问题:“判定性问题” (decision problem)。在数年之后的1936年,Alonzo Church 和 Alan Turing 证明了:为“判定性问题”设计一个通用算法这件事是不可能的。

与此同时,他们各自详细阐述了两个计算模型:Alonzo Church的Lambda演算(后文都称λ演算),Alan Turing的理论机器(之后被称作图灵机)。

冯.诺依曼结构实现了理论上的图灵机,并且用在了如今的电脑上。而Alonzo Church的计算模型,其实与图灵机一样强大,但由于一些历史原因,走了上了一条更加学术化,更不商业化的道路。

本文会借助javascript的语法(es2015)来介绍λ演算中的一些重要概念,展现λ演算对现代语言的影响和对未来编程的重要性。

Lambda演算

λ演算是一个为了表达和计算函数的形式化系统,有着自己的化简规则和语法。整个系统是基于表达式的(也叫λ项)。

一个表达式可以是一个变量(variable),一个抽象体(abstraction)或者一个应用(application)。

  1. expression = variable || abstraction || application

下面是所有的表达式类型:

变量 X 就是一个表达式

  1. variable = expression

如果 X 是变量,E 是表达式,则λx.E是一个抽象体

  1. abstraction = λ(variable).(expression)

如果 E 和 A 都是表达式,则 EA 是一个应用

  1. application = (expression)(expression)

函数抽象体

在λ演算中,函数是用λ表示的匿名函数。一个匿名函数中只存在标识符和他自己的函数体。下面的表达式定义了一个函数(也叫做λ抽象体):

紧跟在λ后面的名字是参数标识符,点(.)后面的表达式是函数体。我们用javascript表示它:

  1. function(x) {

  2. return x

  3. }

改写成箭头函数:

  1. x => x

现在定义一个抽象体,它接收一个变量y,然后返回y的平方,我们可以这么写:

函数应用

函数可以被应用在表达式上。在表达式 EA 中,E 是一个函数,它被应用到了表达式 A 上。换句话来说,表达式 A 就是表达式 E 的输入,然后输出 E(A) 。

把 E 替换成抽象体 λy.y^2,然后得到下面的式子:

  1. const E = y => (y ** 2) // Abstraction

  2. E(A) // Application

通过将函数体中的 y 替换成参数 y 的值,来计算这个函数应用的结果。比如:把表达式 A 替换成整数“5”:

y[y:=A]意思是:在函数体中,所有出现变量 y 的地方必须都被替换成表达式 A 。

多参函数

λ 演算中的所有抽象体都只接收一个参数。如果要实现获取多个参数,就要借助多重应用了。如果有下面这样的函数:

我们其实习惯像下面这样定义和应用它:

  1. const F = (x,y) => (x + y)

  2. F(5, 10)

用不同的方式,我们可以先定义一个函数,这个函数接收一个参数 x ,返回一个新的函数,这个新的函数接收一个参数 y :

  1. const F = x => (y => (x + y))

可以通过下面两步,应用这个接收两个参数的函数:

  1. const F = x => (y => (x + y))

  2. F(5)(10)

  3. // "x => (y => 5 + y)"

  4. // "x => (y => 5 + 10)"

  5. // 15

这个策略就是传说中的“柯里化”(Currying),在Haskell Curry中有介绍。

为了便于理解,想象一个计算矩形面积(A=base * height)的抽象体:

  1. constRectangleArea= base=> (height => (base* height))

  2. RectangleArea(2)(4)

将 2 传进第一个函数的参数 base ,然后返回一个新的函数。将 4 传进第二个函数,作为 height 的值,最终返回这个矩形的面积。

定义数据类型

在无类型λ演算中,函数是唯一的基础类型。所以,如果要使用布尔类型,数字类型以及算数运算,就需要定义一些抽象体去表示它们。接下来我们定义一些比较简单的类型及它们的运算:布尔类型,and 与 or 操作。

如果你想深入了解,推荐看一看 The untyped Lambda Calculus

Alonzo Church 这样定义布尔类型:

  1. constTrue= a => b => a

  2. constFalse= a => b => b

可以把布尔值的逻辑运算看作是一种“抉择行为”。上面两个函数中,都有2个参数,最终返回其中一个参数。不同的是,函数 True 选择返回第一个参数,而函数 False 选择返回第二个。

基于上面的定义,可以得出 If-then-else 的结构:

  1. constIf= Condition=> Then=> Else=> Condition(Then)(Else)

如果 Condition 的位置接收到的是 True ,那么就会返回 Then 作为结果,因为 True 总是返回第一个参数。如果 Condition 的位置接收到的是 False ,那么就会返回 Else 作为结果,因为 False 总是返回第二个参数。

定义下面两个log函数,帮助我们查看运行结果

  1. const isTrue = () => "it's true!"

  2. const isFalse = () => "it's false!"

将布尔值传进 If :

  1. constFirst= If(True)(isTrue)(isFalse)

  2. constSecond= If(False)(isTrue)(isFalse)

  3. First() // "it's true!"

  4. Second() // "it's false!"

现在我们通过化简的过程解释这个结果。我们可以发现 a 其实就是 Then , b 就是 Else :

在了解了 If 的定义之后,再看看 and 和 or 的定义:

  1. constAnd= Exp1=> Exp2=> Exp1(Exp2)(Exp1)

  2. constOr= Exp1=> Exp2=> Exp1(Exp1)(Exp2)

在数学逻辑运算中,只有当两个表达式都是 true 的时候, and 操作符才会返回 true 。or 操作符只有当两个表达式都是 false 的时候,才会返回 false 。基于上面的结论,函数 And 始终会返回 False ,除非 And(True)(True) 这样调用它。函数 Or 始终会返回 True ,除非 Or(False)(False) 这样调用它。

只需要通过置换操作符应用中的变量,就能检验上面所定义的式子。比如像下面这样:

下面是所有可能的化简过程:

  1. | Operator| Reduction| Result|

  2. |-------------------|---------------------|-----------|

  3. | And(True)(True) | True(True)(True) | True|

  4. | And(True)(False) | True(False)(True) | False|

  5. | And(False)(True) | False(True)(False) | False|

  6. | And(False)(False) | False(False)(False) | False|

  7. | Or(True)(True) | True(True)(True) | True|

  8. | Or(True)(False) | True(True)(False) | True|

  9. | Or(False)(True) | False(False)(True) | True|

  10. | Or(False)(False) | False(False)(False) | False|

到目前为止,我们已经定义了很多结构,如:True , False , If , And , Or ,接下来通过比较简单和直观的方式检验一下:

  1. constResult1= If(And(True)(True))(isTrue)(isFalse)

  2. constResult2= If(And(True)(False))(isTrue)(isFalse)

  3. constResult3= If(Or(False)(True))(isTrue)(isFalse)

  4. constResult4= If(Or(False)(False))(isTrue)(isFalse)

  5. Result1() // "it's true"

  6. Result2() // "it's false"

  7. Result3() // "it's true"

  8. Result4() // "it's false"

最后,你需要记住的是,λ演算并不是数据类型的具体实现,只是一个形式化的系统,它并不需要代表任何计算过程,因为都可以使用函数去模拟它们。

λ演算和函数式编程

通过图灵机描述的可计算性,引出了命令式编程。通过λ演算描述的可计算性,引出了函数式编程 -- Cooper & Leeuwen(2013)

早在电子计算机诞生之前,Alonzo Church 就创造了λ演算。但它对现代编程语言却有着深远的影响。作为第二个高级编程语言的Lisp,它就是启发自λ演算。再比如说,所有支持匿名函数的语言里(像Haskell,JavaScript,Python,Ruby等等)都会有几分Alonzo Church的影子。

函数式的模式催生表达能力强的代码,因为这些模式与数学模型有着更加直接的对应关系,因此也更加合理。正因为在数学的世界里,函数式的代码具备引用透明性(给定相同的输入,始终会有相同的输出),这让它可以在多个处理器中同时运行。

λ演算影响着多种多样的现代编程语言,这不仅仅是因为它的形式化系统是图灵完备的,也是因为它的简洁性和表达能力,这些层面上的能力是对未来的编程是非常重要的。

参考资料

  • Henk Barendregt, Erik Barendsen (2000). Introduction to Lambda Calculus.

  • Raúl Rojas (1998). A Tutorial Introduction to the Lambda Calculus.

  • Manuel Eberl (2011). The untyped Lambda Calculus.

  • Barry Cooper, J. van Leeuwen (2013). Alan Turing: His Work and Impact .

关于本文 译者:@Gloria 译文:https://zhuanlan.zhihu.com/p/98104104 作者:@Alexandre Thebaldi 原文:https://medium.com/@ahlechandre/lambda-calculus-with-javascript-897f7e81f259

为你推荐


【第1719期】简明 JavaScript 函数式编程-入门篇


【第1679其】函数式编程浅析

    您可能也对以下帖子感兴趣

    文章有问题?点此查看未经处理的缓存