% Author: Brigitte Pientka
%{{
# Normalizing lambda-terms
}}%
%{{
## Syntax
We define first intrinsically well-typed lambda-terms using the base type nat
and function type.
}}%
LF tp: type =
| nat: tp
| arr: tp -> tp -> tp
;
LF exp: 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 T
.
}}%
schema ctx = 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 [gamma |- lam \x. M]
, and the application case [gamma |- app M N]
. In the variable case, we simply return the variable. In the abstraction case, we recursively normalize [gamma, 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 [gamma |- M]
. If this results in an abstraction [gamma |- lam \x. M']
, then we continue to normalize [gamma |- M'[ ,N] ]
substituting for x
the term N
. Otherwise, we normalize recursively [gamma |- N]
and rebuild the application.
Recall that all meta-variables are associated with the identity substitution [..] by default which may be omitted.
}}%
rec norm : (gamma: ctx) [gamma |- exp T] -> [gamma |- exp T] =
fn e ⇒ case e of
| [gamma |- #p ] ⇒ [gamma |- #p]
| [gamma |- lam \x. M] ⇒
let [gamma, x:exp _ |- M'] = norm [gamma, x:exp _ |- M] in
[gamma |- lam \x. M']
| [gamma |- app M N] ⇒
(case norm [gamma |- M] of
| [gamma |- lam \x.M'] => norm [gamma |- M'[..,N]]
| [gamma |- M'] ⇒
let [gamma |- N'] = norm [gamma |- N] in
[gamma |- app M' N' ]
)
;