函数式编程起源-Lambda演算

函数式编程起源-Lambda演算

前言

翻译自:Lambda Calculus with JavaScript

判定性问题和可计算性

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

简单来说,这是早在1928年提出的一个重要的数学问题:“判定性问题” (decision problem)。在数年之后的1936年,Alonzo ChurchAlan 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)

函数抽象体

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

1
λx.x

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

1
2
3
function (x) { 
return x
}

改写成箭头函数:

1
x => x

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

1
λy.y^2

函数应用

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

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

1
2
EA = E(A)
EA = (λy.y^2)(A)

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

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

1
EA = (λy.y^2)(A)=y[y:=A]=A^2=5^2=25

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

多参函数

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

1
f(x,y) = x + y

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

1
2
const F = (x,y) => (x + y)
F(5, 10)

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

1
λx(λy.x+y)

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

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

1
2
(λx.(λy.x+y))(5)=x[x:5]=λy.5+y
(λy.5+y)(10) = y[y := 10] = 5+10 = 15

1
2
3
4
5
const F = x => (y => (x + y))
F(5)(10)
// "x => (y => 5 + y)"
// "x => (y => 5 + 10)"
// 15

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

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

1
λb. (λh.b * h)

1
2
const RectangleArea = base => (height => (base * height))
RectangleArea(2)(4)

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

定义数据类型

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

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

Alonzo Church 这样定义布尔类型:

1
2
true = λa. (λb.a) \quad
false = λa. (λb.b)

1
2
const True = a => b => a
const False = a => b => b

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

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

1
if = λp.(λa. (λb. p a b))

1
const If = Condition => Then => Else => Condition(Then)(Else)

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

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

1
2
const isTrue = () => "it's true!"
const isFalse = () => "it's false!"

将布尔值传进If

1
2
3
4
const First = If(True)(isTrue)(isFalse)
const Second = If(False)(isTrue)(isFalse)
First() // "it's true!"
Second() // "it's false!"

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

1
if true = λp.(λa.(λb. p a b)) true = p[p := true] = true a b = λa.(λb.a) a b = a

1
if false = λp.(λa.(λb. p a b)) false = p[p := false] = false a b = λa.(λb.b) a b = b

在了解了If的定义之后,再看看andor的定义:

1
2
and = λp.(λq. p q p)
or = λp.(λq. p p q)

1
2
const And = Exp1 => Exp2 => Exp1(Exp2)(Exp1)
const Or = Exp1 => Exp2 => Exp1(Exp1)(Exp2)

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

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

1
and true false = λp.(λq. p q p) true false = p[p := true] = q[q := false] = true false true = λa.(λb. a) false true = false

1
...
1
or true false = λp.(λq. p p q) true false = p[p := true] = q[q := false] = true true false = λa.(λb. a) true false = true
1
...

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

Operator Reduction Result
And(True)(True) True(True)(True) True
And(True)(False) True(False)(True) False
And(False)(True) False(True)(False) False
And(False)(False) False(False)(False) False
Or(True)(True) True(True)(True) True
Or(True)(False) True(True)(False) True
Or(False)(True) False(False)(True) True
Or(False)(False) False(False)(False) False

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

1
2
3
4
5
6
7
8
const Result1 = If(And(True)(True))(isTrue)(isFalse)
const Result2 = If(And(True)(False))(isTrue)(isFalse)
const Result3 = If(Or(False)(True))(isTrue)(isFalse)
const Result4 = If(Or(False)(False))(isTrue)(isFalse)
Result1() // "it's true"
Result2() // "it's false"
Result3() // "it's true"
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 .

0%