函数抽象与λ表达式，如何从零开始？
摘要：tags: - 函数式编程 - 数学 - λ演算 目录抽象抽象点函数抽象λ表达式 | λ项表达式的构成命名函数运用约束变量与自由变量归约 | 消解α转换 | α换名β归约η归约DEF原语 | 定义命名特殊的λ表达式恒等函数运用函数自运用函数
目录抽象抽象点函数抽象λ表达式 | λ项表达式的构成命名函数运用约束变量与自由变量归约 | 消解α转换 | α换名β归约η归约DEF原语 | 定义命名特殊的λ表达式恒等函数运用函数自运用函数
⚠ 本文导出自Obsidian，可能存在格式偏差（例如链接等）
本文地址：https://www.cnblogs.com/oberon-zjt0806/p/18708237
λ演算（λ Calculus）是函数式编程中的基础。在函数式编程中，λ演算是构成函数（尤其是复合函数）的重要方式。
抽象
对于一个具体的问题——
❓ 例
买了4支笔，每支3元，求花了多少钱？
当然，这个问题相当容易，我们只需要计算
4 * 3 = 12
抽象点
那么5支笔呢？6支笔呢？于是我们重新计算，发现只需要把4相应的改成5和6，就可以解决了，那么其他的情况呢？于是我们用一个变量来替换掉4的位置。
num * 3
刚才我们恰好完成了一个抽象的过程，我们把一个变数装入了变量中，并使用符号来描述这个变量。在这步抽象中，我们不再关心购买的数量具体是多少，我们知道只要给出明确的num，我们就能求出最后的价格。此时，num不仅仅代表一个变量，同时也叫做一个抽象点。
类似地，如果单价发生变动时，我们也可以做出类似的抽象，使用另一个变量替换掉3，至此我们引入了第二个抽象点。
num * price
于是我们形成了一个关于num和price的抽象表达式，现在只要给出具体的num和price，我就能求出具体的总花销了。
在计算时，我们使用原语 LET ... IN ... 将抽象点替换为具体的内容，这里LET ... IN ...原语被定义为：LET子句替换一个抽象点为具体内容，并将其代入IN子句的内容，得到的是被替换后的表达式。例如——
LET num = 5 IN num * price
=> 5 * price
LET price = 8 IN LET num = 5 IN num * price
=> LET price = 8 IN 5 * price
=> 5 * 8 => 40
至此我们也可以说，我们通过抽象的方式，构建了一个关于num和price的函数。
函数抽象
刚才我们完成了两个变量的抽象。然而，抽象点并不限于数值变量，运算本身也可以作为抽象点。
💡 运算也是函数
而我们都知道一个运算本身就是一个函数，比如一个二元运算实际上就是一个二元函数，因此对运算的抽象，本质上也是对函数的抽象
我们刚刚获得了形如这样的表达式：
a * b
现在假设我们在做一个二元的计算器，支持a与b的四则运算，显然上面的表达式不能完全满足我们的需求，因为上面的表达式只能计算乘法。
a + b
a - b
a * b
a / b
^
至此，除了a和b这两个抽象点外，我们发现了第三个抽象点——*也可以被抽象。于是我们引入符号 op 来抽象中间的运算符——
a op b
op也同样是一个抽象点，因此我们也可以使用LET ... IN ...原语来替换op
LET op = + IN (LET a = 5 IN (LET b = 7 IN a op b))
=> LET op = + IN (LET a = 5 IN a op 7)
=> LET op = + IN (5 op 7)
=> 5 + 7 => 12
a、b、op是我们引入的抽象符号，称为命名。
❓ 更进一步地……
难道LET ... IN ... 原语就不能被抽象吗？
^c84638
λ表达式 | λ项
在先前的表达式中，我们几乎把所有东西都抽象为抽象点。随着表达式愈发的复杂，抽象点开始变得越来越多，我们迫切地需要一种统一化的语言来管理这些抽象点以及它们之间的联系。
Alonzo Church在20世纪30年代引入了λ演算系统，通过统一地，数学化地方式来描述这些函数抽象，基于该演算系统下用来描述这些抽象的定式就是λ表达式（λ Expression）。
表达式的构成
λ表达式可以下列三者任一个
命名 <name>
函数 <func>
运用 <app>
用巴科斯范式（BNF）表述为——
<expr> ::= <name>|<func>|<app>
命名
λ系统下的命名就是我们刚刚提及的抽象符号，由一串非空白的字符序列构成。
a
berry
everYthinG
15
+
*
->
以上这些都是可以使用的命名。
函数
λ表达式允许是一段函数定义，这也是λ表达式举足关键的存在。λ系统中的函数形式被定义为——
<func> ::= λ<name>.<body>
<body> ::= <expr>
其中，<name>依旧是刚才提到的命名，<body>部分称为函数体，包含了这个函数的定义。而这个定义本身又是一个λ表达式。这个形式的出现意味着λ表达式可以递归地嵌套。这也提供了让各个函数相互组合的机会，从而能够形成复杂的表达式结构。
具体一个函数如何定义，我们以数学中的函数为例：\(f(x) = x+1\)，在λ表达式中表示为
λx.x+1
-- or much more functional --
λx.(+ x 1)
其中λ 算子引领一个命名，被引领的命名λ<name>被称为约束变量（Bound Variable）。约束变量与函数体之间用约束符.分隔开。整体表述为约束变量<name>被约束到<body>上。
❗ 约束满足右结合律
原则上来说，函数的原子定义（即最小定义）的形式中，仅包含一个λ算子和约束符.，在约束后形成的表达式中可以继续使用λ算子进行约束
λa.(λb.(λc.(...)))
可以发现，.约束满足右结合律，因此在符合这个顺序的前提下，括号通常可以省略
λa.λb.λc.(...) <=> λa.(λb.(λc.(...)))
在某些情况下，如果已知全体约束变量都只由一个字符命名，在不引起冲突的情况下，可以约定一种更为简洁的记法 （由于本文中可能出现多字符的命名，因此会规避这种写法） ——
λ(a,b,c).(...) <=> λabc.(...) <=> λa.(λb.(λc.(...)))
^3bba62
运用
命名和函数都尚且停留在抽象层面，是声明性的成分，而运用就像LET ... IN ...原语一样，要替换掉函数中的抽象点。回答上面的[[#^c84638|思考]]，运用本身在某种意义上很像是对LET ... IN ...的抽象（但还并不完全是）。
在程序设计中，运用也叫做调用（Call）。运用的形式如下——
<app> ::= (<func> :: <expr>)
还是上面的例子，我们对5运用函数，就可以写作
(λx.(+ x 1) 5)
左边是要运用的函数，右边是运用的目标表达式。由这两个构成的运用由括号包裹起来，构成一对，因此函数的运用形成的表达式也被称为约束对（Bound Pairs）。
❗ 运用满足左结合律
与函数约束类似，运用的原子定义的形式中，仅包含一个函数和表达式，约束对也是体现了这种一一对应的关系，在运用后形成的表达式中可以继续进行运用，假设f是一个已知函数
(((f a) b) c)
与约束符相反，可以发现，运用符(* *)约束满足左结合律，因此在符合这个顺序的前提下，括号通常可以省略
(f a b c) <=> (((f a) b) c)
特殊地，如果约束对在最外层，那么最外层的括号也可以省略
f a b c <=>(f a b c) <=> (((f a) b) c)
^887c32
约束变量与自由变量
考虑如下表达式（每个命名均为首次定义）——
λx.(x y)
在[[#函数]]定义中，λ算子规定了x是这个函数的约束变量，但在函数体中y并没有被任何算子约束。此时称y为自由变量。
如果没有提供任何λ约束，那么表达式所有出现的命名都是自由变量——
例如对于单一的命名x，则x本身为自由变量。
对于运用式(f x)，f和x均为自由变量。
归约 | 消解
回到这个例子上来
LET op = + IN (LET a = 5 IN (LET b = 7 IN a op b))
现在我们可以通过λ表达式的写法来改写上面的LET ... IN ...原语（清晰起见，这里不省略括号）
(λop.(λa.(λb.(op a b) 7) 5) +)
然而这样的记法依旧冗长，在约束变量被确定下来时，我们可以实现进行一些消解来对原式化简，得到更简单的λ表达式，这个消解过程称为归约（Reduction）。归约前后的λ表达式在计算上的结果是等同的。
引入=>记号表示归约过程，记号左侧是归约前的表达式，右侧是归约后的表达式。例如——
(λx.(+ x 1) 5) => + 5 1
α转换 | α换名
先介绍一下α转换，所谓α转换是指，当约束变量被约束到函数体时，在不引发冲突的前提下，约束变量和所约束的函数体中的的命名同步变化后，表达式等价。
例如下面这几个函数都是等同的
λx.x <=> λa.a <=> λbalabala.balabala
严格来说，α转换并没有使表达式精简，它的出现主要说明一件事——函数的定义与约束变量的命名无关。重命名前后，始终是同一个函数。这种关系可以也叫做α等价。
ℹ
α转换通常用于解决λ表达式中的命名冲突问题
β归约
所谓β归约，就是指当遇到约束对(f a)时，通过替换行为将f中的约束变量替换为a
(λx.(+ x 1) 5) => + 5 1
比如对于上面的例子——
(λop.(λa.(λb.(op a b) 7) 5) +)
=> (λop.(λa.(op a 7) 5) +)
=> (λop.(op 5 7) +)
=> + 5 7
可以发现通过β归约对约束对逐步替换，使原本冗长的表达式变成了最终的+ 5 7。β归约的最终形式称为β范形（β-normal form）。
⚠ 注意
有些表达式可能无法归约为β范形。因为它们可以无限地进行β归约。
例如：[[#自运用函数]]
η归约
由于我们没有规定函数定义中，函数体一定要包含约束变量，例如λx.A，如果命名A的定义中不包含任何关于x的约束，那么意味着A与x无关（或者说A是一个自由变量/表达式），在这种情况下，如果对这个函数运用任何实参(λx.A x)，实际上不会替换A中任何内容，此时可发生η归约——
(λx.A x) => A
η归约通常用于清理无关约束。
DEF原语 | 定义命名
归约主要是对表达式本身进行简化，其简化结果依然是一个λ表达式。而如果这个表达式反复出现多次，写起来依旧很繁杂，不够直观。
更直接的办法是将λ表达式装入一个不冲突的命名中，引入DEF原语——
DEF <name> = <expression>
这样一来，任何出现<expression>的地方都可以用<name>表示。例如
DEF plus = λa.λb.(+ a b)
plus 5 7
⚠ DEF vs LET
需要注意的是，DEF原语与LET原语不同的关键在于，DEF原语是在定义表达式的命名替换，也就是给一个表达式起了个名字，定义之后不可重复定义，而LET原语根据我们刚刚了解到的，实际上是在执行表达式的替换运用，或者更进一步的说，是在进行β归约。也就是说，可以对表达式做出多次LET，而对一个命名而言，只能DEF一次（但同一个表达式可以DEF给不同的命名）。
DEF a = (λx.x x)
DEF a = (λx.(+ x 1)) --->> × Redefinition to a is not allowed
特殊的λ表达式
恒等函数
DEF identity = λx.x
所谓恒等函数，顾名思义，函数体与输入是相同的。这一点可以给出恒等变换的运用约束对时，进行β归约得到体现。
identity a => a
运用函数
DEF call = λf.λx.(f x)
运用函数显而易见，接收一个函数和一个参数，然后对两者构建一个[[#运用|约束对]]，也就是执行运用。
❓ 思考
既然有约束对的存在，为什么还要引入运用函数？
回想前面提到的[[#函数抽象]]，结合运用函数的定义，我们就会发现，运用函数中对约束对的函数进行了抽象，使之成为了一个约束变量。
call sind 30
=> sind 30
自运用函数
DEF self_call = λs.(s s)
在此考虑一个情况，函数本身是一个λ表达式，对于函数的运用也是一个λ表达式，而运用函数的参数也是λ表达式……如果这三个表达式都是同一个，会是什么样的局面。
这就是自运用函数。例如，我们对恒等函数进行自运用——
self_call identity
=> (λs.(s s) λx.x)
=> (λx.x λx.x)
=> λx.x
进行β归约我们发现，实际上就可以解释为“对恒等函数应用恒等函数”，我们记得恒等函数的输入和输出是相同的，所以输出的依然是恒等函数。
那如果我们对自运用函数自身使用自运用呢？前方高能——
self_call self_call
=> (λs.(s s) λs.(s s))
=> (λs.(s s) λs.(s s))
=> ...
归约结果可以继续归约，并且无论如何继续，还依然原来的形式，这意味着可以无限归约。
记住这个性质，后面有用。