13 - Schema types and bindings

Summary

This chapter shows how to use schemas to define new data types. It also explains the mathematical meaning or semantics of schemas. This will help you use schemas expressively and reason about Z texts.

Schema types

So far we have treated schemas as nothing more than macros that we can use to abbreviate blocks of mathematical text. In this view, schemas and the schema calculus are just conveniences: They save us a lot of writing, but they don't introduce any new concepts. This modest view provides practical benefits — but it isn't very ambitious.

Schemas are more than just abbreviations. They are objects in their own right. Schema definitions declare new data types called schema types. The instances of schema types are objects called bindings. Schema references denote sets of bindings. Schema types and bindings are new kinds of mathematical objects.

So far we have defined only three kinds of fundamental data types — all of the others are built up from these: basic types, declared as in [X], whose instances are individuals; set types, declared as in ℙ X, whose instances are sets; and Cartesian product types, declared as in X × Y, whose instances are tuples. Schema types and their instances, bindings, are the fourth (and last) kind of data type in Z.

A binding is the formal realization, in Z, of what we have been calling a situation or a state: an assignment of particular values to a collection of named variables.