Normal forms

Figure 4.13: A proof of the diamond property.

If 1 ^∗ r1 : G ⇒^cN n¹ ₁ G1 and 1^∗ r2 : G⇒^cN n² ₂ G2, withc1

Then the theorem easily follows by “completing the lattice”, as suggested

in figure 4.14. ✷

4.4.1 Normal forms

When defining a transition system, a distinguished subset of the config-urations are termed “normal forms”.At first glance, it seems natural to say that G is in normal form iff G contains no redices, since this amounts to saying that there exists no G such that 1 (j) r : G ⇒a G.However, in the absence of “garbage collection” this is too restricted: some redices which are no longer needed may prevent a graph from being in normal form.

✠

Therefore we rather settle on (where G is equipped with demand function D):

Definition 4.4.5 A graph G is in normal form if it contains no redex a

with D(a) ≥ 1. ✷

Another condition turns out to be of interest:

Definition 4.4.6 A graph G is said to be in well-typed normal form if

all nodes n with D(n) = 2 are passive. ✷

For the connection between normal forms and well-typed normal forms, we have

Fact 4.4.7 Suppose G has result node n0, and is in well-typed normal

form.Then also G is in normal form. ✷

Proof: We have thatD =Clo[G](D_n0).It will be sufficient to show that a is a partial application if D(a) ≥ 1, i.e. if D(a) ≥ d with d ∈ {1,2} using the inference system in figure 4.9. Below, this will be done by induction in the proof tree.

If D(a) ≥ d because Dn0(a) = d, then d = 2 (and a = n0).As G is in well-typed normal form, a is passive – but this is a contradiction.

If D(a) ≥ 1 because D(a) ≥ 2, or if D(a) ≥ 2 because a = S(p , i), D(p) ≥ 2 then again well-typedness tells us that a is passive, again yielding a contradiction.

If D(a) ≥1 because a =S(a,1), D(a) ≥ 1 then by the induction hypothesisa is a partial application – hence alsoa is a partial application.

If D(a) ≥ 1 because Ndarg(a, a), D(a) ≥ 1 then by induction a is a partial application - but this yields a contradiction.

If D(a) ≥ 1 because a is passive or a genuine partial application,

then clearly a is a partial application! ✷

For the opposite direction, supposeG has result node n0 and is in normal form but not in well-typed normal form.This could for instance happen if n0 is a cons-cell with partial applications as children.Then it seems fair to say that G is “ill-typed” in the sense that “the result node cannot be assigned a first-order type”⁹.Recall from the beginning of this chapter that we do not want to formulate any type system.

Definition 4.4.8 Let G be singlelabeled and in well-typed normal form, and letnbe a node inGwithD(n) = 2.Then we can define Val_G(n), “the value of n”, as follows: let l = L(n) (exists as n is passive), let a =Ar(l), and let {n_i|i ∈ {1. . . a}} be defined by n_i = S(n, i).As D(n_i) = 2, it makes sense to define

Val_G(n) = l(Val_G(n₁), . . . ,Val_G(n_a))

(ValG(n) may be an infinite term, if G is cyclic). ✷ As already mentioned, even if G is in normal form there may exist G such that 1 (j) r : G ⇒a G.However, for our purposes the content of the following lemma will be sufficient:

Lemma 4.4.9 SupposeGis in normal form and 1 ^∗ r : G ⇒^cN n G.Then G is in normal form, and n = 0. G is in well-typed normal form if and only if G is, in which case also – provided G and hence also G is single-labeled – Val_G(r(n)) = Val_G(n) for n such that D(n) = 2. ✷ Proof: It will be enough to show that if 1 (j) r : G⇒a G and G is in normal form then

1. D(a) = 0.

2. G is in normal form.

3. G is in well-typed normal form iff G is.

4.IfGis in well-typed normal form and singlelabeled, then Val_G(r(n)) = ValG(n) for n with D(n) = 2.

9Notice that we are not saying that it should be possible to assing an arbitrary node a first-order type.

1 is straightforward (as G contains no redex a with D(a) ≥ 1).Then 2 follows by lemma 4.3.13. 4 is immediate, as r respects passive nodes (but this does not show the “if”-part of 3, since in principle G might contain non-passive nodes n with D(n) = 2).To show 3, proceed as follows:

“if ” Suppose G is in well-typed normal form.It will be sufficient to prove the following: if D(n) ≥ 2 using the inference system in figure 4.9 (where D(n) = max{D(n)|r(n) = n}), then there exists n in G with D(n) = 2 such that r(n) = n (and hence n is passive, as n is passive).This will be done by induction in the proof tree, with only two non-trivial cases:

• Suppose D(n) ≥ 2 because n = S(p, i), D(p) ≥ 2.

By induction, there exists p in G with D(p) = 2 such that r(p) = p.Let n= S(p , i), then D(n) = 2 and r(n) = n.

• Suppose D(n) ≥2 because D(n) = 2.But this just means that there exists n in G such that D(n) = 2, r(n) = n.

“only if ” SupposeGis notin well-typed normal form.Then there exists a node n with D(n) = 2 which is not passive.As G is in normal form, n is not a redex (and in particular not equal a).But then, as r respects all nodes but a, r(n) is not passive – yet D(r(n)) = 2, showing that G is not in well-typed normal form.

✷ The following lemma states that one is not able to arrive at a normal form by doing a non-normal order step:

