Efficient Reduction Functions in Coq

Bruno Barras INRIA-Rocquencourt

June, 18^{th}, 1998

Plan

1. Motivations

2. Definitions

3. Naive Attempt

4. Abstract Machine (KAM)

5. Substitution Calculus

1. Coq and Reduction

1 Coq and Reduction

Programs: βδι-reduction Type system: polymorphism, dependent types

• Dependent types:

Array : nat → Set
| 17 42 5 | : Array(3) : Set
T_{1} : Array(2 + 1)
T_{2} : Array(\sqrt{9})

T_{1} = T_{2} well-typed ? Array(2 + 1) ≡^{?} Array(\sqrt{9})

1. Coq and Reduction

• Proof by reflection:

(a + b)(a − b) = a^{2} − b^{2}
a(a − b) + b(a − b) = a^{2} − b^{2}
a^{2} − ab + (ba − b^{2}) = a^{2} − b^{2}
a^{2} − b^{2} = a^{2} − b^{2}

Define F such that

– F ((X + Y)(X − Y)) =_{βδι} X^{2} − Y^{2} – ∀a, b, P. F (P)(a, b) = P (a, b)

2. Definitions

2 Definitions

Pure λ-calculus

De Bruijn notation:

t := n (n ∈ IN) | λt | (t t′)

Example:

λu.(λx.(x λy.x) (λz.z u)) λ_{u}(λ_{x}(0_{x} λ_{y}1_{x}) (λ_{z}0_{z} 0_{u}))

β-reduction:

(λm n) → {n/0}m

Goal: compute β (head) normal form

2. Definitions

Coq’s encoding of terms

• λ is used as a binder

• ( ) bears a tag. Typed λ-calculus:

λx:T. M ≡ Lambda_{x}(T λM)
(M N) ≡ AppL(M N)

New β rule:

AppL(Lambda_{x}(T λM) N) → {N/0}M

2. Definitions

Strategies

Call by value (ML) Weak normal form of argument first

(λx.(x + x) (ˆ1 + ˆ1))

→_{ι} (λx.(x + x) ˆ2)
→_{β} ˆ2 + ˆ2
→_{ι} ˆ4

+ Avoid duplication of redexes − Useless computations ⇒ Faster on functional programs

2. Definitions

Call by name Leftmost outermost first

(λx.(x + x) (ˆ1 + ˆ1))

→_{β} (ˆ1 + ˆ1) + (ˆ1 + ˆ1)
→_{ι} ˆ2 + (ˆ1 + ˆ1)
→_{ι} ˆ2 + ˆ2
→_{ι} ˆ4

+ Laziness − Redundant computations ⇒ Better for proof normalisation

2. Definitions

Lazy (LML) Call by name with sharing

(λx.(x + x) (ˆ1 + ˆ1))

→_{β} (\underline{ˆ1 + ˆ1}) + (\underline{ˆ1 + ˆ1})
→_{ι} ˆ2 + ˆ2
→_{ι} ˆ4

+ Number of reduction steps < CBV, CBN − Overhead (updates) ⇒ Good trade-off

3. First implementation

3 First implementation

let rec norm = function
  Rel i    -> Rel i
| Lam t    -> Lam (norm t)
| App(a,b) -> (match (norm a) with
                 Lam f -> norm (subst b f)
               | na -> App(na, norm b))
let rec nrm_whd = function
  (App(a,b), s)   -> nrm_whd (a, (b::s))
| (Lam f, (b::s)) -> nrm_whd (subst b f, s)
| (Lam t, [])     -> Lam (whdn t)
| (Rel i, s)      -> app_list (Rel i) (List.map whdn s)
and whdn t = nrm_whd (t,[])

Quadratic factor O(n) substitutions in terms of size O(n)

Memory allocation

(λ_{x}λ_{y}(\overbrace{… 1_{x} … λλ … 2_{y} … 3_{x} …}^{M}) T_{1} T_{2})

(λ_{y}(… ↑^{1}T_{1} … λλ … 2_{y} … ↑^{3}T_{1} …) T_{2}) (… T_{1} … λλ … ↑^{2}T_{2} … ↑^{2}T_{1} …)

2 substitutions:

• M re-allocated twice

• T_{1} re-allocated 4 times

• T_{2} re-allocated once

3. First implementation

Parallel substitution

(λ_{x}λ_{y}(\overbrace{… 1_{x} … λλ … 2_{y} … 3_{x} …}^{M}) T_{1} T_{2})

({T_{1}/0_{x}}λ_{y}M T_{2})

{T_{1}/1_{x}; T_{2}/0_{y}}M

(… T_{1} … {T_{1}/1_{x}; T_{2}/0_{y}}λλ … 2_{y} … 3_{x} …)

(… T_{1} … λλ … ↑^{2}T_{2} … ↑^{2}T_{1} …)

• M, T_{1}, T_{2} re-allocated once Closure = delayed substitution Environment = parallel substitution

C := ⟨E, t⟩ E := C⃗

• In CBN, arguments are frozen

• In CBV, partial application

4. Krivine’s Abstract Machine

4 Krivine’s Abstract Machine

State: (e, t, s) ∈ E × t × C⃗ Initial: ([ ], t, [ ]) Transitions:

\begin{matrix}(e, (u v), s) → & (e, u, ⟨e, v⟩ :: s) \\ (e, λt, c :: s) → & (c :: e, t, s) \\ (⟨e′, v⟩ :: e, 0, s) → & (e′, v, s) \\ (c :: e, n + 1, s) → & (e, n, s) \end{matrix}

Computes weak head normal form (CBN)

KAM under abstractions (KN, Crégut 91)

type clos = Clos of env * lambda
 and env  = clos list
let rec kn k = function
  (e, App(a,b), s)      -> kn k (e, a, (Clos(e,b)::s))
| (e, Lam f, (arg::s))  -> kn k ((arg::e), f, s)
| (((Clos(e',u))::_), Rel 0, s) -> kn k (e', u, s)
| ((_::e), Rel n, s)    -> kn k (e, Rel (n-1), s)
| (e, Lam f, [])        ->
    Lam (kn (k+1) (((Clos([], Rel (-k-1)))::e), f, []))
| ([], Rel n, s)        ->
    app_list (Rel (k+n))
      (List.map (fun (Clos(e,t)) -> kn k (e,t,[])) s)

succ = λλλ(1 (2 1 0))

(A, B) = λ(0 ↑^{1}A ↑^{1}B)

pred = λ(0 λ(succ (0 λλ1), 0 λλ1) (ˆ0, ˆ0) λλ0)

(pred n̂) Tnorm Twhdn Tkn TOCaml

10  0.3 0.02
14  5
15  9
16  19
50  0.6 0.005
100  3.3 0.01 0.0004
200  19 0.021
1000  0.14 0.005
O(2^{n}) O(n^{2}) O(n)  O(n)

5. Explicit Substitutions

5 Explicit Substitutions

Why ?

• Closer to the implementation

• Correctness proof Closure Calculus Mutable terms with shifts:

T := n̄ (n ∈ IN) | λ_{⟨S,t⟩}T | (T T′) |↑^{n}T | [S]t Substitution (cf λϕ, in Lescanne 93)

S := id | S. T |↑^{n}S |⇑^{n}S

5. Explicit Substitutions

Sharing

λu.(\underline{λx}.(x λy.x) (\underline{λz.z u}))

→ λu.(\underline{λz.z u} λy.(\underline{λz.z u}))
→ λu.(\underline{u} λy.\underline{u})

De Bruijn:

\begin{aligned}& λ_{u}(\underline{λ_{x}}(0_{x} λ_{y}1_{x}) (\underline{λ_{z}0_{z} 0_{u}})) \\ → & λ_{u}(\underline{λ_{z}0_{z} 0_{u}} λ_{y}(\underline{λ_{z}0_{z} 1_{u}}))) \end{aligned}

Explicit shift:

\begin{matrix}→ & λ_{u}(\underline{λ_{z}0_{z} 0_{u}} λ_{y} ↑^{1}(\underline{λ_{z}0_{z} 0_{u}})) \\ → & λ_{u}(\underline{0_{u}} λ_{y} ↑^{1}\underline{0_{u}}) \end{matrix}

5. Explicit Substitutions

Weak reduction or not ?

let rec pow2 = function
  0 -> 1
| n -> let x = pow2 (n-1) in x+x
let rec pow2 = function
  0 -> 1
| n -> (pow2 (n-1))+(pow2 (n-1))

\begin{aligned}& (λf.λx.(x f f (f x)) λy.M) \\ → & λx.(x λy.nf(M) λy.nf(M) \{x/y\} M) \end{aligned}

⇒ 2 usages for f

5. Explicit Substitutions

Reduction Rules

Substitution:

\begin{matrix}[S](u v) → & ([S]u [S]v) \\ [S]λt → & λ_{⟨S,t⟩} [⇑^{1}S]t \\ [id]n → & n̄ \\ [S. T]0 → & T \\ [S. T](n + 1) → & [S]n \\ [↑^{k}S]n → & ↑^{k}[S]n \\ [⇑^{k}S]n → & n̄ if n < k \\ [⇑^{k}S]n → & ↑^{k}[S](n − k) if n ≥ k \end{matrix}

Confluent and terminates (no composition) Beta:

\begin{matrix}(λ_{⟨S,m⟩}T N) → & [S. N]m \\ (↑^{k}λ_{⟨S,m⟩}T N) → & [↑^{k}S. N]m \end{matrix}

\begin{matrix}(↑^{n}T, s) → & (T, ↑^{n}:: s) \\ ((M N), s) → & (M, N :: s) \\ (λ_{⟨S,t⟩}T, M :: s) → & (S. M, t, s) \\ (λ_{⟨S,t⟩}T, ↑^{n}:: M :: s) → & (↑^{n}S. M, t, s) \\ (#a, s) → & (!a, U(a) :: s) \\ (M = λ_{⟨S,t⟩}T, U(a) :: s) → & (M, s) a := M \\ (n̄, U(a) :: s) → & (n̄, s) a := n̄ \\ ([S]t, s) → & (S, t, s) \\ (S, λt, s) → & (λ_{⟨S,t⟩} [⇑^{1}S]t, s) \\ (S, (m n), s) → & (S, m, [S]n :: s) \\ (S, n, s) → & (S(n), s) \end{matrix}

CBN  Lazy
Recursive function Coq V5.10  Coq V6.1
Abstract machine  KN  KNP, Coq V6.3?