The consistency theorem for free type definitions in Z
Michael Z. Spivey · Formal Aspects of Computing · 1996
Abstract Successive editions of the author's reference manual for the Z specification language [ZRM89, ZRM92] gave different sufficient conditions for the consistency of free type definitions. Both were expressed in terms of the settheoretic constructions present in the type definition. Whilst the first edition specified that these constructions should be continuous , in the sense that they preserve limits of ascending chains of sets, the second edition specified that they should be finitary , i.e., that the result of each construction should be the union of a set of finite approximations. This short note clarifies the relationship between these two conditions.