变量 Variable

代表一个输入值，即实参 (arguments)

  • 形如 $x,y,z$

抽象 Abstraction

相当于定义一个函数，并规定输入量，其本身就代表一个函数

  • 形如 $\lambda{x}.M$ ，其中 $\lambda$ 是一个函数定义符，它代表一个函数定义的起点
  • $M$ 即为函数体，而 $x$ 即为形参 (parameters)
  • $M$ 即为返回的值

应用 Application

相当于对函数的调用，其本身输出一个变量

  • 形如 $(M N)$，表示将 $M$ 应用于 $N$ ，即 $N \rightarrow M$
  • 当然，这个括号不是必须的，总之就是后者应用于前者

[!attention] 你需要搞清楚的是，以上三种东西其实都可以作为一个函数存在，即自然数也被定义为了函数、自然数也是有参数和返回值的函数，在Lambda演算中，所有东西都必须是函数。 当然，我们这里说的“函数”也并非lambda演算的内容，这是为了方便理解所引入的概念 数学语言里描述的种种东西，在lambda演算中都有自己的表达方式，但首先，让我们了解它的基本运算规则

β归约 $\beta\ reduction$

这个过程其实相当好理解，我们有了形参 parameters和实参 arguments，那么就完全可以把实参带入到形参的位置，这就是β-规约 (β-reduction)。比如下面这个例子 \(\lambda x.(xb)E\) 注意到这个和上面的Application的模板一样，即$M=\lambda x.(xb)$ $N=E$ β规约后，我们得到了 \(\lambda x.(xb)E\rightarrow_\beta Eb\) $λ$的存在就指定了$N$应该替换的部分，在这个例子里，是$\lambda x.$指定了形参$x$。所以你就将$N$，这里是$E$，代入进去，并去掉函数的定义部分

另外，当一个式子被β规约到无法继续规约了，我们称其为β标准型 β Normal Form

多参数输入 / 柯里化 Currying

可见，Application这个模板里只允许一个形参的定义和一个实参的传入，那么多参数的传入就需要嵌套了 \((\lambda x.(\lambda y.x)Y)X\) 上面这个演算所实现的功能是输入两个值，只返回前者，在这里为$X$。我们进行两次β规约，则有 \(\displaylines{ (\lambda y.X)Y\\ X }\) 这个过程被我们称作柯里化 Currying。我们之后就直接在 $\lambda$ 和 $.$ 中允许多个变量的存在，以方便观看和阅读

η等价 $\eta-equivalence$

这个是视频里没有讲的，我是通过问AI才问出来的

定义: 如果一个函数$F$对任意一个输入$x$都有$F\ x=G\ x$，那么可以认为$F$与$G$是等价的，写作 \(F =_{\eta}G\)

例如函数 $F:=λx.M x$，对于任意参数$y$都有$F y=(λx.M x) y→β​M y$ 所以我们说$F ={\eta}M$ 也就是说，形如上面这种的基本都可以把$x$省略掉

这也很大程度解释了[[2025-12-20-Lambda - 3 自然数定义#幂运算]]中我的疑惑

[[2025-12-20-Lambda - 2 逻辑符号定义]]