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