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.
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').
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).
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);
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]];
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.