SyntaxWe define first intrinsically well-typed lambda-terms using the base type
natand function type.
LFtp : type= | nat : tp | arr : tp → tp → tp; LFexp : tp → type= | lam : (exp T1 → exp T2) → exp (arr T1 T2) | app : exp (arr T2 T) → exp T2 → exp T;
Next, we define the context schema expressing the fact that all declarations must be instances of the type
exp T for some
schemactx = exp T;
Finally, we write a function which traverses a lambda-term and normalizes it. In the type of the function
norm we leave context variables implicit by writing
(g:ctx). As a consequence, we can omit passing a concrete context for it when calling
norm. In the program, we distinguish between three different cases: the variable case
[ ⊢ #p ], the abstraction case
[γ ⊢ lam λx. M], and the application case
[γ ⊢ app M N]. In the variable case, we simply return the variable. In the abstraction case, we recursively normalize
[γ, x:exp _ ⊢ M] extending the context with the additional declaration
x:exp _. Since we do not have a concrete name for the type of
x, we simply write an underscore and let Beluga's reconstruction algorithm infer the argument. In the application case, we first normalize recursively
[γ ⊢ M]. If this results in an abstraction
[γ ⊢ lam λx. M'], then we continue to normalize
[γ ⊢ M'[ ,N] ] substituting for
x the term
N. Otherwise, we normalize recursively
[γ ⊢ N] and rebuild the application.
Recall that all meta-variables are associated with the identity substitution […] by default which may be omitted.
recnorm : (γ:ctx) [γ ⊢ exp T] → [γ ⊢ exp T] = fne ⇒ casee of| [γ ⊢ #p] ⇒ [γ ⊢ #p] | [γ ⊢ lam (λx. M)] ⇒ let[γ, x : exp _ ⊢ M'] = norm [γ, x : exp _ ⊢ M] in[γ ⊢ lam (λx. M')] | [γ ⊢ app M N] ⇒ casenorm [γ ⊢ M] of| [γ ⊢ lam (λx. M')] ⇒ norm [γ ⊢ M'[…, N]] | [γ ⊢ M'] ⇒ let[γ ⊢ N'] = norm [γ ⊢ N] in[γ ⊢ app M' N'];