Lambda演算是Alonzo Church在1930年代开发的框架，用于研究具有函数的计算。

• 函数创建-Church引入了符号λx.E来表示一个函数，其中“ x”是形式参数，而“ E”是功能体。这些函数可以不带名称和单个参数。

• 函数应用程序-Church使用符号E ₁ .E ₂表示函数E ₁在实际参数E _{2上的应用}。并且所有功能都在单个参数上。

Lambda微积分的语法

Lamdba演算包含三种不同类型的表达式，即

E :: = x (变量)

| E ₁ E ₂ (函数应用程序)

| λx.E (函数创建)

其中λx.E称为Lambda抽象，E称为λ表达式。

评估Lambda微积分

纯lambda演算没有内置函数。让我们评估以下表达式-

(+ (* 5 6) (* 8 3)) 

在这里，我们不能以“ +”开头，因为它仅对数字起作用。有两个可简化表达式：(* 5 6)和(* 8 3)。

我们可以先减少一个。例如-

(+ (* 5 6) (* 8 3)) 
(+ 30 (* 8 3)) 
(+ 30 24) 
= 54

β还原法则

我们需要一个减少规则来处理λs

(λx . * 2 x) 4 
(* 2 4) 
= 8

这称为β-还原。

形式参数可以多次使用-

(λx . + x x) 4 
(+ 4 4) 
= 8

当存在多个术语时，我们可以按以下方式处理它们-

(λx . (λx . + (− x 1)) x 3) 9 

内部x属于内部λ ，外部x属于外部λ 。

(λx . + (− x 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
= 11

自由和绑定变量

在表达式中，变量的每个出现都是“自由”(对λ)或“绑定”(对λ)。

(λx。E) y的β折减将在E中自由出现的每个x替换为y 。例如-

减少Alpha

Alpha还原非常简单，无需更改lambda表达式的含义即可完成。

λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x) 

例如-

(λx . (λx . + (− x 1)) x 3) 9 
(λx . (λy . + (− y 1)) x 3) 9 
(λy . + (− y 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
11 

丘奇-罗斯定理

Church-Rosser定理指出以下内容-

• 如果E1↔E2，则存在一个E，使得E1→E和E2→E。“以任何方式进行归约最终都可以产生相同的结果。”

• 如果E1→E2，并且E2是正规形式，则E1到E2的正规阶归约。 “如果存在法线降阶，将总是产生一种法线形式。”