Isabelle/UTP

Metalogical operators

The metalogic for Isabelle/UTP is simply HOL itself. This allows us to treat UTP expressions and predicates as objects, and manipulate and query them in various ways. UTP predicates do not contain explicit syntax and thus all meta-logic operators are semantic in nature.

Unrestriction and Usedby

In the section on variables, we saw how lens operators allow us to check the similarity of two variables, for example using lens independence (\(x \bowtie y\)). We can check whether an expression e depends on a particular variable x using unrestriction, which is written as x \(\sharp\) P. Unrestriction plays a similar role to “free variables”, in that it allows us to determine if a variable is relevant for an expression’s evaluation. For example, consider a literal expression «v». It yields the same valuation regardless of the state-space, and thus it is unrestricted by any variable: x \(\sharp\) «v» is a theorem. On the other hand, it is not the case that x \(\sharp\) &x, since the valuation of this expression directly depends on the value of variable x. Yet, it is the case that x \(\sharp\) &y, provided that \(x \bowtie y\) – x and y are different areas of the state space.

As we noted in the section on variables, lenses can also be used to collect multiple variables in a set. Unrestriction additionally supports the notation {&x,&y,&z} \(\sharp\) P which states that P does not refer to any of the variables in the set. Internally the collect set becomes a summation of the corresponding lenses.

Unrestriction is not precisely the same as free variables, because it is a semantic rather than syntactic property. To see this, consider that z \(\sharp\) \((z < 0 \wedge z \ge 0)\). This is because the expression is semantically equivalent to true, no matter the valuation of z, and thus the expression does not depend on z.

The unrestriction operator distributes expression and predicate operators in an intuitive way, taking care to observe variables bound by quantifiers and abstractions. For example, \(y \sharp (\exists x \bullet P)\) provided that \(x \bowtie y\) – x and y are distinct – and \(y \sharp P\). The unrestriction laws for predicate calculus can be viewed in the repository. Proof of unrestriction conjectures can be undertaken by the tactic unrest_tac that applies all known unrestriction introduction rules.

The dual operator of unrestriction is called “usedby”, and is written as x \(\natural\) P. Rather than stating that P cannot depend on x, it states that P may only depend upon x. Thus x is an upper bound on the possible variables P can refer to it. It is useful in situations when we want to restrict a predicate to a particular set of variables. Like unrestriction it also support the set-style notation {&x,&y,&z} \(\natural\) P.

Substitution

We adopt a similar approach to that used by Back and Wright in their refinement calculus (see Chapter 9 on Relations) and model substitutions as functions on the state space: \(\sigma : \alpha \Rightarrow \alpha\). Intuitively, a substitution describes how the values of variables in the state space should be updated upon its application. The simplest substitution is the identity function id which simply retains the present value for all variables. A substitution can also be modified with the syntax \(\sigma(x \mapsto_s v)\), for lens \(x : \tau \Longrightarrow \alpha\) and expression \(v : (\tau, \alpha)\) uexpr, which changes the value of x to expression v in the substitution. Expression v can depend on previous values of x and any other variables in the state-space. For convenience, we also have the notation \([x_1 \mapsto_s v_1, \cdots, x_n \mapsto_s v_n]\) which constructs a substitution from n maplets.

Substitutions can be applied to expressions using the dagger notation \(\sigma \,\dagger\, e\), which applies the function to every possible state input of e. We also support the more traditional syntax for substitutions \(P [\!| v / x |\!]\), which is equivalent to \([x \mapsto_s v] \dagger P\).

As for unrestriction, there are a large number of laws for distributing substitutions through various operators. A sample of such laws for predicate calculus can be views in the repository. Such laws can be applied using the tactic subst_tac.

Alphabet Manipulation

Alphabets in Isabelle/UTP are simply represented as state space types, as in \(\alpha\) upred. Often it is convenient to be able to add or remove variables from an alphabet in order to grow or shrink the state space. Enforcing a particular alphabet is useful for ensuring that predicates are correct-by-construction, as the Isabelle type system is employed to ensure this.

Since variables are not atomic syntactic entities, we cannot simply remove them from a set. Instead it is necessary to perform a semantic transformation on the state space type. Fortunately, it turns out that we can again employ lenses to formalise these transformations.

First, we have the alphabet extrusion operator \(P \oplus_p a\) for P : \((\tau, \alpha)\) uexpr and a : \(\alpha \Longrightarrow \beta\). Lens a describes how state space \(\alpha\) can be losslessly embedded into a “larger” state space \(\beta\). The result of applying the alphabet extrusion is therefore an expression of type \((\tau, \beta)\) uexpr – the state space has changed to become \(\beta\). The semantics of the expression is the same, and any variables present in \(\beta\) but not in \(\alpha\) will be unrestricted.

Second, we have the alphabet restriction operator \(P \upharpoonleft_p a\) for P : \((\tau, \beta)\) uexpr and a : \(\alpha \Longrightarrow \beta\). It is similar to extrusion, but throws away part of \(\beta\) to result in an expression of type \((\tau, \alpha)\) uexpr. Unlike extrusion it is therefore lossy in nature. Nevertheless, we do have the intutive inverse law: \((P \oplus_p a) \upharpoonleft_p a = P\).