fixpoint

recursive function construct

fun f x. e = valid expr in λ-calculus syntatic sugar

eq m n = true or false

fac = fun f n. if eq n 0 then 1 else mult n (f (pred n))

FAC = λf.λn. if eq n 0 then 1 else mult n (f (pred n))

f: partial impl of factorial 3×2×1 f(3) f(2) f(1)

FAC: improved impl of factorial

give me f(3)

n = 4 f (pred 4) = f(3) f(4)

FAC f(3) -> f(4)

FAC = λf.λn. if eq n 0 then 1 else mult n (f (pred n)) fac₀ = FAC (λn. omega) ——- 1 fac₁ = FAC (FAC (λn. omega)) ——- 2 × 1 fac₂ = FAC³ λn. omega ——- 3 × 2 × 1 ... facₙ = FAC n+1 λn. omega

suppose fac = correct impl of factorial fac ~= FAC fac = correct impl of factorial

    fac is a fixed point of FAC

    f(x) = x
    f(x) = 2 - x  f(1) = 2 - 1 = 1

fixed point combinator: fix takes F, returns a fixed point of F.

fac = fix(FAC) FAC(fix(FAC)) = fix(FAC)