「Learn LambdaCalculus」#0

前言

前段时间,GZTime也跟我聊过一些关于lambda演算的东西
学Haskell的时候也总是能听说这个东西
看起来挺有意思,来学学_(:з」∠)_

那我也引用GZTime引用的知乎同学的一句话:

在介绍λ演算之前,我们需要放空一下我们的大脑,忘掉C语言,忘掉冯·诺伊曼机,忘掉图灵机,甚至要忘掉0和1,加和减。我们来到一个只有符号的世界。在这个新的世界里,只需要几条简单的定义和规则,便可以构造出与图灵机完全等价的计算模型,即它是图灵完全(Turing Complete)的。和图灵机一样,这个计算模型可以解决任何一个可以机械计算的问题;与图灵机倾向于硬件实现不同,它更倾向于逻辑的推理。它就是λ演算(Lambda演算)。

lambda term

一个合法的lambda表达式又被称为lambda项(lambda term),以下三个规律归纳性地定义了一个合法的lambda项:

  • Variable:一个变量 x 本身也是一个合法的lambda项
  • Abstraction:如果 M 是一个合法的lambda项,x 是一个变量,那么 (λx.M) 也是一个合法的lambda项(这相当于定义了一个 x -> M 的函数)
  • Application:如果 M 和 N 都是合法lambda项,那么 (M N) 也是一个合法lambda项

lambda表达式的组成有变量、抽象符号λ和一个点.、括号

所有lambda项构成$\Lambda$空间,通过上述合法lambda项的定义,$\Lambda$空间的正式定义是:

  • 如果$x$是一个变量,那么$x\in\Lambda$
  • 如果$x$是一个变量且$M\in\Lambda$,那么$(\lambda x.M)\in\Lambda$
  • 如果$M, N\in\Lambda$,那么$(M\ N)\in\Lambda$

notation

为了使lambda表达式的记法更清晰,可以有以下简化:

  • 一个lambda项最外侧的括号可以省略。比如 (M N) 可以写成 M N
  • 应用是左结合的。比如 M N P 表示的实际是 ((M N) P)
    这和Haskell中函数左结合是一样的
  • 抽象是尽可能向右延伸的。比如 λx.M N 实际上表示的是 λx.(M N) 而不是 (λ. M) N
    这和Haskell中lambda表达式向右一直延伸是一致的,因此一般要为lambda表达式加上括号
  • 嵌套的多个lambda表达式可以缩写成类似多元函数的样子。比如 λx.λy.λz.M 就可以缩写成 λxyz.M

Free & bound variables

在一个lambda表达式中,也有自由变量(free variables)和约束变量(bound variables)的概念。

在lambda项 λx.M 中,λx被称为binder,它将输入的x与M中的变量x绑定在一起,这时x就是约束变量,而其它的所有变量都是自由变量。

 比如在表达式 λx.x+y 中,x就是约束变量,y是自由变量。

对于一个lambda项M的自由变量构成的集合FV(M),也有一些规律需要满足:

  • 如果 x 是一个变量,那么 FV(x) = {x}
  • FV(λx.M) = FV(M) \ {x} (M中除去x之外的变量都是自由变量)
  • FV(M N) = FV(M) ∪ FV(N) (M应用在N上得到的lambda项的自由变量是MN两个lambda项的自由变量的并集)

Substitution

lambda项也有一种记法叫做替换(substitution),记法 t[x:=r] 表示将lambda项t中的自由变量x都替换成r。它满足以下规律:

  • x[x:=r]=r (一个变量就是自由变量,将其替换成r就变为r)
  • y[x:=r]=y if x!=y (如果x和y不相等,那么)

「Learn LambdaCalculus」#0

https://blog.tonycrane.cc/p/92a6fc79.html

作者

TonyCrane

发布于

2021-08-04

更新于

2021-08-23

许可协议

评论