3. A Strict Computation Model for µZ

A strict computation model for µZ is described in the style of natural semantics [10]. The intention is to get a model which is abstract enough to provide an idea of computation in µZ, but also near enough to an implementation to serve as a starting point for its design.

The computation model is not primarily designed with the goal to get ``maximal'' computation power out of µZ. A complete model cannot be realized anyway. Efficient implementability and transparent traceability of execution are as significant as computation power. The last point is in particular important for the application to test-case evaluation, where the reason of the failure of a test needs to be understandable by humans. A major design decision derived from these considerations is to use a strict evaluation order. Strictness in the context of µZ means that members of the singleton set, $\Mzsingle{e}$, are completely evaluated before the set is constructed. Similarly, in constructed values, $\Mzconst{\mzconst}{\mzexS}$, the arguments are fully evaluated prior to the constructor call. Moreover, we will not provide ``parallel or'' ( $\bot \lor true \equiv true \lor \bot \equiv true$): disjunctions are computed from left to right². However, ``parallel and'' ( $\bot \land false \equiv false \land \bot \equiv false$) is provided in non-strict contexts, i.e. the properties of schemas. Thus $\Mzschema{p_1}{\mzex_1} \mzcap \Mzschema{p_2}{\mzex_2}$ is $\mzempty$ if one of the properties $\mzex_i$ is false, independent of possible divergency of the other property, whereas $\mzex_1 \mzcap \Mzschema{p}{\mzex_2}$ will be always undefined if $\mzex_1$ is undefined.

1. Disjunctive Normal Form

An expression inside a complement will not contribute to resolution in its context. Thus it makes a difference whether distributivity laws for pushing a complement into expressions have been applied. Moreover, only certain forms of properties of schemas contribute to resolution. Hence it is necessary to normalize expressions prior to constructing their operational semantics. To this end, the disjunctive normal form of expression is defined as follows:

$$\begin{array}{lllllllllll}\arraycolsep2pt \begin{array}{lcll}... ... \mzexp_2 & \text{\emph{property}} \end{array}\Also \end{array}$$

The normal form is justified by the de-Morgan laws of the calculus, as well as the several distributivity laws for translation. Beneath a translation there might still appear a conjunction, since translations cannot be pulled out of complements. We assume that complement is pushed as far as possible. Hidings should be pulled, embeddings pushed, and consecutive translations contracted. A lot of further partial evaluation which follows from the equational laws could be applied on normalization; however, apart of complement pushing, none of these really affects the power of the computation model.

The representation of schema properties, $\mzexp$, determines the contribution to resolution. The form $\Mztest{d}$ takes a set and tests if it is the non-empty set, the form $\Mztestn{d}$ is a shortcut for $\mzcomplement \Mztest{d}$ and tests if its operand is the empty set. These properties are executed using residuation, thus all variables in d need to be bounded before the test can be completed. The form $\mzpat \mzin \mzexd$ denotes the member test of a pattern $\mzpat$ in the disjunction $\mzexd$, where $\mzexd$ is reduced by residuation. The form p₁ = p₂ demands the unification of two patterns. The variables appearing in the patterns p, p₁, and p₂ must be directly bounded by the enclosing schema.

It can be shown that any flexible appearances of variables in a property can be converted into a membership-property together with a sequence of simple equations of flexible variables, x = x'. By a flexible appearance we mean a variable x used as in $\Mzschema{P~x}{ C~\Mzsingle{\Pi~x}}$, where C is a positive conjunctive context build from intersections and translations, and $\Pi$ a context of constructor applications.

Proof.

Let $\Mzschema{p}{\Mztest{(\mzbigcap \mzexlS)}}$ be a schema with a positive conjunctive property as an intermediate result of normalization, where constructor decomposition has been performed, hidings have been pulled and absorbed by the overall hiding of $\Mztest{\_}$, and embeddings have been pushed to the leaves. Henceforth $\Mztest{(\mzbigcap \mzexlS)}$ must match (modulo associativity and commutativity)

$$\Mztest{(\MztransN{\Mzsingle{x_1}}{p_1}{q_1} \mzcap \ldots \mzcap \MztransN{\Mzsingle{x_n}}{p_n}{q_n} \mzcap e)}$$

where the x_i are flexible and where e does not contains variables in flexible position. Next we unify the patterns q_i against each other (if this fails then the property reduces to $\mzempty$ already at normalization time). Let $\mzpass$ be the resulting substitution, and let $\mzvass = \{x_1 \mapsto \mzpdosubs \mzpass ~ \mzpat_1, \ldots, x_n \mapsto \mzpdosubs \mzpass ~ \mzpat_n \}$ be a substitution for the flexible variables x_i, and $q = \mzpdosubs \mzpass ~ q_1$ the unified translation target. Let $\mzvarS = \mzpvars q \cap \bigcup (\mzpvars \limg \ran \mzvass \rimg)$ the variables in q which are tight to the flexible variables (q can contain further variables introduced by embeddings). Then we construct the schema $\Mzschema{\mzpdosubs \mzvass ~ p}{(\mzvarS) \mzin \MztransN{(\mzedosubs \mzvass ~ e)}{q}{(\mzvarS)}}$. Yet, this schema might not be well-formed, since $\mzpdosubs \mzvass ~ p$ may result in a non-linear pattern. In this case, a simple renaming of double occurrences of variables is performed, adding aliases like x = x' for each renamed variable.

