Fundamenta Informaticae XX (2001) 1–1 1 IOS Press

Errata of “Explicit Environments”

Masahiko Sato

Takafumi Sakurai

Rod Burstall

Abstract. Errata of [1].

1. Section 6.2

It would be helpful to give a supplementary explanation to the proof of Lemma 6.2 and 6.3. To prove the induction step of Lemma 6.2 and 6.3, we have to use the fact

If w(δ′) < w(δ), then w((e, δ′)) < w((e, δ)).

To prove this, we need to show that ω^{h(δ)} > w(δ) and that w(δ′) < w(δ) implies h(δ′) ≤ h(δ).

We can prove these properties, but we have an easier way of proving the Lemmas. Let w_{o} be the original w. Redefine w by w(δ):=⟨h(δ), w_{o}(δ)⟩ and the order on weights by ⟨h_{1}, o_{1}⟩ < ⟨h_{2}, o_{2}⟩:=h_{1} ≤ h_{2} ∧ o_{1} < o_{2}.

2. Appendix

Case 3.5.2.2. in the proof of Lemma 6.8 should be corrected as follows.

In ‘case 3.5.2.2. \overline{f} is empty:’, (ι_{c_{1}})_{σ_{1}}[(δ_{1}(e), ι_{x})] may not be a decoration, because δ_{1}(e) may contain bindable variables. So, the proof of this case should be replaced by the following proof.

Putting

γ′_{i} := (γ_{i})_{σ_{i}}[((δ_{i}, ι_{f}), ι_{x})] (i = 1, 2),
d:= c_{π}[e[[f]][[x]]], d_{2} := (c_{2})_{σ_{2}}[δ_{2}(e)[[f]][[x]]],

we have two decoreations γ′_{i} : d ↦ d_{i} (i = 1, 2) and have c_{2} → d_{2}, so that ν(d_{2}) < ν(c_{2}). From the fact that c_{1} ⪯_{c} c_{2}, we can see that d_{1} ⪯_{d} d_{2}. Hence, by IH, we see that d_{1} is SN.

References

[1] Sato, M., Sakurai T., and Burstall, R., Explicit Environments, Fundamenta Informaticae, 45, 2001, 79–115.