请解析λ演算中的简单算子释义及Wadler论文中的相关规则

Hey there, let's break this down step by step—first covering some foundational λ-calculus operators, then diving into the core syntactic and reduction rules from Phillip Wadler's 1994 paper Monads and composable continuations that you asked about.

Here are a few simple, ubiquitous λ-calculus operators with plain-English explanations:

• Identity combinator (I): Defined as λx.x. This is the simplest function you can write—it takes any input and spits it back out exactly as-is. Think of it as a "pass-through" operator that does nothing but preserve values.
• K combinator (Constant function): λx.λy.x. This takes two arguments, completely ignores the second one, and returns the first. It's handy for creating functions that always return a fixed value, no matter what you feed them next.
• Pair operator: λx.λy.λf.f x y. This wraps two values into a single "pair" structure. To extract the first element, you apply the pair to λa.λb.a; to get the second, use λa.λb.b.
• Boolean operators:
  • true = λx.λy.x (chooses the first of two arguments)
  • false = λx.λy.y (chooses the second of two arguments)
    These aren't just values—they're functions that encode boolean logic directly through argument selection.

Wadler frames these constructs as syntactic sugar that maps directly to pure λ-calculus terms, with clear reduction rules. Let's break each one down:

1. Addition (d + e) #

Arithmetic operations like addition are shorthand for applying a primitive addition function to two terms. The formal translation is:

d + e ≡ (+ d e)
Where + is a primitive λ-term that takes two numeric arguments and returns their sum. The reduction rule follows standard function application: if d evaluates to numeral n and e evaluates to m, d + e reduces to the numeral representing n + m.

2. Conditional (if c then d else e) #

This uses the λ-calculus boolean definitions we covered earlier. The conditional is just syntactic sugar for applying the boolean term c to d and e:

if c then d else e ≡ c d e
Semantically, if c reduces to true, the whole term evaluates to d; if c reduces to false, it evaluates to e. This is exactly how λ-calculus booleans work—they're functions that select between two options.

3. Let Binding (let x = d in e) #

Let bindings let us create temporary variables or avoid repeating terms, and they're just shorthand for anonymous function application:

let x = d in e ≡ (λx.e) d
Here's what happens: we define an anonymous function that takes x and returns e, then immediately apply that function to d. This safely substitutes d for every free occurrence of x in e (following λ-calculus substitution rules to avoid variable capture). For example, let x = 5 in x + 3 becomes (λx.x + 3) 5, which reduces to 8.

4. Recursive Let Binding (letrec) #

Regular let can't handle recursive definitions because the variable isn't in scope when defining the term. letrec fixes this using the fixed-point combinator (Y), the standard way to express recursion in pure λ-calculus. The Y combinator is defined as:
Y = λf.(λx.f (x x)) (λx.f (x x))
Its key property is Y f = f (Y f)—it generates the fixed point of f, which lets functions refer to themselves.

Wadler's translation rule for letrec is:

letrec x = d in e ≡ (λx.e) (Y (λx.d))
Breaking this down: we first use Y to create a recursive version of d (so x refers to itself in d), then substitute that recursive term into e using the same pattern as regular let. For example, a recursive factorial function defined with letrec gets translated to use Y to enable the function to call itself.

内容的提问来源于stack exchange，提问作者user65526