Curien’s normalizer is defined with a driver loop initializing the weakCM-machine. As seen in Section 9.1, Lescanne’s normalizer has the same structure. We simplified the abstract ma-chine corresponding to Lescanne’s normalizer by merging the data-structure continuation into the existing stack. We identify this simplification as corresponding to erasing moot con-trol delimiters in the corresponding direct-style normalization function.
We showed that both the functional correspondence between abstract machines and eval-uation functions and the syntactic correspondence between reduction semantics and abstract machines can be applied to strong normalization. In so doing, we established connections between an array of semantic artifacts: Curien’s normalizer, a continuation-based normal-ization function, a normalnormal-ization function in direct style, a traditional-style abstract machine, and a reduction semantics. A small variation on the direct-style normalization function leads to alternate but equivalent abstract machines and reduction semantics.
The normalization function corresponding to Curien’s normalizer is compositional. The first abstract machine (Section 10.3) uses two stacks, one corresponding to the original stack of Curien’s machine and one corresponding to the non-tail calls introduced in the driver loop. These two stacks are a consequence of our mechanical development of the abstract machine. The abstract machines corresponding to known normalization functions would normally have the one-stack architecture of the second abstract machine (Section 10.6). We do note, however, that this two-stack architecture is also found in Landin’s SECD machine (Section 4.5.2).
This chapter is based on joint work with Olivier Danvy and Kevin Millikin, but mistakes are mine.
Chapter 11
Strong normalization starting from Crégut’s KN -machine
In the previous chapter our starting point was Curien’s normalizer, implementing normal-ization of de Bruijn-indexedλ-terms toβ-normal forms. The normalizer has a driver loop, which repeatedly instantiates the weakCM-machine.
Crégut’s first specification for strong normalization also consists of a driver loop and a weak machine, with the driver loop repeatedly instantiating the weak machine [13]. Crégut has recently superseded this normalizer with his definition of theKN-machine [14]. This ma-chine takes the form of an abstract mama-chine (Section 4.5.2).
Roadmap In this chapter our starting point is Crégut’sKN-machine (Section 11.1). In pre-vious chapters we have seen the value of having abstract machines in disentangled form.
We hence disentangle the KN-machine in Section 11.2. Again, the disentangled version is in the image of defunctionalization. We present the higher-order direct-style compositional normalization function functionally corresponding to this version of the KN-machine (Sec-tion 11.3). We present the reduc(Sec-tion semantics syntactically corresponding to that abstract machine in Section 11.4.
11.1 Crégut’s definitional specification of the KN -machine
Crégut’s machine performs strong normalization of closed de Bruijn-indexedλ-terms. In the paper Crégut lets de Bruijn indices start at0. For uniformity with the rest of this text, we ‘shift’ the de Bruijn indices such that they start at1 and we adjust the transition rules accordingly.
Nonterminal configurations of theKN-machine are composed of four parts: (1) a ‘term’
elementu, (2) an environmente, (3) a stacks, and (4) a global de Bruijn levelmholding the
current abstraction-depth:1
Level m ::= {0, 1, 2, . . .}
P p ::= {t, m}
U u ::= t|Vm|p
c ::= (u, e) EnvKN e ::= •|c·e
StackKN s ::= •|c·s|Λ·s|p·s
ConfigurationKN := U×EnvKN×StackKN×Level
Here t ∈ TermdeB as defined in Section 1.6. The start configuration of the KN-machine is composed of the argument term for normalizationt, an empty environment, an empty stack, and0as the current abstraction-depth:(t, •, •, 0). The machine always stops with a use of the ‘unload transition’ when the term-part is aλ-term with an associated de Bruijn level and the stack is empty:2
KN({t, m0}, e, •, m) → t
Crégut’s definition of theKN-machine is transliterated into our notation:
normalizeKN : TermdeB→TermdeB
normalizeKNt = KN(t, •, •, 0)
KN : ConfigurationKN→TermdeB KN(1, (u, e0)·e, s, m) = KN(u, e0, s, m)
KN(i+1, c·e, s, m) = KN(i, e, s, m) KN(t t0, e, s, m) = KN(t, e, (t0, e)·s, m)
KN(λt, e, s, m) = KN(t, c·e, s0, m), ifs=c·s0 KN(λt, e, s, m) = KN(t, (Vm,•)·e, Λ·s, m+1), ifs6=c·s0 KN(Vm0, e, s, m) = KN({m−m0, m}, e, s, m)
KN({t, m0}, e, •, m) = t
KN({t, m0}, e, (t0, e0)·s, m) = KN(t0, e0, {t, m0}·s, m0) KN({t, m0}, e, {t0, m00}·s, m) = KN({t0t, m00}, e, s, m)
KN({t, m0}, e, Λ·s, m) = KN({λt, m0}, e, s, m)
Crégut proves the correctness of theKN-machine, i.e., that theKN-machine actually computes normal forms when they exist:3
Theorem 6 (Crégut)
Letta be closed term andt0be aβ-normal form.
Thent=βt0 ⇐⇒ normalizeKNt=t0
11.1.1 Normalization method
When the current term element is an index i, the second rule removes the first i− 1 clo-sures in the environment and the first rule then selects thei-th closure. Because Crégut only considers closed terms the environment always contains enough closures.
1The set of de Bruijn levels Level contain0as opposed to the set of de Bruijn indices Index used inλ-terms.
2For now, we differ from using the metavariablenranging overβ-normal forms to follow Crégut’s definition.
We thus also define the co-domain of the normalization function to be TermdeBinstead of NFormdeB.
3Lescanne and Curien do not present corresponding theorems for their machines.
Considering an applicationtt0the machine continues normalization of the left sub-termt with a new closure (consisting of the right sub-termt0 paired with the current environment) pushed on the stack.
Meeting an abstraction the top element of the stack is inspected with two different out-comes: (1) If that element is a closurecthe abstraction is the left sub-term of an application, andcis moved to the environment. That is, de Bruijn index1is bound to that closure and the rest of the environment is ‘lifted’ by one. (2) If the top element of the stack is not a closure, the abstraction is not the left sub-term of an application and the body of the abstraction must be normalized with an indicationΛon the stack that the normalized body is the body of an abstraction in the residual normal form. Also the current de Bruijn level is incremented and 1is bound to a special closure(Vm,•).
When such a special closure(Vm0,•)is substituted for a de Bruijn index, that index is (as explained above) bound by an abstraction that is part of the normal form. That is, the result should be an adjusted de Bruijn index. By construction the abstraction has levelm0and the current de Bruijn level ism, i.e., the resulting index is the differencem−m0. This residual de Bruijn index is introduced in the construction{m−m0, m}.
A construction{t, m0}indicates that a partial resulttis found and its de Bruijn level ism0. The next configuration depends on the stack. If the stack is emptytis the complete normal form. If the top element of the stack is a closure(t0, e0), the left sub-term of an application could not be reduced to an abstraction, and the right sub-termt0must be normalized in the application-time environmente0. {t, m0}is pushed on the stack to indicate an application must be constructed witht as left sub-term when normalization of the right sub-term is finished. Finally, if the top element of the stack indicates a residual abstraction (Λ) the partial resulttis the normalized body of an abstraction, and the partial result isλt.
A de Bruijn levelmis included in{t, m}-constructions such that right sub-terms of resid-ual applications are normalized with the correct current de Bruijn level.
11.1.2 Normalization of open terms
Because not all terms have a normal form, normalization is partial. But as theKN-machine is defined above normalization is also not defined on terms with free variables. In this text all machines so far normalize also such open terms. Only one transition rule is needed to extend theKN-machine to also normalize open terms:
KN(i, •, s, m) = KN({i+m, m}, •, s, m)
Considering an index that in the argument term corresponds to thei-th free variable, the second rule ofKNsubtracts the length of the environment in small steps. This length is the number of abstractions from the root of the term to the index, because the environment is always extended when normalizing the body of abstractions and nowhere else. The obtained index is therefore i. The above rule then adds the current abstraction-depth m, i.e., the number or constructed abstractions from the root to the index where it occurs in the residual term. In result, the de Bruijn indexi+mat that place in the normal form, then corresponds to thei-th free variable of the overall term. Alsomis the current level of the residual term i+m. We continue with the above rule included.