λ-演算中的范式与求值策略

1. 范式的基本概念
   在λ-演算中，范式是指无法继续进行β归约的λ项。具体分为两类：

   • 正规形式：不含任何β可约式（即形如(λx.M)N的子项）。例如，λx.x是范式。
   • 头正规形式：形如λx₁.λx₂.…λxₙ. y M₁…Mₘ（其中y可为变量或更复杂的项），且所有Mᵢ也是头正规形式。
     注意：所有正规形式都是头正规形式，但反之不成立（例如λy. (λx.x) z是头正规形式但不是正规形式）。

2. 范式的存在性与唯一性

   • 若项存在范式，则在α-等价意义下唯一（由Church-Rosser定理保证）。
   • 并非所有项都有范式，例如(λx.xx)(λx.xx)会无限归约。

3. 求值策略的分类
   求值策略决定β归约的触发顺序，主要分为两类：

   • 严格策略：在函数应用前先对参数求值。包括：
     • 按值调用：仅当参数为值（变量或抽象）时归约。例如(λx.M)(λy.N)先计算参数(λy.N)。
     • 按名调用：允许参数为非值，但禁止在抽象内部归约。
   • 非严格策略：允许未求值的参数直接代入函数体。包括：
     • 按需调用（Haskell采用）：延迟参数求值，且共享重复计算。

4. 策略的数学描述
   以按值调用为例，其归约规则为：

   M → M'  
   -------------  
   M N → M' N  
   

   N → N'  
   -------------  
   V N → V N'  (V为值)  
   

   (λx.M) V → M[V/x]  
   

   按需调用则通过闭包技术实现，将未求值参数包装为悬吊计算。

5. 策略与终止性的关系

   • 若按需调用能终止，则按值调用必然终止（反之不成立）。
   • 经典例子：(λx.λy.y) Ω（其中Ω为发散项）在按需调用下得到范式λy.y，而按值调用会陷入无限循环。

6. 实现与扩展

   • 实际语言常混合多种策略（如OCaml的按值调用+惰性数据结构）。
   • 形式化分析工具（如操作语义机器）可通过标记求值上下文精确描述策略差异。