2. The µZ Calculus

In this section the definition of the µZ calculus is given: its syntax, semantics, and equational theory. As the meta language we loosely orient at the Z notation.

1. Syntax and Informal Semantics

Let $\mzvar \in \MZVAR$ be variable symbols, and let $\mzconst \in \MZCONST$ be (term) constructor symbols. The µZ calculus knows the syntactic categories of expressions, and a subset of them, patterns:

$$\begin{array}{lllllllllll}\mzex \in \MZEX & ::= & \bt{ \Mzva... ...x} } \\ \mzpat \in \MZPAT & \subseteq & \MZEX \par\end{array}$$

The form $\Mzconst{\mzconst}{\mzexS}$ describes a constructor application, where $\mzexS$ is a sequence of expressions. (We generally use the convention to denote sequences of terms t by $\Sq{t}$.) The set of patterns $\MZPAT \subseteq \MZEX$ are those expressions which are solely build from constructor application to patterns, $\Mzconst{\mzconst}{\mzpatS}$, and variables, $\mzvar$.

The form $\Mzsingle{\mzex}$ denotes a singleton set. The form $\mzmu \mzex$ is the singleton set selection, which returns the element of a singleton set, and is undefined for each other set. The usual forms for set algebra are provided: the empty set is denoted by $\mzempty$, set intersection by $\mzex \mzcap \mzex'$, set union by $\mzex \mzcup \mzex'$, and set complement by $\mzcomplement \mzex$.

The form $\MztransN{\mzex}{\mzpat_1}{\mzpat_2}$ describes the translation of the set $\mzex$, and is not so familiar (it may found its roots in category theory). The result of translation consists of all elements which match against $\mzpat_2$, such that there exists an element in $\mzex$ which matches against the pattern $\mzpat_1$ under the same substitution. Thereby, both patterns may contain unbound variables, which may be denoted by wildcards (_). For example, the cartesian product of two sets, $\mzex_1 \cross \mzex_2$, can be expressed in µZ as $\MztransN{\mzex_1}{x}{(x,\_)} \mzcap \MztransN{\mzex_2}{y}{(\_,y)}$ (with $(\_,\_)$ the constructor symbol for pairs used in mixfix notation). Vice versa, the range of a binary relation $\mzex$ (a set of pairs) is denoted as $\MztransN{\mzex}{(\_,y)}{y}$. We call a translation with $\mzpvars \mzpat_1 \subseteq \mzpvars \mzpat_2$ an embedding and with $\mzpvars \mzpat_1 \supset \mzpvars \mzpat_2$ a hiding. Note that there might exist translations which are neither embeddings or hidings.

The form $\Mzschema{\mzpat}{\mzex}$ describes a set-comprehension, or a schema in Z speech. It denotes the set of values which match the pattern $\mzpat$ such that the boolean expression $\mzex$ is true under the binding of variables resulting by the match. A boolean expression is thereby just a set-expression over the element type of units (a type containing just one element): let $\mzcunit$ be the 0-ary constructor for this element, then truth is the set $\Mzsingle{\mzcunit}$, falsity the empty set, conjunction intersection, disjunction union, and negation complement. For example, the (sugared) schema $\Mzschema{(x,y,z)}{x < y \mzcap y < z}$ describes the set of triples where each member is larger then the previous one. The boolean expression x < y thereby is syntactic sugar for the form $\MztransN{((\_ < \_) \mzcap \Mzsingle{(x,y)})}{\_}{\mzcunit}$ (where $\_ < \_$ is a binary relation, a set of pairs). The conclusive translation can be read as: we are not interested in the actual result of the intersection, we just want to know if it is empty or not.

The form $\Mzfix{p}{\mzex}$ describes the smallest member of the set $\Mzschema{p}{p = \mzex}$ (where the equality abbreviates $\MztransN{(\Mzsingle{p} \mzcap \Mzsingle{\mzex})}{\_}{\mzcunit}$). The order needed here is discussed in Sect. 2.3. If a smallest member does not exists, the form is undefined.

The µZ calculus uses a shallow-polymorphic type system which, since it is fairly standard, is not made explicit within this paper. To this end, constructors $\mzconst$ have associated a (generic) type, and expressions are assumed to have a principal type. A further condition for well-formedness is that patterns in translations and schemas are used linear (no variable is allowed to appear twice).

For commonly used forms of expressions, syntactic sugar is used:

$$\begin{array}{lll} \mzuniv & \leadsto & \mzcomplement \mzem... ...zexS) & \leadsto & \mzex \mzcap \mzbigcap \mzexS \end{array}$$

Following Z conventions, $\langle a_1,\ldots,a_n \rangle$ is a sequence display, and $\_ \cat \_$ sequence concatenation.

2. Mappings

Before we take a closer look on the meaning of µZ expressions, the translation of Z into µZ is discussed. A brief comparison with the functional logic language Curry [7] is also given, anticipating some basics about the computation model of µZ.

Z.

The operations of the simple-typed $\lambda$-calculus contained in Z are mapped as follows:

