International Journal of Foundations of Computer Science \begin{matrix}c \\ ◯ \end{matrix} World Scientific Publishing Company

Errata of CATEGORICAL MODEL CONSTRUCTION FOR PROVING SYNTACTIC PROPERTIES [1]

TAKAFUMI SAKURAI

1. Revised version

We list up errors of our paper [1] here, but we would like you to read the revised version of this paper:

    http://www.math.s.chiba-u.ac.jp/~sakurai/papers/cms.dvi.gz

2. Section 4, p.217

The condition

(P1) if P (M[x := N]) and P (N), then P (λx.M)

should be replaced by the conditions

(P1a) If P (M[x := z]) where z is a variable, then P (M).

(P1b) If P (M), then P (λx.M).

and some proofs should be modified accordingly.

3. Section 4, p.219

The identities in the Remark

Ψ ∘ Φ(\overline{γ}x|M) = Ψ(\overline{γ}|λx.M) = \overline{γ}x|(λx.M)x
Φ ∘ Ψ(\overline{γ}|N) = Φ(\overline{γ}x|Nx) = \overline{γ}|λx.Nx

should be

Φ ∘ Ψ(\overline{γ}x|M) = Φ(\overline{γ}|λx.M) = \overline{γ}x|(λx.M)x
Ψ ∘ Φ(\overline{γ}|N) = Ψ(\overline{γ}x|Nx) = \overline{γ}|λx.Nx

(Φ and Ψ should be exchanged.)

4. Section 6, p.228

The condition (P1) if P (M[x := N]) for some P -value or type N, then P (λx.M) in page should be replaced by the conditions (P1a) If P (M[v := N]) where N is a variable or a type, then P (M). (P1b) If P (M), then P (λv.M). and some proofs should be modified accordingly. References

1. T. Sakurai, “Categorical Model Construction for Proving Syntactic Properties”, International Journal of Foundations of Computer Science, 20 12 (2001) 213–244.