As an example consider the schema $\Mzschema{x}{(e,x) \mzin e'}$. This results in the normalized schema

$$\Mzschema{x}{x \mzin \MztransN{(\MztransN{\Mzsingle{e}}{x}{(x,\_)} \mzcap e')}{(\_,y)}{y}}.$$

The next example, $\Mzschema{(x,y,z)}{(e,x) \mzeq (y,z) \in e'}$, demonstrates aliasing:

$$\Mztest{(\bt{\MztransN{\Mzsingle{x}}{x}{(\_,x)} \mzcap \Mzt... ...} \mzcap % \\ \MztransN{\Mzsingle{e}}{x}{(x,\_)} \mzcap e')}}$$

Unification of $(\_,x)$ with $(y,\_$) and $(\_,z)$ yields (y,z). The resulting schema is

$$\Mzschema{(z,y,z')}{(y,z) \mzin (\MztransN{\Mzsingle{e}}{x}{(x,\_)} \mzcap e') ~ \cap ~ z \mzeq z'}.$$

In a subsequent normalization step this is reduced to a conjunction of two schemas, one holding the pattern-membership, the other the alias.

2. Values and Constraints

Values are a subset of normalized expressions, enriched by a tailored representation of a schema-like construct, called an intension. An intension consists of a pattern and a constraint. A basic constraint, $\Mzctr{\mzvass}{\mzexp}$, is a value assignment paired with a property expression. Constraints may be composed by conjunction and by disjunction, though we expect only conjunctions in intensions (disjunctions are needed later on):

$$\begin{array}{lllllllllll}\begin{array}{lcll} \mzexv \in \MZ... ... \in \MZVASS & == & \MZVAR \pfun \MZEXV \end{array}\end{array}$$

An intension $\Mzinten{p}{\Mzctr{\mzvass}{\mzexp}}$ can be interpreted as the schema $\Mzschema{p}{\mzedosubs \mzvass ~\mzexp}$. However, there are a few differences. First, it is possible that the above expansion results in an infinite term, since $\mzvass$ may contain an assignment referring to the intension itself. This circularity of assignments is used to express fixed-points in the computation model. Second, the property $\mzexp$ may contain free variables which are neither bounded by p not by $\mzvass$. These variables may be considered as ``local existential'' for the intension, and are used to represent hiding translations by intensions.

A (partial) equality on values, written as $v \nfeq v'$, is assumed. The equality takes commutativity and associativity of unions into account. Since equality of intensions cannot be decided, a second relation $v \nnfeq v'$ is required, which decides inequality. On base of value equality and inequality, a unification for ``extended patterns'' build from constructor application, variables, and values, written as $\Mzvunify{\mzpat_1}{\mzvass}{\mzpat_2}$, is assumed. This unification uses $\_ \nfeq \_$ for comparing values found at the bottom of constructor terms. The form $\Mzvnunify{\mzpat_1}{\mzvass}{\mzpat_2}$ decides whether unification fails (using $\_ \nnfeq \_$).

In principle, more powerful notions of unification can be embedded in our framework (e.g. set unification). This would require some technical modifications of the rules given in the next section to deal with sets of unifiers returned by unification instead of a single unifier.

3. Computation

Computation is defined by two relations, which are mutually dependent. The first relation, $\Ored{\mzex}{\mzvass}{\mzex'}$, describes a strict reduction step on expressions under the value assignment $\mzvass$. It cannot be applied to unbound variables, which means in the context of its usage that the according computation ``suspends''. The second relation, $\Osolv{\mzctr}{\mzctr'}$, describes a resolution step by mapping a constraint into a constraint. $\mzctr$ is expected to be in disjunctive normal form, and $\mzctr'$ will be so as well.

A few notational conventions for defining these relations are introduced. We write $\cbigand \mzctrS$ for a conjunction of constraints, and $\cbigor \mzctrS$ for a disjunction. For a sequence of basic constraints, $\MzctrS{\mzvassS}{\mzctrS}$ is written. The set of free variables used in a constraint can be retrieved by $\mzpvars \mzctr$. The notation $\Mzvunifyr{\mzpat_1}{\mzvass}{\mzvass'}{\mzpat_2}$ ``refines'' the assignment $\mzvass$ to the assignment $\mzvass'$ by the result of unifying $\mzpat_1$ with $\mzpat_2$. With $\mzvass \cpush \mzctr$ the propagation of an assignment into a constraint is described, which distributes over conjunction and disjunction. For basic constraints we have $\mzvass \cpush (\Mzctr{\mzvass'}{\mzexp}) = \Mzctr{(\mzvass' \circ \mzvass)}{\mzexp}$, where $\_ \circ \_$ is the usual composition of mappings. The common assignment of a conjunction of constraints is extracted with $\mzvass \cpull \mzctr$: for basic constraints we have $\mzvass \cpull \Mzctr{\mzvass}{\mzexp}$, and for conjuncted ones $\mzvass \cpull (\mzctr_1 \cand \mzctr_2)$ iff $\mzvass = \mzvass_1 \cup \mzvass_2 \in \MZVASS$ and $\mzvass_i \cpull \mzctr_i$ ($i \in \{1,2\}$).

Figure 1: Expression Reduction Rules

The rules for $\Ored{\mzex}{\mzvass}{\mzex'}$ are given in Fig. 1. Rule describes a reduction step in an arbitrary strict expression context STRICT, which is any context apart of the property of a schema. Rule describes the substitution of a variable, which will be only possible if the variable is bounded in $\mzvass$. This is one source of ``suspension''. Rule reduces a schema to an intension. The rule is only applicable if free variables of the property are either bounded by the pattern or by the substitution - that is variables from outer scopes are not allowed to be free. This is the other source of ``suspension''. Rule describes the construction of a fixed-point. The rule is cyclic in its premise, forestalling the resulting value $\mzexv$ in an assignment $\mzvass'$ which is used to calculate this value (the usual technique used in natural semantics for constructing fixed-points). A finite number of reduction steps is required to map the expression $\mzex$ to a value $\mzexv$: the expression $\mzex$ may contain several schemas, and the value form is reached not before all these schemas have been converted to intensions.

Rules to describe the elimination of tautologies in set union of values, rules to similar for set intersection of values. With $V \langle v_1,\ldots,v_n \rangle$ a value sequence context is denoted, where the v_i appear in some order in the sequence. Rules and model the combination of intensional values by intersection. If the patterns can be unified, then we simply concatenate the constraints of the intensions, making local existential variables disjunct; if they do not unify, the intersection reduces to $\mzempty$. Rule describes the distribution of intersection over union values. It should be noted that in an implementation intersection can be realized more efficiently as hinted by the rules: given a total order on values, and set values in a normalized form $\mzbigcup \Mzsingle{\mzexvS} \cup \mzbigcup \Mzinten{\mzpatS}{\mzctrS}$, their intersection can be realized by processing the extensional part, $\mzexvS$, in linear time, and then the combinations with the intensional part.

Rule handles the reduction of a translation to an intension. It uses the possibility to use existential variables in an intensions constraint: $\mzpat_1$ may contain variables not bounded by $\mzpat_2$. Rule  describes the translation of complement to an intension.

Rules to handle the $\mzmu$-operator. Once the argument of $\mzmu$ has been reduced to a value v, the elements of v are enumerated by resolving a constraint $x \mzin v$. The state of this sub-resolution is stored in an intermediate expression construct, $\mzmunarrow (\mzvar, \mzctr)$. Once the sub-resolution is in solved form, $\cbigor (\MzctrS{\mzvassS}{\mzunivS})$, a unique assignment for $\mzvar$ is extracted, if it exists.

Figure 2: Constraint Resolution Rules

The rules for constraint resolution, $\Osolv{\mzctr}{\mzctr'}$, are given in Fig. 2. Rule describes the left-to-right resolution of disjunctive constraints, rule the elimination of unsolvable constraints. Rules and describe the elimination of unsolvable and solved constraints in a conjunction, where $S\langle \mzctr \rangle$ is a sequence context. Rule describes a resolution step of a basic constraint in context of a conjunction. This rule models the concurrent execution of constraints by ``interleaving'', since the selection of a constraint in the context S is undetermined. The selected constraint rewrites to a disjunction. The conjunction context S is expanded for each member of this disjunction. In an implementation, this expansion can be implemented by backtracking (Sect. 4).

Rules to handle the reduction of expressions to values in basic constraints by $\Ored{\mzex}{\mzvass}{\mzex'}$. Rule decomposes the membership test on a value union into disjuncted constraints. Rule and describe a basic resolution step, reducing a membership-test on a singleton set to an assignment or a failure. Rule and describe the resolution of a member-ship test on an intension. The constraint of the intension is imported into the current resolution. Variables used in the intension's pattern and constraint are renamed by $\mzpass$ to fresh ones. Finally, rules and model the resolution of a pattern equality.

Rules to handle the resolution of tests of emptiness and non-emptiness of sets. Similar to the treatment of $\mzmu$ in expression reduction, a sub-resolution is started which enumerates the elements of the set v by resolving the constraint $x \mzin v$. The state of this resolution is stored in an intermediate property expression, $\Mztestnarrow{s}{\mzvar,\mzctr}$, where s is either $\mzuniv$ or $\mzempty$, depending on the pole of the test. The test succeeds (resp. fails, depending on s) if at least one constraint can be solved, it fails (resp. succeeds) if no constraint can be solved (which requires to enumerate the entire set).