Slide 1

Specification and Verification

of a Formal System for Non-mutual Structural Recursion

Andreas Abel December 17, 1999

Slide 2

Terms

s, t, t⃗ ::= x, λx.t, fun g(x)=t, t s, function space σ ) τ
in_{j}(t), case(t, x⃗.t),  coproduct  Σσ⃗
(t⃗), pi_{j}(t),  product  Πσ⃗
fold(t), unfold(t)  inductive type μX.σ

σ(μ X.σ(X)) fold ; −) (− ; unfold μ X.σ(X)

Named function introduction:

t ∈ Tm^{τ}[Γ, x^{Πσ⃗} , g^{Πσ⃗)τ} ] ⊢ g(x) sr t fun g^{Πσ⃗)τ} (x^{Πσ⃗} )=t ∈ Tm^{Πσ⃗)τ} [Γ] Slide 3

Dependencies

Δ = {y R t} where y ∈ TmVar^{σ} , t ∈ Tm^{τ}, R ∈ {<_{σ,τ}^{Tm}, ≤_{σ,τ}^{Tm}}

Judgements

Δ ⊢ s R t  R ∈ {<^{Tm}, ≤^{Tm}} structural ordering
Δ ⊢ (s⃗) ≺_{π} t  lexicographic ordering
Δ ⊢ g(x) sr t  g structural recursive in t

Slide 4

Structural Ordering

Right hand side rules (R ∈ {<^{Tm}, ≤^{Tm}}):

(RcaseR) Δ, x_{i} ≤^{Tm} s ⊢ s_{i} R t for i=1, ..., n

Δ ⊢ case(s, x⃗.s) R t
(RpiR) {Δ ⊢ s R t \atop Δ ⊢ pi_{j}(s) R t}
(RappR) {Δ ⊢ s R t \atop Δ ⊢ s a R t}  (RunfR) Δ ⊢ s ≤^{Tm} t Δ ⊢ unfold(s) R t

Slide 5 Left hand side rules (R ∈ {<^{Tm}, ≤^{Tm}}):

(RcaseL) Δ, x_{i} ≤^{Tm} t, y R t_{i}, Δ′ ⊢ p for i=1, ..., n

Δ, y R case(t, x⃗.t), Δ′ ⊢ p
(RpiL) {Δ, y R t, Δ′ ⊢ p \atop Δ, y R pi_{j}(t), Δ′ ⊢ p}

(RappL) {Δ, y R s, Δ′ ⊢ p \atop Δ, y R s a, Δ′ ⊢ p} (RunfL) Δ, y <^{Tm} t, Δ′ ⊢ p

Δ, y R unfold(t), Δ′ ⊢ p

Slide 6 Reflexivity and transitivity:

(≤^{Tm}refl) Δ ⊢ t ≤^{Tm} t

(<^{Tm}transL) Δ ⊢ s R t  y <^{Tm} s ∈ Δ  R ∈ {<^{Tm}, ≤^{Tm}}

Δ ⊢ y <^{Tm} t

(<^{Tm}transR) Δ ⊢ s <^{Tm} t  y R s ∈ Δ  R ∈ {<^{Tm}, ≤^{Tm}}

Δ ⊢ y <^{Tm} t

(≤^{Tm}trans) {Δ ⊢ s R t  y S s ∈ Δ  R, S ∈ \{<^{Tm}, ≤^{Tm}\} \atop Δ ⊢ y ≤^{Tm} t}

Slide 7

Lexicographic Ordering

(lex<^{Tm}) {Δ ⊢ s_{π(k)} <^{Tm} pi_{π(k)} (t) \atop Δ ⊢^{k} (s⃗) ≺_{π}^{Tm} t}

(lex≤^{Tm}) Δ ⊢ s_{π(k)} ≤^{Tm} pi_{π(k)} (t) Δ ⊢^{k+1} (s⃗) ≺_{π}^{Tm} t

Δ ⊢^{k} (s⃗) ≺_{π}^{Tm} t

Δ ⊢ (s⃗) ≺_{π}^{Tm} t :{} Δ ⊢^{1} (s⃗) ≺_{π}^{Tm} t

Slide 8

Structural Recursion

(srvar) {y ≠ g \atop Δ ⊢ sr y}  (srin) {Δ ⊢ sr t \atop Δ ⊢ sr in_{j}(t)}

(srcase)

Δ ⊢ sr s Δ, x_{i} ≤^{Tm} s ⊢ sr t_{i} for i=1, ..., |t⃗|
Δ ⊢ sr case(s, x⃗.t)
(srtup) {Δ ⊢ sr t_{i} for i=1, ..., |t⃗| \atop Δ ⊢ sr (t⃗)}  (srpi) {Δ ⊢ sr t \atop Δ ⊢ sr pi_{j}(t)}