Lemma 4.4.10 Suppose 1 (j) r : G ⇒a G, with G in normal form and with D(a) = 0.Then also G is in normal form. ✷ Proof: Suppose G contains a redex a₁ with D(a₁) ≥ 1.Then, as r respects all nodes but a and a = a₁, we conclude that r(a₁) is a redex in G with D(r(a₁))≥ 1 – i. e. G is not in normal form. ✷ We will expect “normal forms to be unique”.In some sense, this is the content of the following theorem:

Theorem 4.4.11 Let G be a singlelabeled graph with result node n0.

Suppose 1 ^∗ r1 : G ⇒_N G1 and 1 ^∗ r2 : G ⇒_N G2, with G1 and G2 in well-typed normal form.Then ValG₁(r1(n0)) = ValG₂(r2(n0)). ✷

Proof: By theorem 4.4.4, there exist G, r₁ and r₂ such that

1 ^∗ r₁ : G1 ⇒_N G, 1 ^∗ r₂ : G2 ⇒_N G, and such that r1+r₁ = r2+r₂. By fact 4.3.14,r₁(n0) (r₂(n0)) is a result node ofG₁ (G₂), and then by fact 4.4.7 G₁ and G₂ are in normal form. By lemma 4.4.9, G is in well-typed normal form and Val_G(r₁(r₁(n0))) = Val_G1(r₁(n0)), Val_G(r₂(r₂(n0))) = Val_G2(r₂(n0)).But this shows that Val_G1(r₁(n0)) = Val_G2(r₂(n0)). ✷ Next we show that “all normal order reductions have equal length”:

Lemma 4.4.12 Suppose 1 ^∗ r₁ : G ⇒ⁿN n G₁ and 1 ^∗ r₂ : G ⇒ⁿN n G₂.Then G₁ is in normal form iff G₂ is in normal form, in which case G₁ = G₂. ✷ Proof: By theorem 4.4.4, we find that there existsG, r₁, r₂ andn such that 1 ^∗ r₁ : G1 ⇒ⁿ_{N n} G, 1^∗ r₂ : G2 ⇒ⁿ_{N n} G.Suppose G1 is in normal form.Then it must hold that n = 0, hence G2 = G1. ✷ The following lemma says that instead of first doing a non-normal order step and then a normal order step, one can do the normal order step first:

Lemma 4.4.13 Let G be singlelabeled.Suppose 1 (j) r₁ : G ⇒a G₁ and 1 (j1) r2 : G1 ⇒a₁ G2, with D(a) = 0 and D1(a₁) ≥ 1 (where D (D1) is the demand function of G (G1)).Then there exist r₁, r₂, G₁ and a with r₁(a) = a₁ and D(a) ≥ 1 such that

1 (j₁) r₁ : G ⇒a G₁,1 (j) r₂ : G₁ ⇒r₁(a) G₂

and r₁+r₂ = r₁+r₂. ✷

Proof: Lemma 4.3.13 tells us that there exists a in G with r1(a) = a₁ such that D(a) ≥1 and a is a redex.Hence (as G is singlelabeled) there exists r₁ and G₁ such that 1 (j₁) r₁ : G ⇒a G₁ (for some j₁). a =a, so lemma 4.4.3 applied to r₁ and r₁ says that there exists r₂,r₂ and G₂ such that

1 (j) r₂ : G₁ ⇒r₁(a) G₂,1 (j₁) r₂ : G1 ⇒r₁(a) G₂

and r₁+r₂ = r₁+r₂. Now, by lemma 4.4.2 applied to r₂ and r₂ exploiting that r₁(a) = a₁, we have r₂ = r₂, G₂ = G₂ and j₁ = j₁.Hence the claim.

✷

We now can show that “normal order reduction is optimal”:

Theorem 4.4.14 Let G be singlelabeled.Suppose 1 ^∗ r : G ⇒^cN n G, with G in normal form.Then there exists G in normal form, reduction r and c with n ≤ c ≤ c, such that 1 ^∗ r : G ⇒^cN c G.Moreover, G is

in well-typed normal form iff G is. ✷

Proof: By repeated applications of lemma 4.4.13, we find that there ex-istr,r, G, c ≥ nandc such that 1 ^∗ r : G ⇒^cN c G, 1 ^∗ r : G ⇒^cN0 G, r+r = r and c+c = c.

By repeated application of lemma 4.4.10, we see that G is in normal form. The last claim of the theorem follows from lemma 4.4.9. ✷ In a similar vein, we can show that “if there exists a looping evaluation with arbitrary many normal order steps, then also normal order reduction will loop” First we make the following

Definition 4.4.15 GivenG (singlelabeled).We say that G loops at level 1 by a normal order strategy, if for all n and G such that

1 ^∗ : G ⇒ⁿN n G

G is not in normal form. ✷

Theorem 4.4.16 Let singlelabeled graph G be given.Suppose for all n, there exists n₁ ≥ n, r₁ and G₁ such that 1 ^∗ r₁ : G ⇒N n₁ G₁.Then G loops at level 1 by a normal order strategy. ✷ Proof: Let 1^∗ : G ⇒ⁿN n G; we want to show that G is not in normal form.By assumption, there exists r₁, G₁ and n₁ ≥ n + 1 such that 1 ^∗ r₁ : G ⇒_{N n1} G₁. By repeated application of lemma 4.4.13, we find G₁ and n₁ ≥ n₁ such that 1 ^∗ : G ⇒ⁿ_{N n}¹ ₁ G₁.Hence, as n₁ ≥ n+ 1, we find G and c ≥ 1 such that

1 ^∗ : G ⇒ⁿN n G and 1^∗ : G ⇒^cN c G₁

the right hand side of which shows that G is not in normal form.Now

apply lemma 4.4.12 to the left hand side. ✷