函数抽象与λ表达式，如何从零开始？

目录抽象抽象点函数抽象λ表达式 | λ项表达式的构成命名函数运用约束变量与自由变量归约 | 消解α转换 | α换名β归约η归约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 + * -> 以上这些都是可以使用的命名。 函数 λ表达式允许是一段函数定义，这也是λ表达式举足关键的存在。