# 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.