(srlam) {Δ ⊢ sr t  y ≠ x \atop Δ ⊢ sr λy. t}  (srapp) {Δ ⊢ sr t  Δ ⊢ sr s \atop Δ ⊢ sr t s}

(srapprec) {Δ ⊢ sr (a⃗)  Δ ⊢ (a⃗) ≺_{π}^{Tm} x \atop Δ ⊢ sr g(a⃗)}

Slide 9

Values

v, v⃗ ::= in_{j}(v), (v⃗), fold(v), λx.t, fun g(x)=t

Operational Semantics

(opvar) ⟨x; e, x = v⟩ ] v  (opin) ⟨t; e⟩ ] v ; ⟨in_{j}(t); e⟩ ] in_{j}(v)

(opcase) ⟨t; e⟩ ] in_{j}(w)  ⟨t_{j}; e, x_{j} = w⟩ ] v^{τ} ; ⟨case(t, x⃗.t); e⟩ ] v

(optup) ⟨t_{i} ; e⟩ ] v_{i} for 1 ≤ i ≤ n ; ⟨(t⃗); e⟩ ] (v⃗)  (oppi) ⟨t; e⟩ ] (v⃗) ; ⟨pi_{j}(t); e⟩ ] v_{j}

(opfold)

⟨t; e⟩ ] v
⟨fold(t); e⟩ ] fold(v)

(opunfold)

⟨t; e⟩ ] fold(v)
⟨unfold(t); e⟩ ] v

Slide 10

(opapp) ⟨t; e⟩ ] f  ⟨s; e⟩ ] u  f@u ] v ; ⟨t s; e⟩ ] v

(oplam) ⟨λx.t; e⟩ ] ⟨λx.t; e⟩ (opappvl) ⟨t; e, x = u⟩ ] v ; ⟨λx.t; e⟩@u ] v

(oprec) ⟨fun g(x)=t; e⟩ ] ⟨fun g(x)=t; e⟩

(opappvr) ⟨t; e, g = ⟨fun g(x)=t; e⟩, x = u⟩ ] v ; ⟨fun g(x)=t; e⟩@u ] v

Slide 11

Good Values

f ∈ VAL^{σ)τ} {} ∀u ∈ VAL^{σ} . ∃v ∈ VAL^{τ}. f@u ] v

Strong Evaluation

f@u ⟩ v :{}  f@u ] v and v ∈ VAL
⟨t; e⟩ ⟩ v :{}  ⟨t; e⟩ ] v and v ∈ VAL and
⟨t′; e′⟩ ⟩ for every subclosure ⟨t′; e′⟩

Slide 12

Structural Ordering on Values

(≤refl) v ≤ v  (Rin) {v R w \atop v R in_{j}(w)}

(Rtup) {v R w_{j} for some j ∈ \{1 …|w⃗|\} \atop v R (w⃗)}

(Rarr) f@u ⟩ w  v R w ; v R f (Rfold) {v ≤ w \atop v R fold(w)}

(lex<) {v_{π(k)} < w_{π(k)} \atop (v⃗) ≺_{π}^{k} (w⃗)}  (lex≤) {v_{π(k)} ≤ w_{π(k)}  (v⃗) ≺_{π}^{k+1} (w⃗) \atop (v⃗) ≺_{π}^{k} (w⃗)}

Slide 13

Interpretation of the Structural Ordering

\begin{aligned}e ⊨^{wk} s R^{Tm} t & :\{\} & ⟨s; e⟩ ⟩ v ) ⟨t; e⟩ ⟩ w ) v R w \\ e ⊨ s R^{Tm} t & :\{\} & ⟨s; e⟩ ⟩ v & ⟨t; e⟩ ⟩ w & v R w \\ e ⊨ Δ & :\{\} & ∀p ∈ Δ. e ⊨ p \end{aligned}

Soundness of the Structural Ordering

Δ ⊢ s R^{Tm} t
R ∈ {<^{Tm}, ≤^{Tm}, ≺^{Tm}}
∀e ⊨ Δ. e ⊨^{wk} s R^{Tm} t

Slide 14

Soundness of Structural Recursion

f_{0} ≡ ⟨fun g(x)=t_{0}; e_{0}⟩ ∈ VAL

We can assume (by wellfoundedness of VAL)

∀w ≺ v_{0}. f_{0}@w ⟩

Lemma.

Δ ⊢ sr t  e ⊨ Δ  ⟨g; e⟩ ] f_{0}  ⟨x; e⟩ ⟩ v_{0} ; ⟨t; e⟩ ⟩