Type Preservation for Parallel Reduction for the Simply-typed Lambda-calculus

We discuss the notion of parallel reduction, a standard relation relevant to many other important case studies, like the Church-Rosser Theorem. This case study is part of ORBI, the Open challenge problem Repository for systems reasoning with BInders. For a detailed description of the proof and a discussion regarding other systems see (Felty et al, 2014).
The mechanization highlights several aspects:

Context exchange via substitution
Free substitution property for parametric and hypothetical derivations
Type reconstruction via inference

Syntax

We encode the simply-typed lambda-calculus in the logical framework LF using Twelf-style syntax.

tp : type.

--name tp T. 

arr : tp → tp → tp.

nat : tp.

tm : type.

--name tm M x.

app : tm → tm → tm.

lam : (tm → tm) → tm.

Judgements and Rules

We describe parallel reduction and typing judgement for the simply-typed lambda-calculus using axioms and inference rules. The Beluga code is a straightforward HOAS encoding of the associated rules.

Parallel reduction

The predicate pr of type tm → tm → type defines parallel reduction, that M may reduce to M' or M → M'. β-reduction pr_b and its congruence rules pr_l and pr_a comprise the set of inference rules.

pr : tm → tm → type.

pr_l : ({x : tm} (pr x x → pr (M x) (N x))) → pr (lam M) (lam N).

pr_b : ({x : tm} (pr x x → pr (M x) (M' x))) → pr N N' → pr (app (lam M) N) (M' N').

pr_a : pr M M' → pr N N' → pr (app M N) (app M' N').

Typing judgement

Following the judgements-as-types principle, we define the type family oft which is indexed by terms tm and types tp. Constructors of_app and of_lam encode the typing rules for application and abstraction, respectively.

oft : tm → tp → type.

--name oft H. 

of_app : oft M1 (arr T2 T) → oft M2 T2 → oft (app M1 M2) T.

of_lam : ({x : tm} (oft x T1 → oft (M x) T2)) → oft (lam M) (arr T1 T2).

Context declarations

Just as types classify expressions, contexts are classified by context schemas.

schema rCtx = block (x:tm, pr_v:pr x x);

schema tCtx = some [t : tp] block (x:tm, of_v:oft x t);

schema trCtx = some [t : tp] block (x:tm, of_v:oft x t, pr_v:pr x x);

Substitution Lemma

Beluga enjoys the usual substitution property for parametric and hypothetical derivations for free since substitutivity is just a by-product of hypothetical-parametric judgements. Strictly speaking, the substitution lemma does not need to be stated explicitly in order to prove type preservation for parallel reduction but we've encoded it regardless. While this is usually proved by induction on the first derivation, we show it as a corollary of the substitution principles. In stating the substitution lemma we explicitly state that the types S and T cannot depend on the context g, i.e. they are closed.

rec subst : (g:tCtx) [g, b : block (x:tm, of_v:oft x T[]) ⊢ oft M[…, b.1] S[]] → [g ⊢ oft N T[]] → [g ⊢ oft M[…, N] S[]]  =
fn d1 ⇒ fn d2 ⇒ let  [g, b : block (x:tm, of_v:oft x T) ⊢ D1[…, b.1, b.2]] =
                                                                  d1 in 
  let  [g ⊢ D2] = d2 in [g ⊢ D1[…, _, D2]];

Type Preservation for Parallel Reductions

We prove type preservation for parallel reduction: when M steps to N and M has type A then N has the same type A. expressions to depend on the context since we may step terms containing variables. Substitution property for parametric and hypothetical derivations is free. We do not enforce here that the type A is closed. Although this is possible by writing A[] the statement looks simpler if we do not enforce this extra invariant.

rec tps : (g:trCtx) [g ⊢ pr M N] → [g ⊢ oft M A] → [g ⊢ oft N A]  =
fn r ⇒ fn d ⇒ case r of 
  | [g ⊢ #p.3] ⇒ d
  | [g ⊢ pr_b (λx. λpr_v. R1) R2] ⇒
    let  [g ⊢ of_app (of_lam (λx. λof_v. D1)) D2] = d in 
    let  [g, b : block (x:tm, of_v:oft x T, pr_v:pr x x) ⊢ F1[…, b.1, b.2]] =
    tps [g, b : block (x:tm, of_v:oft x _, pr_v:pr x x) ⊢ R1[…, b.1, b.3]] [g, b ⊢ D1[…, b.1, b.2]] in
    let  [g ⊢ F2] = tps [g ⊢ R2] [g ⊢ D2] in [g ⊢ F1[…, _, F2]]
  | [g ⊢ pr_l (λx. λpr_v. R)] ⇒
    let  [g ⊢ of_lam (λx. λof_v. D)] = d in 
    let  [g, b : block (x:tm, of_v:oft x T, pr_v:pr x x) ⊢ F[…, b.1, b.2]] =
    tps [g, b : block (x:tm, of_v:oft x _, pr_v:pr x x) ⊢ R[…, b.1, b.3]] [g, b ⊢ D[…, b.1, b.2]] in
    [g ⊢ of_lam (λx. λof_v. F)]
  | [g ⊢ pr_a R1 R2] ⇒
    let  [g ⊢ of_app D1 D2] = d in 
    let  [g ⊢ F1] = tps [g ⊢ R1] [g ⊢ D1] in 
    let  [g ⊢ F2] = tps [g ⊢ R2] [g ⊢ D2] in [g ⊢ of_app F1 F2];

The β-reduction case is perhaps the most note-worthy. We know by assumption that d:[g ⊢ oft (app (lam A (λx. M x)) N)) (arr A B) and by inversion that d:[g ⊢ of_a (of_l λx. λu. D1 x u)D2 ] where D1 stands for oft (M x) B in the extended context g, x:tm , u:oft x A. Furthermore, D2 describes a derivation oft N A. A recursive call on D2 yields F2:oft N' A. Likewise, y the i.h. on D1, we obtain a derivation F1:oft M' B in g, b:block (x:tm , of_x:oft x A). We now want to substitute for x the term N', and for the derivation oft x A the derivation F2. This is achieved by applying to F1 the substitution …, _ F2). Since in the program above we do not have the name N available, we write an underscore and let Beluga's type reconstruction algorithm infer the appropriate name.