$$\begin{array}{lllllllllll}\bt[4pt]{ \lambda p @ e & \leadsto... ...\MztransN{\Mzsingle{e'}}{x}{(x,\_)})}{(\_,y)}{y}) }\end{array}$$

This handles functions as sets of pairs. The mapping of the application in fact also captures relational application as used in Z: it is sufficient that e is a binary relation which is right-unique and defined just at the point e'.

We have already noted that predicate expressions are a special case of set-expressions over the element type of units, and have defined abbreviations for the basic predicates of membership-test and equality. To make the picture complete, here is the mapping of quantifiers:

$$\begin{array}{lllllllllll}\bt[4pt]{ \exists x @ e & \leadsto ... ...mplement (\Mztest{\Mzschema{x}{\mzcomplement e}}) }\end{array}$$

The underlying semantic of the mapping of predicate calculus is a partial three-point logic, as discussed in Sect. 2.3.

In Z, a schema denotes a set of bindings, where bindings are tuples (records) with named components. The set is constraint by the declarations of a schema as well as by the property. For example, the Z schema $[a:\nat;b:\num\vert a < b]$ denotes the set of bindings $\lbind a \bind x, b \bind y \rbind$, where $x \in \nat$, $y \in \num$, and x < y. Assuming appropriate µZ constructors for bindings, the above Z schema is mapped to µZ by $\MztransN{\nat}{x}{\lbind a \bind x, b \bind \_ \rbind} \mzcap \Mzschema{\lbind a \bind x, b \bind y \rbind}{x < y}$ (the constraint $y \in \num$ vanishes since $\num$ is a given type). The property x < y is further translated as described in the previous section.

The connectivities of the schema calculus easily map as well. Schema conjunction in Z, $S_1 \land S_2$, is the set of bindings with the joined signature of S₁ and S₂ where components with the same name are identified. This is expressed in µZ as $\MztransN{S_1}{\Sigma(S_1)}{\Sigma} \mzcap \MztransN{S_2}{\Sigma(S_2)}{\Sigma}$, where $\Sigma$ is the pattern for the joined signature, and the same pattern variables are chosen at the identified positions. Existential schema quantification, $\exists S @ S'$, is mapped to $\MztransN{(\MztransN{S}{\Sigma(S)}{\Sigma(S')} \mzcap S')}{\Sigma(S')}{\Sigma(S') \setminus \Sigma(S)}$ (where $\Sigma(S') \setminus \Sigma(S)$ denotes the removal of the components from S in S'. Similarly, the remaining connectivities of the schema calculus are mapped.

Functional Logic Languages.

Languages such as Curry[7] can be mapped in principle to µZ. The exact operational semantics of such a mapping will not be the same, since for example in µZ a strict reduction order is preferred by design. An illustration of such a mapping is helpful anyway.

A function definition in Curry with constraints is mapped as follows (where the fresh variables y_i below must not appear in the patterns $\mzpat_i$):

$$\begin{array}{lllllllllll}f~p_1 \vert c_1 ~ ~ = e_1; \ldots; ... ...% \\ \Mzschema{(p_n,y_n)}{c_1 \mzcap y_n = e_n}}\>}\end{array}$$

Thereby, an equational constraint c of Curry directly maps to an according equation in µZ. Conjunctions of constraints are expressed by intersection. Calling a function which returns a constraint with a free variable as the argument, such as C x, amounts to membership test, $x \mzin C$. In fact, µZ allows a richer constraint language than Curry (for example, disjunction and universal quantification) which, however, will not always be executable.

The computation model of µZ as described later on executes constraints concurrently, using both residuation as well as backtracking to deal with free variables. An access to a free variable is generally suspended in a nested context. This is for example the case for arguments of the $\mzmu$-operator, (and therefore for function application e e' which is defined using $\mzmu$), or for negative constraints. Backtracking may take place for constraints which map to the membership test of a pattern in a set. For illustration consider the definition of an ``append'' relation on lists. Below a shortcut for introducing local variables is used: $\Mzschema{p \setminus q}{e}$ is equivalent to $\MztransN{\Mzschema{(p,q)}{e}}{(p,q)}{p}$:

$$\begin{array}{lllllllllll}\Mzfix{app}{ \<\Mzschema{(\langle\... ...tminus t}{(xs,ys,t) \mzin app \mzcap zs = x::t}} \>\end{array}$$

Applying this relation to unbound xs and ys but bound zs will compute the possible partitions of the list zs, as usual in logic languages.

µZ is higher-order since sets can be stored in variables - and the relation app as defined above is nothing more than a set. Yet, as Curry, the µZ's computation model does not employs higher-order unification. This restriction is, however, not bounded to the notion of a type of a value (whether it is a set or not) but to the representation: sets which are extensionally represented are incorporated by a simple equality test in unification. An extensional representation is given by applying constructors, singleton sets, and set union to extensional values.

3. Semantics

We will not give a detailed semantic mapping here, but only discuss the principles. The model of µZ is based on a hierarchical typed universe, where sets are represented as partial characteristic (boolean) functions in a set-theoretical meaning, which can be founded by Z itself or by ZF set theory [18]. This representation of sets is a generalization of partial three-point logics [13] to the case of set-algebra. There are three observation to be made about a set represented as a partial characteristic function: an element is member (it is in the domain and is mapped to true), an element is not member (it is in the domain and is mapped to false), or it is unknown to be member or not (it is not in the domain). As a result, we are able to give expressions of the kind $\Mzschema{x}{1 \div x = 1}$ a meaning: for 0, membership is unknown, for all other numbers it is known (1 is member and the other numbers are not).

Indeed, for infinite sets the test whether an element is in the domain of a characteristic function is not computable, but it is possible to delay the need for this computation. For example, the intersection of two sets represented by partial characteristic functions is defined as $f_1 \mzcap f_2 = \lambda x @ f_1~x \land f_2~x$, where the conjunction can be executed by ``parallel and''. Thus the meaning behaves compositionally: $\Mzschema{x}{1 \div x = 1} \mzcap \Mzschema{x}{x \neq 0}$ is a set with no unknowns. This is a prerequisite for a clean equational theory of µZ. The valid laws will be discussed in more detail in the next section. In particular, we will see that De-Morgan's laws hold, such that a disjunctive normal form can be constructed.

To give the fixed-point operator of µZ a meaning, an order on values need to be defined. Since we have union and intersection as total functions on sets, a µZ set constitutes a complete lattice, with the empty set (the total characteristic function constantly delivering false) the bottom element and the universal set of the according type the top element. The order for fixed-point construction is derived from this: $f_1 \sqsubseteq f_2 \iff f_1 \mzcap f_2 = f_1$. The order is pointwise lifted to values yielded from constructor application. Since we are not in a constructive world a priori, $\Mzfix{p}{e}$ might be not defined, since e may not be monotonic.

4. Equational Theory

µZ has a rich equational theory which can be used for partial evaluation and even for providing a narrowing semantics by plain expression transformation. Within this section, we will only discuss those laws which are necessary for establishing a disjunctive normal form as needed for the computation model.

The set operators of µZ follow the usual laws for boolean algebras. Commutativity and distributivity of union and intersection hold, and De Morgan's laws are satisfied such that we can build a conjunctive or disjunctive normal form. However, because of partiality, the principle of excluded middle does not hold ( $\mzcomplement \mzex \mzcap \mzex \equiv \mzempty$ does not hold). Yet, we have $\mzcomplement (\mzcomplement \mzex) \equiv \mzex$, and excluded middle for the case of singleton sets: $\Mzsingle{\mzex} \mzcap \mzcomplement \Mzsingle{\mzex} \mzequiv \mzempty$.

A singleton set containing a constructor application with arity greater zero can be decomposed into an intersection of embeddings as follows:

$$\Mzsingle{\Mzconst{\mzconst}{\mzex_1,\ldots,\mzex_n}} \mzeq... ...sN{\Mzsingle{\mzex_n}}{x_n}{\Mzconst{\mzconst}{\_,\ldots,x_n}}$$

Several laws regarding set translation are of interest. Consecutive translations are composable, if the intermediate patterns can be unified. If they cannot be unified, consecutive translation reduces to the empty set. Any translation distributes over set union. A translation by an embedding distributes over set intersection. A translation which is neither hiding or embedding can be split into an embeddings and a consecutive hiding. Any hiding can be lifted out of an intersection, by widening the scope of the hidden variables. The last two laws read as follows:

$$\begin{array}{lllllllllll}\zwhereR{ \MztransN{\mzex}{\mzpat_... ... }{ % \mzpvars \mzpat_1 \supset \mzpvars \mzpat_2 }\end{array}$$

Hence, since embeddings can be distributed and hidings can be lifted out of intersections, meanwhile other translations can be decomposed into embeddings and hidings, it is possible to normalize expressions such that embeddings are pushed to the leafs and hidings are pulled to the top of intersections.

Unfortunately, set complement does not distribute over translation, and translation cannot be lifted out of a complement in the general case. It is notable in this context that the complement of a hiding is related to a $\forall$-quantor: $\forall x @ e$ maps to $\mzcomplement (\MztransN{\Mzschema{x}{\mzcomplement e}}{x}{\mzcunit})$. The fact that complement cannot be pushed to the leaves is a hint to the necessary incompleteness of any computation model.

Schema construction distributes over union and intersection: $\Mzschema{\mzpat}{\mzex \mzcup \mzex'} \mzequiv \Mzschema{\mzpat}{\mzex} \mzcup \Mzschema{\mzpat}{\mzex'}$, and similarly for intersection. Set complement distributes over schema construction as follows: $\mzcomplement \Mzschema{\mzpat}{\mzex} \mzequiv \Mzschema{\mzpat}{\mzcomplement \mzex} \mzcup \mzcomplement (\MztransN{\mzuniv}{\mzpat}{\mzpat})$. Those elements need to be added which are in the complemented schema's meaning since they do not match the pattern $\mzpat$.