Expressibility in the Kleene Algebra of Partial Predicates with the Complement Composition

Abstract

In the paper we investigate the expressibility of partial predicates in the Kleene algebra extended with the composition of predicate complement and give a necessary and sufficient condition of this expressibility in terms of the existence of an optimal solution of an optimization problem. We also investigate the expressibility in the first-order Kleene algebra with predicate complement. The obtained results may be useful for software verification using an extension of the Floyd-Hoare logic for partial pre- and postconditions.

1 Introduction

A popular approach to software verification is based on application of Floyd-Hoare logic [1, 2] which allows one to derive valid assertions (triples) of the form $\{p\}f\{q\}$, where f is a program, p is a precondition, and q is a postcondition. Assertions are interpreted as follows: if an input data d of the program f satisfies the precondition p, and the program terminates on d, then the program’s output satisfies the postcondition q. The classical Floyd-Hoare logic admits the case when the program f has an undefined execution result (e.g. due to nontermination). However, the pre- and postcondition predicates are assumed to have a definite truth value (true or false). In some situations the latter assumption is not convenient and it makes sense to consider pre- and postconditions expressed by partial predicates which can be undefined on some data. This can happen, e.g., if pre- and postconditions can be most easily expressed using partial operations such as division of numbers. Then one has to either reinterpret/change the meaning of classical Floyd-Hoare triples and take into account partiality of predicates, or try to eliminate the need to ever deal with undefined predicate values by performing special well-formedness checks which imply that predicates are applied only to values on which they can be guaranteed to be defined.

Both approaches lead to certain complications: the former one leads to multiple possible triple interpretations, some of which make the rules of the classical Floyd-Hoare logic unsound; the latter one complicates triple derivations by requiring definedness of predicates in all intermediate derivation steps which may be inessential to the validity of a target triple.

When explicit unrestricted partial pre- and postconditions are allowed, at least two obvious generalized interpretations of a triple $\{p\}f\{q\}$ can be given [9]:

• (a) “strong triple”: if the precondition p is defined and true on the program’s input, and the program terminates with a result y, then the postcondition q is defined on y, and q is true on y.

• (b) “weak triple”: if the precondition p is defined and true on the program’s input, and the program terminates with a result y, and the postcondition q is defined on y, then q is true on y.

The “weak triple” interpretation makes the rules of the classical Floyd-Hoare logic unsound [14, 15], but this interpretation is attractive in the case of high-level verification of code implementing numerical algorithms in environments like Matlab or Octave and in other similar applications. In this sort of situations, during formal verification it is difficult to take into account all details of implementation of floating-point arithmetic and give precise error bounds for an algorithm implementation. Algorithm verification using the model of ideal real number/rational number arithmetic can be much more feasible and can be useful for detecting high-level flaws (unrelated to floating point arithmetic). In particular, such models are used in VerSAA [1] verifier for Matlab code and in Simulink Design Verifier. However, e.g., during high-level verification of a numerical algorithm in the model of ideal real number arithmetic in most cases it makes no sense to formally prove that zero values never appear in the denominators of division expressions in postconditions, since, anyway, the behavior of a verification model is an inexact approximation of the behavior of an actual program. So, in order to ensure validity of a triple under “strong triple” interpretation one is required to prove more (i.e. to prove a stronger statement) than what is necessary to prove the validity of a triple under “weak triple” interpretation, while the information content in the statement about triple validity relevant to the real-world decision making is essentially the same in both cases.

In the previous papers [4, 5, 9, 11,12,13, 16] we investigated an inference system for a variant of an extension of Floyd-Hoare logic for partial pre- and postconditions which is sound under “weak triple” interpretation. The formulation of the rules of this inference system requires the change of semantics (and, it turns out, syntax) of the logical language which is used to express the pre- and postcondition formulas. Note that the formulation of the rules of the classical Floyd-Hoare logic depends on the usual boolean compositions ($\lnot$, $\wedge$) which are applied to total predicates which appear in the program’s body and/or pre- and postconditions, e.g. the loop rule uses both the conjunction and negation:

Here p represents the loop invariant.

The formulation of the rules of the mentioned extension of Floyd-Hoare logic depends on compositions of partial predicates (from program’s body and/or pre- and postconditions). In this situation one needs to express and interpret compositions of predicates in terms of a certain three-valued logic, where the third truth value corresponds to the case where a predicate is undefined.

From the viewpoint of pragmatics, propositional compositions of such a logic have to be based on a finite system of functions of three-valued logic ($P_3$) which contains reasonable generalized versions of boolean negation and conjunction. In $P_3$ there exist multiple sets of functions which, arguably, fit this description. One choice is the system $\{f_T,f_F,f_{U},f_{\lnot },f_{\wedge }\}$, where $f_T,f_F,f_U$ are pairwise different constant functions (T for “true”, F for “false”, U for “undefined”), and $f_{\lnot }$, $f_{\wedge }$ are, respectively, an unary and binary operation on a 3 element set defined in accordance with the truth tables for negation and conjunction of Kleene’s strong 3-valued logic, i.e.

This system is not functionally complete in $P_3$, and, it turns out, the corresponding propositional compositions of predicates are not sufficient for representing the sequence and loop rules of the inference system of [9] for “weak triple” interpretation. A functionally complete (in $P_3$) extension of $\{f_T,f_F,f_{U},f_{\lnot },f_{\wedge }\}$ is sufficient for this purpose, but, from the results of [9] it turns out that a certain extension of $\{f_T,f_F,f_{U},f_{\lnot },f_{\wedge }\}$ which is not functionally complete in $P_3$ is also sufficient. Such an extension can be obtained by adjoining to $\{f_T,f_F,f_{U},f_{\lnot },f_{\wedge }\}$ an unary function $f_{\sim }$ defined as follows:

The propositional composition of partial predicates corresponding to $f_{\sim }$ was called in [9] the predicate complement and denoted as $\sim$. This composition can be used to extend the signature of the Kleene algebra of partial predicates [10]. Using such an extended signature, the loop rule of an extended Floyd-Hoare logic for partial pre- and postconditions with “weak triple” interpretation can be reformulated as [9]:

In this paper we investigate the question of expressibility of partial predicates in the Kleene algebra extended with the composition of predicate complement and give a necessary and sufficient condition of this expressibility in terms of the existence of an optimal solution of a special constrained optimization problem.

This is closely related to the properties of the functional closure of $\{f_T,f_F,f_{U},f_{\lnot },f_{\wedge },f_{\sim }\}$. The number of n-ary functions in this closure is $2^{3^n+O(2^n)}$ (see Proposition 2 in Sect. 3), which is asymptotically lower than the cardinality of the set of all n-ary operations on a three element set ($3^{3^n}$), and these functions have special properties that can be useful for software verification using the above mentioned extended Floyd-Hoare logic for partial pre- and postconditions and “weak triple” interpretation. For example (see Lemma 4 in Sect. 5), when checking satisfiability of an expression $E(x_1,...,x_n)$ over $\{f_T,f_F,f_{U},f_{\lnot },f_{\wedge },f_{\sim }\}$ by searching for a “true” value of E in some search space S, any evaluation of $E(x_1,...,x_n)$ which gives the “false” value can be used to eliminate from S elements which belong a metric ball with center $(x_1,...,x_n)$ and radius 1 in the sense of Chebyshev distance (the cardinality of which is at least $2^n$).

2 Notation

Unless indicated otherwise, n will denote an integer number.

The notation $f : A \,\tilde{\rightarrow }\,B$ means that f is a partial function on a set A with values in a set B, and $f: A \rightarrow B$ means that f is a total function from A to B.

The notation $x \mapsto e(x)$, where e is some expression, denotes a function which maps x to e(x). The domain of this function should be clear from the context.

For a function $f : A \,\tilde{\rightarrow }\, B$:

• $f(x)\downarrow$ means that f is defined on x;

• $f(x)\downarrow =y$ means that f is defined on x and $f(x)=y$;

• $f(x)\uparrow$ means that f is undefined on x;

• $dom(f)=\{ x \in A~|~f(x)\downarrow \}$ is the domain of a function.

We will denote as $f_{1} (x_1 )\cong f_{2} (x_2 )$ the strong equality, i.e. $f_{1} (x_1 )\downarrow$ if and only if $f_{2} (x_{2} )\downarrow$, and if $f_{1} (x_{1} )\downarrow$, then $f_{1} (x_{1} )=f_{2} (x_{2} )$.

The symbols T, F will denote the “true” and “false” values of predicates and $Bool = \{T,F\}$. The symbol $\bot$ will denote a nowhere defined partial predicate.

Depending on the context, $|\cdot |$ will denote either the cardinality of a set, or the absolute value of an (integer) number.

We will use $\circ$ to denote functional composition: $(f \circ g)(x) \cong f (g(x))$.

3 Preliminaries

Let $D \ne \emptyset$ be a set, $n\ge 1$, and $P_1$, ..., $P_n$ be partial predicates on D.

The Kleene algebra of partial predicates on D with predicate complement and constants $P_1,...,P_n$ is the algebra

$$\begin{aligned} APr_{P_1,...,P_n}(D)= (D~ \tilde{\rightarrow }~\{T,F\}; \vee , \wedge , \lnot , \sim , P_1, P_2,..., P_n), \end{aligned}$$

where

• 1. $\vee , \wedge , \lnot$ are the operations of disjunction, conjunction and negation on partial predicates defined in accordance with Kleene’s strong three-valued logic as follows:

  $$(P \vee Q)(d) = {\left\{ \begin{array}{ll}T, &{} \text {if }P(d)\downarrow = T \text { or } Q(d)\downarrow =T;\\ F, &{} \text {if }P(d)\downarrow = F \text { and } Q(d)\downarrow =F; \\ \text {undefined} &{} \text {in other cases}. \end{array}\right. }$$
  $$(P \wedge Q)(d) = {\left\{ \begin{array}{ll}T, &{} \text {if }P(d)\downarrow = T \text { and } Q(d)\downarrow =T;\\ F, &{} \text {if }P(d)\downarrow = F \text { or } Q(d)\downarrow =F; \\ \text {undefined} &{} \text {in other cases}. \end{array}\right. }$$
  $$(\lnot P)(d) = {\left\{ \begin{array}{ll}T, &{} \text {if }P(d)\downarrow = F ;\\ F, &{} \text {if }P(d)\downarrow = T ; \\ \text {undefined} &{} \text {in other case}. \end{array}\right. }$$

• 2. $\sim$ is the unary operation of predicate complement:

  $$(\sim P)(d) = {\left\{ \begin{array}{ll}T, &{} \text {if }P(d)\uparrow ;\\ \text {undefined}, &{} \text {if }P(d)\downarrow . \end{array}\right. }$$

Let V, W be non-empty sets, $n \ge 1$, and $Q_1$, ..., $Q_n$ be partial predicates on $V \,\tilde{\rightarrow }\,W$ (i.e. the set of all partial functions on V which take values in W). The elements of V will be interpreted as variable names, the elements of W as values, and the elements of $V \,\tilde{\rightarrow }\, W$ as partial variable assignments.

Denote $QPr^V_W=(V \,\tilde{\rightarrow }\, W) \tilde{\rightarrow }\{T,F\}$. We will call the elements of the set $QPr^V_W$ partial quasiary predicates over V and W. For a fixed finite V, such elements can be considered as continuations of partial n-ary predicates on W for $n=|V|$ to the cases when some arguments are undefined with the possibility of having a defined (“true” or “false”) value when some arguments are undefined, e.g. if $Q \in QPr^V_W$, Q(d) may take the “true” value when d is nowhere defined on V (empty variable assignment).

An existential quantification composition $\exists v$ (with parameter $v \in V$) is an unary operation on $QPr^V_W$ such that for each $Q \in QPr^V_W$:

$$(\exists v (Q))(d) = {\left\{ \begin{array}{ll}T, &{} \text {if }Q(d \nabla ^v a)\downarrow = T \text { for some } a \in W;\\ F, &{} \text {if }Q(d \nabla ^v a)\downarrow = F \text { for all } a \in W; \\ \text {undefined} &{} \text {in other cases}, \end{array}\right. }$$

where $d \nabla ^v a$ denotes the element of $V \,\tilde{\rightarrow }\, W$ with the graph

$$\begin{aligned} \{(v,a)\} \cup \{((v',d(v'))~|~ v' \in V \backslash \{v\}, d(v')\downarrow \}. \end{aligned}$$

When one restricts attention to total predicates and total variable assignments over a fixed finite V, $\exists v$ has the meaning corresponding to the meaning of the existential quantifier in the classical first order logic.

Similarly, a universal quantification composition $\forall v$ (with parameter $v \in V$) is an unary operation on $QPr^V_W$ such that for each $Q \in QPr^V_W$:

$$(\forall v (Q))(d) = {\left\{ \begin{array}{ll}T, &{} \text {if }Q(d \nabla ^v a)\downarrow = T \text { for all } a \in W;\\ F, &{} \text {if }Q(d \nabla ^v a)\downarrow = F \text { for some } a \in W; \\ \text {undefined} &{} \text {in other cases.} \end{array}\right. }$$

A renomination (variable renaming) composition $R^{\bar{u}}_{\bar{v}}$ with parameters $\bar{u} = (u_1,...,u_n) \in V^n$ and $\bar{v} = (v_1,...,v_n) \in V^n$ (where $n \ge 1$) such that $u_1,u_2,...,u_n$ are pairwise different, is an unary operation on $QPr^V_W$ such that for each $Q \in QPr^V_W$ and $d \in {}^VW$:

$$\begin{aligned} R^{\bar{u}}_{\bar{v}}(Q)(d)\cong Q(r^{\bar{u}}_{\bar{v}}(d)), \end{aligned}$$

where $r^{\bar{u}}_{\bar{v}}(d)=d \circ rn^{\bar{u}}_{\bar{v}}$ and $rn^{\bar{u}}_{\bar{v}}:V \rightarrow V$ is the function with the graph $\{(u_1,v_1),...,(u_n,v_n)\} \cup \{(u,u)~|~u\in V\backslash \{u_1,...,u_n\}\}$.

The first-order Kleene algebra of partial predicates over the set of variable names V and values W with predicate complement and constants $Q_1,...,Q_n$ is the algebra

$$\begin{aligned}&AQPr_{Q_1,...,Q_n}(V,W)\\&\quad =(QPr^V_W; \vee , \wedge , \lnot , \sim , \{R^{\bar{u}}_{\bar{v}}\}_{n' \ge 1, \bar{u} \in V^{n'}_{\ne },\bar{v} \in V^{n'}}, \{\exists v\}_{v \in V}, \{\forall v\}_{v \in V}, Q_1,..., Q_n), \end{aligned}$$

where $\vee , \wedge , \lnot , \sim$ are defined as above for $D = V\,\tilde{\rightarrow }\, W$, and $V^{n'}_{\ne }$ is the set of tuples $(v_1,...,v_{n'}) \in V^{n'}$ such that $v_i\ne v_j$ for all $i,j \in \{1,2,...,n'\}$ such that $i \ne j$.

Note that for a finite V the signature of $AQPr_{Q_1,...,Q_n}(V,W)$ contains only finitely many unary operation symbols.

We will also use the following algebra which we call the renominative Kleene algebra of partial predicates with predicate complement and constants $Q_1,...,Q_n$:

$$\begin{aligned} ARPr_{Q_1,...,Q_n}(V,W)= & {} (QPr^V_W; \vee , \wedge , \lnot , \sim , \{R^{\bar{u}}_{\bar{v}}\}_{n' \ge 1, \bar{u} \in V^{n'}_{\ne },\bar{v} \in V^{n'}}, Q_1,..., Q_n). \end{aligned}$$

We will say that a variable name $v \in V$ is unessential for a quasiary predicate $Q : (V \,\tilde{\rightarrow }\, W) \tilde{\rightarrow }Bool$, if $Q(d|_{V \backslash \{v\}}) \cong Q(d)$ for all $d \in V \,\tilde{\rightarrow }\, W$.

Let $X = \{-1,0,1\}$ and $F^{(n)}$ be the set of all n-ary functions (operations) $f : X^n \rightarrow X$. The elements of $F^{(n)}$ will represent functions of 3-valued logic $P_3$ (where 1 corresponds to the “true” value and $-1$ corresponds to the “false” value, and 0 is an intermediate truth value).

Let $F = \bigcup _{n \ge 0} F^{(n)}$.

We will denote as $\bar{x} = (x_1,x_2,...,x_n)$ a tuple of values $x_i \in X$.

Consider $X^n$ as a metric space with Chebyshev distance:

$$\begin{aligned} \rho _n((x_1,...,x_n),(y_1,...,y_n)) = \max _{i=1}^n |x_i-y_i|. \end{aligned}$$

Proposition 1

For $n \ge 1$, the equilateral metric dimension¹ of the metric space $(X^n, \rho _n)$ is $2^n$.

Proof

Let us show by induction on n that $|A| \le 2^n$ for any set $A \subseteq X^n$ such that $\rho _n(\bar{x}, \bar{y})=\rho _n(\bar{x}', \bar{y}')$ for all $\bar{x}, \bar{y}, \bar{x}', \bar{y}' \in A$ such that $\bar{x} \ne \bar{y}$ and $\bar{x}' \ne \bar{y}'$ (equidistant subset).

Induction base ($n=1$). The set $\{-1,0,1\}$ is not an equidistant subset, so $|A|\le 2$ for any equidistant subset $A \subseteq X$.

Induction step. Assume that for $n \ge 1$ it holds that $|A| \le 2^n$ for any equidistant subset A in $(X^n, \rho _n)$. Let $A'$ be an equidistant subset in $(X^{n+1}, \rho _{n+1})$. Let $A_j = \{(x_1,...,x_{n})~|~(x_1,...,x_n,j) \in A'\}$ for $j \in \{-1,0,1\}$.

For each $j \in \{-1,1\}$, $\bar{x}=(x_1,...,x_n) \in A_0 \cup A_j$, and $\bar{y}=(y_1,...,y_n) \in A_0 \cup A_j$ such that $\bar{x} \ne \bar{y}$ we have:

• 1. there exist $k,l \in \{0,j\}$ such that $\bar{x} \in A_k$ and $\bar{y} \in A_l$ and $|k-l| \le 1$.

• 2. moreover, $\rho _n(\bar{x}, \bar{y})=\max _{i=1}^n|x_i-y_i| = \max (\max _{i=1}^n|x_i-y_i|, |k-l|)$

  $= \rho _{n+1}((x_1,...,x_n,k), (y_1,...,y_n,l))$, where $(x_1,...,x_n,k)$ and $(y_1,...,y_n,l)$ are distinct elements of $A'$.

Since $A'$ is an equidistant subset, we have that $A_0 \cup A_{-1}$ and $A_0 \cup A_{1}$ are equidistant subsets in $(X^n, \rho _n)$. By induction hypothesis, $|A_0 \cup A_{j}| \le 2^n$ for $j \in \{-1,1\}$.

Also note that $A_{-1} \cap A_0 \cap A_{1} = \emptyset$, because otherwise, there exists a tuple $(x_1,...,x_n) \in X^n$ such that $(x_1,...,x_n,j) \in A'$ for each $j \in \{-1,0,1\}$, which contradicts the assumption that $A'$ is an equidistant subset.

Then $|A'| = |A_{-1}| + |A_{0}| + |A_{1}| = |A_{-1} \cup A_0| + |A_{-1} \cap A_0| + |A_1|$

$= |A_{-1} \cup A_0| + |(A_{-1} \cap A_0)\cup A_1| + |A_{-1} \cap A_0 \cap A_1|$

$\le |A_{-1} \cap A_0| + |A_0 \cup A_1| \le 2\cdot 2^n =2^{n+1}$.

We conclude that $|A| \le 2^n$ for each $n \ge 1$ and each equidistant subset A in $(X^n, \rho _n)$.

On the other hand, for each $n \ge 1$ we have $|\{0,1\}^n| = 2^n$ and $\{0,1\}^n$ is an equidistant subset in $(X^n, \rho _n)$, since $\rho _n(\bar{x}, \bar{y}) = \max _{i=1}^n|x_i-y_i| = 1$ for each $\bar{x} = (x_1,...,x_n) \in \{0,1\}^n$ and $\bar{y} = (y_1,...,y_n) \in \{0,1\}^n$ such that $\bar{x} \ne \bar{y}$.

Thus for $n \ge 1$ the equilateral metric dimension of $(X^n, \rho _n)$ is $2^n$.    $\square$

We will say that a function $f \in F^{(n)}$ is short, if it is a short map, i.e. if for all $\bar{x}$, $\bar{y}$ we have

$$\begin{aligned} |f(\bar{x})-f(\bar{y})| \le \rho _n (\bar{x}, \bar{y}). \end{aligned}$$

Let $M^{(n)}$ be the set of all short functions from $F^{(n)}$.

Proposition 2

$|M^{(n)}| = 2^{3^n+O(2^{n})}$

Proof

Since $X^n$ has $2^{3^n}$ subsets, it is sufficient to show that for any $n \ge 1$ and $Z \subseteq X^n$ the number of distinct functions from $M^{(n)}$ which have the set of zeros Z belongs to $\{1,2,3,...,2^{2^n}\}$.

Let $n \ge 1$ and $Z \subseteq X^n$. Denote $M^{(n)}_Z = \{f \in M^{(n)}~|~f^{-1}(\{0\})=Z\}$.

Let $f_Z \in F^{(n)}$ be a function such that $f_Z(\bar{x})=1$ for $\bar{x} \in X^n \backslash Z$ and $f_Z(\bar{x})=0$ for $\bar{x} \in Z$. Then for each $\bar{x}, \bar{y} \in X^n$ such that $\bar{x} \ne \bar{y}$ we have $|f_Z(\bar{x})-f_Z(\bar{y})| \le 1 \le$ $\le \rho _n(\bar{x},\bar{y})$. This and the definition of $f_Z$ imply that $f_Z \in M^{(n)}_Z$. Then $|M^{(n)}_Z| \ge 1$.

If $Z = X^n$, then $|M^{(n)}_Z| = 1 \in \{1,2,...,2^{2^n}\}$.

Now assume that $Z \ne X^n$.

Let $G=(X^n,E)$ be the $\{1\}$-distance graph of the metric space $(X^n,\rho _n)$, i.e. vertices $\bar{x},~ \bar{y} \in X^n$ are connected by an edge in E if and only if $\rho _n(\bar{x},\bar{y})=1$, and let $G_Z$ be a subgraph induced in G by the set of vertices $X^n\backslash Z \ne \emptyset$. Each $f \in M^{(n)}_Z$ is a graph homomorphism from $G_Z$ to the graph $(\{-1,1\},\{\{-1\},\{1\}\})$ ($\{a\}$ denotes a loop), because for each $\bar{x}, \bar{y} \in X^n \backslash Z$ such that $\rho _n(\bar{x},\bar{y}) = 1$ we have $|f(\bar{x})-f(\bar{y})| \le 1$, $f(\bar{x}) \ne 0$, and $f(\bar{y}) \ne 0$, whence $f(\bar{x}) = f(\bar{y})$. Hence f is constant on the vertex set of each connected component of $G_Z$.

Denote as $C_Z$ the set of connected components of $G_Z$. There exists a choice function $c : C_Z \rightarrow X^n$ which selects a vertex from each element of $C_Z$. Then for each $f_1,f_2 \in M^{(n)}_Z$, $f_1 \circ c = f_2 \circ c$ implies $f_1|_{X^n\backslash Z} = f_2|_{X^n\backslash Z}$ and $f_1|_Z = f_2|_Z$, whence $f_1=f_2$. Then the map $f \mapsto f \circ c$ is injective on $M^{(n)}_Z$ and takes values in $\{-1,1\}^{C_Z}$. Then $|M^{(n)}_Z| \le |\{-1,1\}^{C_Z}| = 2^{|C_Z|}$.

Denote as $c(C_Z)$ the image of $C_Z$ under c. We have $|C_Z| = |c(C_Z)|$, since the sets of vertices of connected components are pairwise disjoint and c in injective. Moreover, $c(C_Z)$ is an equidistant subset in the metric space $(X^n, \rho _n)$, because distinct elements $\bar{x}, \bar{y} \in c(C_Z)$ belong to different connected components of $G_Z$ and are not connected by an edge in E, and this implies $\rho _n(\bar{x},\bar{y})=2$. Then Proposition 1 implies that $|c(C_Z)| \le 2^n$. Hence $|M^{(n)}_Z| \le 2^{|C_Z|} \le 2^{2^n}$.

Thus the number of distinct functions from $M^{(n)}$ which have the set of zeros Z belongs to $\{1,2,3,...,2^{2^n}\}$ and we conclude that $|M^{(n)}| = 2^{3^n+O(2^{n})}$.    $\square$

4 Expressibility in Kleene Algebra

As before, let $X = \{-1,0,1\}$.

For any set D and a partial predicate $P : D \,\tilde{\rightarrow }\, \{T, F\}$ denote by $\varPhi (P)$ a function from $D \rightarrow X$ such that for all $d \in D$:

$$\varPhi (P)(d)= {\left\{ \begin{array}{ll} 1, &{} \text {if }P(d)\downarrow =T, \\ 0, &{} \text {if }P(d)\uparrow , \\ -1, &{} \text {if }P(d)\downarrow =F. \\ \end{array}\right. }$$

Note that $\varPhi$ is a bijection between $D \,\tilde{\rightarrow }\, \{T, F\}$ and $D \rightarrow X$.

Let $D \ne \emptyset$ be a fixed set, $P_0,P_1,...,P_n : D\,\tilde{\rightarrow }\,\{T,F\}$ be partial predicates, and $p_i = \varPhi (P_i)$ for $i=0,1,2,...,n$.

Denote $||f|| = \sum _{\bar{x} \in X^n} |f(\bar{x})|$ for $f \in F^{(n)}$ and consider the following (constrained) optimization problem²:

$$\begin{aligned} ||f|| \rightarrow \min \end{aligned}$$

(1)

$$\begin{aligned} f(p_1(d),p_2(d),...,p_n(d))=p_0(d),~~d \in D \end{aligned}$$

(2)

The following theorem characterizes expressibility in the Kleene algebra of partial predicates with predicate complement.

Theorem 1

If $n \ge 1$, a predicate $P_0$ is expressible in the algebra $APr_{P_1,...,P_n}(D)$ if and only if on the set $F^{(n)}$ the problem (1)–(2) has an optimal solution which is a short function.

The proof of this theorem is given in the next section.

$APr_{P_1,...,P_n}(D)$ induces the following pseudo-metric $\tilde{\rho }_{P_1,...,P_n}$ on D:

$$\begin{aligned} \tilde{\rho }_{P_1,...,P_n}(d,d')=\rho _n((p_1(d),...,p_n(d)),(p_1(d'),...,p_n(d'))). \end{aligned}$$

Note that the sum of $\tilde{\rho }_{P_1,...,P_n}$ and any metric on D is a metric on D.

A predicate $P_0$ is called short with respect to (w.r.t.) $P_1,...,P_n$, if $p_0$ is a short map between the pseudo-metric space $(D,\rho _{P_1,...,P_n})$ and $(X,\rho _1)$.

Theorem 2

If $n \ge 1$, $P_0$ is expressible in the algebra $APr_{P_1,...,P_n}(D)$ if and only if $P_0$ is short with respect to $P_1,P_2,...,P_n$.

Proof

“If”: Assume that $P_0$ is short w.r.t. $P_1, P_2, ..., P_n$. Then for all $d,d'\in D$:

$$\begin{aligned} |p_0(d)-p_0(d')| \le \tilde{\rho }_{P_1,...,P_n}(d,d')=\rho _n((p_1(d),...,p_n(d)),(p_1(d'),...,p_n(d'))). \end{aligned}$$

For each $\bar{x} = (x_1,...,x_n) \in X$ let $F(\bar{x})=\{p_0(d)~|~ d\in D \wedge \bigwedge _{i=1}^n p_i(d)=x_i\}$ and $f:X^n \rightarrow X$ be a function such that $f(\bar{x}) \in F(\bar{x})$, if $F(\bar{x}) \ne \emptyset$, and $f(\bar{x})=0$, if $F(\bar{x})=\emptyset$. Since $p_0$ is a short map, $F(\bar{x})$ is a singleton set whenever $F(\bar{x}) \ne \emptyset$. Then $f(p_1(d),p_2(d),...,p_n(d))=p_0(d)$ for all $d \in D$.

Let $\bar{x} = (x_1,...,x_n) \in X^n$, $\bar{y} = (y_1,...,y_n) \in X^n$. Assume that $\bar{x}\ne \bar{y}$. If $F(\bar{x}) = \emptyset$ or $F(\bar{y})=\emptyset$, then $f(\bar{x})=0$ or $f(\bar{y})=0$, whence $|f(\bar{x})-f(\bar{y})| \le 1 \le \rho _n(\bar{x},\bar{y})$. Otherwise, $F(\bar{x})\ne \emptyset$ and $F(\bar{y})\ne \emptyset$, so $f(\bar{x})=p_0(d_x)$ and $f(\bar{y})=p_0(d_y)$ for some $d_x, d_y \in D$ such that $p_i(d_x)=x_i$ and $p_i(d_y)=y_i$ for $i=1,2,...,n$. Then $|f(\bar{x})-f(\bar{y})|=|p_0(d_x)-p_0(d_y)| \le \rho _n(\bar{x},\bar{y})$. We conclude that $f \in M^{(n)}$.

Let $g \in F^{(n)}$ be a function such that $g(p_1(d),...,p_n(d)) = p_0(d)$ for all $d \in D$, Then $f(\bar{x})=g(\bar{x})$ whenever $F(\bar{x}) \ne \emptyset$. Then $||f|| \le ||g||$, since $f(\bar{x})=0$ when $F(\bar{x}) = \emptyset$. Thus on the set $F^{(n)}$ the problem (1)–(2) has an optimal solution which is a short function. Then by Theorem 1, $P_0$ is expressible in $APr_{P_1,...,P_n}(D)$.

“Only if”: Assume that $P_0$ is expressible in $APr_{P_1,...,P_n}(D)$. Then by Theorem 1, there exists $f \in M^{(n)}$ such that $f(p_1(d),p_2(d),...,p_n(d))=p_0(d)$ for all $d \in D$. Then for all $d, d' \in D$:

$$|p_0(d)-p_0(d')| \le |f(p_1(d),...,p_n(d))-f(p_1(d'),...,p_n(d'))| \le \tilde{\rho }_{P_1,...,P_n}(d,d').$$

   $\square$

Let $V \ne \emptyset$, $W \ne \emptyset$ be fixed sets, $Q_0,Q_1,...,Q_n : (V\,\tilde{\rightarrow }\, W)\,\tilde{\rightarrow }\,\{T,F\}$ be partial quasiary predicates, and $q_i = \varPhi (Q_i)$ for $i=0,1,2,...,n$.

If $k\ge 0$ and $m\in [0, 2^{k}-1]$ are integers, and $\bar{v} = (v_1,...,v_k) \in V^k$ (we assume $V^0$ consists of the single empty tuple), denote by $\mathfrak {Q}^{k}_{m,\bar{v}}(P)$, where P is a partial predicate, the k-th element of the finite sequence of predicates $T_j$, $j=0,1,...,k$ such that $T_0=P$ and for all $j=1,2,...,k$:

$$T_{j+1} = {\left\{ \begin{array}{ll}\exists v_j (T_j), &{} b_j = 0; \\ \forall v_j(T_j), &{} b_j = 1, \\ \end{array}\right. }$$

where $(b_j)$ is the j-th digit in the binary expansion of m (starting from the least significant digit).

The following theorem characterizes expressibility in the first-order Kleene algebra of partial predicates with predicate complement.

Theorem 3

Assume that $n \ge 1$ and there exists an infinite set $V' \subseteq V$ such that each name in $V'$ is unessential for each predicate in $\{Q_0, Q_1, ..., Q_n\}$. Then $Q_0$ is expressible in the algebra $AQPr_{Q_1,...,Q_n}(V,W)$ if and only if there exist

• integers $l \ge 1$, $k \ge 0$, $m \in [0,2^k-1]$,

• a tuple $\bar{v} \in V^k$,

• finite sequences of integers $k_j \ge 1$ and $n_j \in [1,n]$ for $j=1,2,...,l$,

• finite sequences of tuples $\bar{u}_j \in V^{k_j}_{\ne }$, $\bar{v}_j \in V^{k_j}$ for $j=1,2,...,l$,

• and a partial predicate P on $V\,\tilde{\rightarrow }\, W$, short w.r.t. $R^{\bar{u}_j}_{\bar{v}_j}(Q_{n_j})$ for $j=1,2,...,l$,

such that $Q_0=\mathfrak {Q}^k_{m,\bar{v}}(P)$.

We will give a proof of this theorem in Sect. 6.

5 Proof of Theorem 1

In order to prove Theorem 1, first let us formulate and prove a number of auxiliary lemmas.

Denote for all $x,y \in X$:

$$\begin{aligned} \lnot x = -x \end{aligned}$$

$$\begin{aligned} \sim x = 1 - |x| \end{aligned}$$

$$x^{[y]} = {\left\{ \begin{array}{ll}x, &{} \text {if } y=1 \\ \sim x, &{} \text {if } y=0 \\ \lnot x, &{} \text {if } y=-1 \\ \end{array}\right. }$$

Lemma 1

$\rho _n(\bar{x}, \bar{y}) = 1-\min _{i=1}^n x_i^{[y_i]}$ for every $n \ge 1$ and $\bar{x}, \bar{y} \in X^n$.

Proof

It is easy to see that for all $x, y \in X$:

$$\begin{aligned} x^{[y]} = 1-|x-y| \end{aligned}$$

Then $\rho _n(\bar{x}, \bar{y}) = \max _{i=1}^n |x_i-y_i| = \max _{i=1}^n (1-x_i^{[y_i]}) = 1 - \min _{i=1}^n x_i^{[y_i]}$.    $\square$

Consider X as a lattice with operations:

$$\begin{aligned} x \vee y = \max (x,y); \end{aligned}$$

$$\begin{aligned} x \wedge y = \min (x,y). \end{aligned}$$

Below we will assume that in expressions involving operations on X the operation $x^{[y]}$ has the highest priority, and is followed (by priority) by the unary operations $\lnot$, $\sim$, which are followed by the binary operations $\wedge$ and $\vee$. As usual, among $\wedge , \vee$, the operation $\wedge$ has higher priority.

Lemma 2

For each short function $f \in F^{(n)}$ and $\bar{x} \in X^n$:

$$\begin{aligned} f(\bar{x}) = \hat{f}(\bar{x}) \wedge f_{\ne 0}(\bar{x}) \vee \lnot f_{\ne 0}(\bar{x}) \end{aligned}$$

where

$$\hat{f}(\bar{x}) = {\left\{ \begin{array}{ll}\bigvee \nolimits _{\bar{y}: f(\bar{y})=1} \bigwedge \nolimits _{i=1}^n x_i^{[y_i]}, &{}\text {if } \exists \bar{y}~f(\bar{y})=1 \\ -1, &{} \text {otherwise} \\ \end{array}\right. }$$

$$f_{\ne 0}(\bar{x}) = {\left\{ \begin{array}{ll}\bigvee \nolimits _{\bar{y}: f(\bar{y})\ne 0} \bigwedge \nolimits _{i=1}^n \sim (x_i^{[y_i]} \wedge \sim x_i^{[y_i]}) \wedge \sim \sim x_i^{[y_i]}, &{} \text {if } \exists \bar{y} ~f(\bar{y})\ne 0 \\ 0, &{} \text {otherwise.} \\ \end{array}\right. }.$$

Proof

It is easy to see that for each $x,y \in X$:

$$\sim (x^{[y]} \wedge \sim x^{[y]}) \wedge \sim \sim x^{[y]} = {\left\{ \begin{array}{ll}1, &{} \text {if } x = y \\ 0, &{} \text {if } x \ne y. \\ \end{array}\right. }$$

Then

$$f_{\ne 0}(\bar{x}) = {\left\{ \begin{array}{ll}1, &{} \text {if } f(\bar{x}) \ne 0 \\ 0, &{} \text {if } f(\bar{x}) = 0. \\ \end{array}\right. }$$

By Lemma 1,

$$\hat{f}(\bar{x}) = {\left\{ \begin{array}{ll}\bigvee \nolimits _{\bar{y}: f(\bar{y})=1} (1-\rho _n(\bar{x}, \bar{y})), &{} \text {if } \exists \bar{y}~f(\bar{y})=1, \\ -1, &{} \text {otherwise}. \\ \end{array}\right. }$$

If $f(\bar{x}) = 1$, then $\hat{f}(\bar{x}) = 1$ and $f_{\ne 0}(\bar{x}) = 1$, so $\hat{f}(\bar{x}) \wedge f_{\ne 0}(\bar{x}) \vee \lnot f_{\ne 0}(\bar{x}) = 1$.

If $f(\bar{x}) = 0$, then $f_{\ne 0}(\bar{x})=0$, so

$\hat{f}(\bar{x}) \wedge f_{\ne 0}(\bar{x}) \vee \lnot f_{\ne 0}(\bar{x}) = (\hat{f}(\bar{x}) \wedge 0) \vee 0 = 0$.

If $f(\bar{x})=-1$, then for each $\bar{y}$ such that $f(\bar{y})=1$ we have $\rho _n(\bar{x}, \bar{y}) \ge |f(\bar{x})-f(\bar{y})|=2$ which implies that $1-\rho _n(\bar{x}, \bar{y})=-1$. Then $\hat{f}(\bar{x}) = -1$ and $f_{\ne 0}(\bar{x})=1$, so $\hat{f}(\bar{x}) \wedge f_{\ne 0}(\bar{x}) \vee \lnot f_{\ne 0}(\bar{x}) = -1$.

Thus

$$\begin{aligned} f(\bar{x}) = \hat{f}(\bar{x}) \wedge f_{\ne 0}(\bar{x}) \vee \lnot f_{\ne 0}(\bar{x}). \end{aligned}$$

   $\square$

Lemma 3

The set of all short functions from F is a precomplete class in F and is the functional closure of the set $\{f_{U},f_{\lnot },f_{\sim },f_{\vee },f_{\wedge }\}$, where $f_{U} \in F^{(0)}$, $f_{\lnot },f_{\sim } \in F^{(1)}$, $f_{\vee },f_{\wedge } \in F^{(2)}$, $f_{U}=0$, $f_{\lnot }(x) = -x$, $f_{\sim }(x) = 1-|x|$, $f_{\vee }(x,y) = \max (x,y)$, $f_{\wedge }(x,y) = \min (x,y)$.

Proof

Denote by S the set of all short functions from F. In accordance with its definition, a short function from F can be alternatively characterized as a function $X^n \rightarrow X$ ($n \ge 0$) which does not change sign on each of the sets $\prod _{i=1}^n\{0,a_i\}$, where $a_1,...,a_n \in \{-1,1\}^n$. In the terminology of [19], such functions correspond to the precomplete class $T^3_{\mathcal {E}_1,1}$ of functions for which the image of the product of sets, 1-equivalent to $\mathcal {E}_1$ is a subset of a set, 1-equivalent to $\mathcal {E}_1$, where two sets are 1-equivalent, if their symmetric difference has no more than 1 element. Thus S is a precomplete class in F. Obviously, $\{f_{U},f_{\lnot },f_{\sim },f_{\vee },f_{\wedge }\} \subseteq S$. On the other hand, since the constant function with value $-1$ is expressible as $f_{\lnot } \circ f_{\sim } \circ f_U$, from Lemma 2 and the definition of $x^{[y]}$ it follows that each $f \in S$ can be expressed as a composition of elements of $\{f_{U},f_{\lnot },f_{\sim },f_{\vee },f_{\wedge }\}$ and of projections $\pi _k^n(x_1,...,x_n)=x_k$ ($n \ge 1$, $k = 1,2,...,n$). Thus S is the functional closure of $\{f_{U},f_{\lnot },f_{\sim },f_{\vee },f_{\wedge }\}$.    $\square$

Lemma 4

The set of all short functions from F is the functional closure of the set $\{f_T,f_F,f_{U},f_{\lnot },f_{\wedge },f_{\sim }\}$, where $f_{F}, f_{U}, f_{T} \in F^{(0)}$, $f_{\lnot },f_{\sim } \in F^{(1)}$, $f_{\wedge } \in F^{(2)}$, $f_F=-1$, $f_{U}=0$, $f_{T}=1$, $f_{\lnot }(x) = -x$, $f_{\sim }(x) = 1-|x|$, $f_{\wedge }(x,y) = \min (x,y)$.

Proof

From the equalities $f_{\sim }(0)=1$, $f_{\lnot }(f_{\sim }(0))=-1$ and the De-Morgan law it follows that the set $\{f_T,f_F,f_{U},f_{\lnot },f_{\wedge },f_{\sim }\}$ has the same functional closure as the set $\{f_{U},f_{\lnot },f_{\sim },f_{\vee },f_{\wedge }\}$ (where $f_{\vee }(x,y) = \max (x,y)$), which is the set of all short functions from F by Lemma 3.    $\square$

Lemma 5

For each $P, Q:D \,\tilde{\rightarrow }\,\{T,F\}$ and $d \in D$ we have:

$\varPhi (\bot )(d) = 0$

$\varPhi (\lnot P)(d) = -(\varPhi (P)(d))$

$\varPhi (\sim P)(d) = 1 - |\varPhi (P)(d)|$

$\varPhi (P \vee Q)(d) = \max (\varPhi (P)(d), \varPhi (Q)(d))$

$\varPhi (P \wedge Q)(d) = \min (\varPhi (P)(d), \varPhi (Q)(d))$

Proof

Follows immediately from the definition $\varPhi$ and operations $\lnot , \sim , \vee , \wedge$ on partial predicates.   $\square$

Lemma 6

The problem (1)–(2) has an optimal solution on $F^{(n)}$ if and only if $p_0$ is continuous in the initial topology on D induced by $p_1,...,p_n$ (where the codomain of $p_i$, i.e. X, is considered as a discrete space).

Proof

“If”: assume that $p_0$ is continuous in the initial topology on D induced by $p_1,...,p_n$. Then there exists $f \in F^{(n)}$ such that $p_0(d)=f(p_1(d),...,p_n(d))$ for all $d \in D$. Then since the set $F^{(n)}$ is finite, the problem (1)–(2) has an optimal solution on $F^{(n)}$.

“Only if”: assume that the problem (1)–(2) has an optimal solution $f \in F^{(n)}$. Then $p_0(d)=f(p_1(d),...,p_n(d))$ for all $d \in D$, so $p_0$ is continuous in the initial topology on D induced by $p_1,...,p_n$.    $\square$

Lemma 7

If the problem (1)–(2) has an optimal solution on $F^{(n)}$, then this solution is unique.

Proof

Assume that the problem (1)–(2) has optimal solutions $f, g \in F^{(n)}$. Then $||f|| = ||g||$ and $f(p_1(d),...,p_n(d))=p_0(d)=g(p_1(d),...,p_n(d))$ for all $d \in D$.

Suppose that $f \ne g$. Then there exists $\bar{x}^* = (x_1^*,...,x_n^*) \in X^n$ such that $f(\bar{x}^*) \ne g(\bar{x}^*)$.

Consider the case when $f(\bar{x}^*) \ne 0$. Let us define a function $h \in F^{(n)}$ as follows: $h(\bar{x}) = f(\bar{x})$, if $\bar{x} \ne \bar{x}^*$, and $h(\bar{x})=0$, if $\bar{x} = \bar{x}^*$. Then for all $d \in D$, $(p_1(d),...,p_n(d)) \ne \bar{x}^*$, so $h(p_1(d),...,p_n(d))=p_0(d)$. Moreover, $||h|| = ||f||-|f(\bar{x}^*)|=||f||-1<||f||$ which contradicts the assumption that f is an optimal solution of (1)–(2).

Consider the case when $f(\bar{x}^*) = 0$. Then $|g(\bar{x}^*)| = 1$. Let us define a function $h \in F^{(n)}$ as follows: $h(\bar{x}) = g(\bar{x})$, if $\bar{x} \ne \bar{x}^*$, and $h(\bar{x})=0$, if $\bar{x} = \bar{x}^*$. Then for all $d \in D$, $(p_1(d),...,p_n(d)) \ne \bar{x}^*$, so $h(p_1(d),...,p_n(d))=p_0(d)$. Moreover, $||h|| = ||g||-|g(\bar{x}^*)|=||g||-1<||g||$ which contradicts the assumption that g is an optimal solution of (1)–(2).

Thus $f=g$. So if the problem (1)–(2) has an optimal solution on $F^{(n)}$, then this solution is unique.    $\square$

Lemma 8

Let $f \in M^{(n)}$, $g \in F^{(n)}$ and $g(\bar{x}) \in \{f(\bar{x}), 0\}$ for each $\bar{x} \in X^n$. Then $g \in M^{(n)}$.

Proof

Let $\bar{x}, \bar{y} \in X^n$. Consider the following cases.

• (1) $g(\bar{x}) = f(\bar{x}), g(\bar{y})=f(\bar{y})$. Then $|g(\bar{x})-g(\bar{y})| = |f(\bar{x})-f(\bar{y})| \le \rho (\bar{x}, \bar{y})$.

• (2) $g(\bar{x}) = f(\bar{x}), g(\bar{y})=0$. Then $|g(\bar{x})-g(\bar{y})| = |f(\bar{x})| \le \rho (\bar{x}, \bar{y})$, if $\bar{x} \ne \bar{y}$, and $|g(\bar{x})-g(\bar{y})| = 0 \le \rho (\bar{x}, \bar{y})$, if $\bar{x} = \bar{y}$.

• (3) $g(\bar{x}) =0, g(\bar{y})=f(\bar{y})$. Then $|g(\bar{x})-g(\bar{y})| = |f(\bar{y})| \le \rho (\bar{x}, \bar{y})$, if $\bar{x} \ne \bar{y}$, and $|g(\bar{x})-g(\bar{y})| = 0 \le \rho (\bar{x}, \bar{y})$, if $\bar{x} = \bar{y}$.

• (4) $g(\bar{x})=0$, $g(\bar{y})=0$. Then $|g(\bar{x})-g(\bar{y})| \le \rho (\bar{x}, \bar{y})$.

Thus $g \in M^{(n)}$.    $\square$

Lemma 9

The problem (1)–(2) has an optimal solution on $M^{(n)}$ if and only if it has an optimal solution on $F^{(n)}$ which belongs to $M^{(n)}$.

Proof

“If”: assume that the problem (1)–(2) has an optimal solution $f \in F^{(n)}$ which belongs to $M^{(n)}$. Then $f(p_1(d),p_2(d),...,p_n(d))=p_0(d)$ for all $d \in D$. Moreover, for each $g \in M^{(n)}$ such that $g(p_1(d),p_2(d),...,p_n(d))=p_0(d)$ for all $d \in D$, we have $g \in F^{(n)}$, so $||f|| \le ||g||$. So f is an optimal solution of (1)–(2) on $M^{(n)}$.

“Only if”: assume that the problem (1)–(2) has an optimal solution f on $M^{(n)}$. Then $f(p_1(d),p_2(d),...,p_n(d))=p_0(d)$ for all $d \in D$. Then since $F^{(n)}$ is finite, the problem (1)–(2) has an optimal solution on $F^{(n)}$. By Lemma 7, the problem (1)–(2) has a unique optimal solution of $F^{(n)}$. Denote it as g. Then $g(p_1(d),p_2(d),...,p_n(d))=p_0(d)$ for all $d \in D$ and $||g|| \le ||f||$. Let us define a function $h \in F^{(n)}$ as follows: for each $\bar{x} \in X^n$, $h(\bar{x}) = f(\bar{x})$, if $g(\bar{x}) \ne 0$, and $h(\bar{x})=g(\bar{x})$, if $g(\bar{x})=0$. Then for all $d \in D$, $h(p_1(d),...,p_n(d))=p_0(d)$. Moreover, $h \in M^{(n)}$ by Lemma 8. Then $||h|| = ||f||$, so for each $\bar{x}$ such that $g(\bar{x})=0$ we have $f(\bar{x}) = 0$. Then $||f|| \le ||g||$. Since $||g|| \le ||f||$ as mentioned above, we have $||f||=||g||$. The f is an optimal solution of (1)–(2) on $F^{(n)}$ and f belongs to $M^{(n)}$.    $\square$

Now we can give a proof of Theorem 1.

Proof

(of Theorem 1). “If”: assume that the problem (1)–(2) has an optimal solution on the set $F^{(n)}$ which is a short function. Denote by f such a solution. Then we have $p_0(d) = f(p_1(d),p_2(d),...,p_n(d))$ for all $d \in D$. By Lemma 3, f belongs to the functional closure of $\{f_{U},f_{\lnot },f_{\sim },f_{\vee },f_{\wedge }\}$, where the functions $f_{\cdot }$ are defined as in Lemma 3. From Lemma 5 it follows that $p_0(d) = \varPhi (P)(d)$ for all $d \in D$ for some predicate $P:D\,\tilde{\rightarrow }\, \{T,F\}$ expressible in the algebra $(D \,\tilde{\rightarrow }~\{T,F\}; \vee , \wedge , \lnot , \sim , \bot , P_1, P_2,..., P_n)$. Since $n\ge 1$ and the predicate $\bot$ can be expressed as $\sim P_1 \wedge \sim \sim P_1$, we conclude that P is expressible in the algebra $APr_{P_1,...,P_n}(D)$. Then $\varPhi (P_0)(d)=\varPhi (P)(d)$ for all $d \in D$. Then the definition of $\varPhi$ implies that $P_0 = P$, so $P_0$ is expressible in $APr_{P_1,...,P_n}(D)$.

“Only if”: assume that a predicate $P_0$ is expressible in algebra $APr_{P_1,...,P_n}(D)$. Then Lemma 5 implies that $\varPhi (P_0)(d)=f(\varPhi (P_1)(d),\varPhi (P_2)(d),...,\varPhi (P_n)(d))$ for all $d \in D$ for some function $f \in F^{(n)}$ which belongs to the functional closure of $\{f_{U},f_{\lnot },f_{\sim },f_{\vee },f_{\wedge }\}$, where the functions $f_{\cdot }$ are defined as in Lemma 3. Then by Lemma 3, f is a short function and $p_0(d)=f(p_1(d),...,p_n(d))$ for all $d \in D$. Then since $M^{(n)} \subseteq F^{(n)}$ is a finite set, the problem (1)–(2) has an optimal solution on the set $M^{(n)}$. Then Lemma 9 implies that the problem (1)–(2) has an optimal solution on $F^{(n)}$ which is a short function.    $\square$

Note that the problem (1)–(2) has the following addition property.

Lemma 10

If the problem (1)–(2) has an optimal solution on $M^{(n)}$, then this solution is unique.

Proof

Assume that f, g are optimal solutions of (1)–(2) on $M^{(n)}$. Then by Lemma 9, (1)–(2) has an optimal solution on $F^{(n)}$ which belongs to $M^{(n)}$. By Lemma 7 this solution is unique. Denote it as h. Then $||h|| \le ||f||$ and $||h|| \le ||g||$. Then h is an optimal solution of (1)–(2) on $M^{(n)}$ and $||h||=||f||=||g||$. Then f, g are optimal solutions of (1)–(2) on $F^{(n)}$. Then by Lemma 7, $f = g$.    $\square$

6 Proof of Theorem 3

First, let us prove auxiliary lemmas.

Lemma 11

Let V and $W \ne \emptyset$ be sets, $Q \in QPr^V_W$, and $v \in V$. Then

$$\begin{aligned} \sim (\exists v~Q) = (\exists v (\sim Q)) \wedge (\forall v (\sim Q \vee \lnot Q)). \end{aligned}$$

Proof

Let us fix $d \in V \,\tilde{\rightarrow }\, W$ and consider the following cases.

• 1. Assume that $(\sim (\exists v Q))(d)\downarrow = T$. Then $(\exists v Q)(d)\uparrow$, so there exists $a \in W$ such that $Q(d\nabla ^v a)\uparrow$ and there is no $b \in W$ such that $Q(d\nabla ^v b)\downarrow = T$. Then $(\sim Q)(d\nabla ^va)\downarrow = T$, so $(\exists v(\sim Q))(d)\downarrow =T$. Moreover, for each $b \in W$, either $Q(d\nabla ^v b)\uparrow$, or $Q(d \nabla ^v b)\downarrow = F$, so either $(\sim Q)(d \nabla ^v b)\downarrow =T$, or $(\lnot Q)(d \nabla ^v b)\downarrow =T$, whence $(\sim Q \vee \lnot Q)(d\nabla ^v b) \downarrow = T$. Hence $(\forall v (\sim Q \vee \lnot Q))(d) \downarrow = T$. Thus $((\exists v (\sim Q)) \wedge (\forall v (\sim Q \vee \lnot Q)))(d)\downarrow = T$.

• 2. Assume that $(\sim (\exists v Q))(d)\uparrow$. Then $(\exists v Q)(d)\downarrow$. Then either there exists $a \in W$ such that $Q(d\nabla ^v a)\downarrow =T$, or $Q(d\nabla ^v b)\downarrow =F$ for all $b \in W$.

  • 2.1. Consider the case when there exists $a \in W$ such that $Q(d\nabla ^v a)\downarrow =T$. Then $(\sim Q)(d\nabla ^v a)\uparrow$ and $(\sim Q \vee \lnot Q)(d \nabla ^u a) \uparrow$. Note that $(\sim Q \vee \lnot Q)(d \nabla ^u b)$ is not false for any $b \in W$, since $(\sim Q)(d \nabla ^u b)$ cannot be false. Then $(\forall v (\sim Q \vee \lnot Q))(d) \uparrow$. Besides, $(\exists v (\sim Q))(d)$ is not false, since $(\sim Q)(d\nabla ^v a)\uparrow$. Then $((\exists v (\sim Q)) \wedge (\forall v (\sim Q \vee \lnot Q)))(d)\uparrow$.

  • 2.2. Consider the case when $Q(d\nabla ^v b)\downarrow =F$ for all $b \in W$. Then $(\exists v (\sim Q))(d)\uparrow$ (since $W \ne \emptyset$). Moreover, $(\sim Q \vee \lnot Q)(d \nabla ^u b)\downarrow = T$ for all $b \in W$. Then $(\forall v (\sim Q \vee \lnot Q))(d)\downarrow = T$. Hence $((\exists v (\sim Q)) \wedge (\forall v (\sim Q \vee \lnot Q)))(d)\uparrow$.

Since $(\sim (\exists v Q))(d)$ cannot be false for any d, we conclude that $(\sim (\exists v Q))(d) \cong ((\exists v (\sim Q)) \wedge (\forall v (\sim Q \vee \lnot Q)))(d)$ for all $d \in V \,\tilde{\rightarrow }\, W$.

Thus $\sim (\exists v Q) = (\exists v (\sim Q)) \wedge (\forall v (\sim Q \vee \lnot Q))$.    $\square$

Corollary 1

Let V and $W \ne \emptyset$ be sets, $Q \in QPr^V_W$, $u, v \in V$, $u \ne v$, and u is unessential for Q. Then $\sim (\exists v~Q) = \forall u \exists v (\sim Q \wedge (\sim R^{u}_v(Q) \vee \lnot R^{u}_v(Q)))$.

The proof follows immediately from Lemma 11 by renaming the right-most bound variable v to u.

Lemma 12

Let V and $W \ne \emptyset$ be sets, $Q \in QPr^V_W$, and $v \in V$. Then

$$\begin{aligned} \sim (\forall v~Q) = (\exists v (\sim Q)) \wedge (\forall v (\sim Q \vee Q)). \end{aligned}$$

Proof

By taking into account Lemma 11 and that $\forall v~Q=\lnot \exists v(\lnot Q)$, $\lnot \lnot Q = Q$, and $\sim (\lnot Q) =~\sim Q$, we have:

$$\sim (\forall v~Q) = \sim (\lnot \exists v~(\lnot Q)) = \sim (\exists v~(\lnot Q)) $$

$$=(\exists v (\sim (\lnot Q))) \wedge (\forall v (\sim (\lnot Q) \vee \lnot \lnot Q)) =(\exists v (\sim Q)) \wedge (\forall v (\sim Q \vee Q)).$$

   $\square$

Corollary 2

Let V and $W \ne \emptyset$ be sets, $Q \in QPr^V_W$, $u, v \in V$, $u \ne v$, and u is unessential for Q. Then $\sim (\forall v~Q) = \forall u\exists v(\sim Q \wedge (\sim R^u_v(Q) \vee R^u_v(Q))).$

The proof follows immediately from Lemma 12 by renaming the right-most bound variable v to u.

Proof

(Of Theorem 3). “If”: By Theorem 2, P is expressible in the algebra $APr_{P_1,...,P_l}(V \,\tilde{\rightarrow }\, W)$, where $P_j = R^{\bar{u}_j}_{\bar{v}_j}(Q_{n_j})$ for $j=1,2,...,l$. Then it is easy to see that $\mathfrak {Q}^k_{m,\bar{v}} (P)$ is expressible in $AQPr_{Q_1,...,Q_n}(V,W)$. Thus $Q_0$ is expressible in $AQPr_{Q_1,...,Q_n}(V,W)$.

“Only if”: Assume that $Q_0$ is expressible in the algebra $AQPr_{Q_1,...,Q_n}(V,W)$. From Corollary 1 and Corollary 2 given above, and elementary properties of $\lnot$, $\vee$, $\wedge$, $\exists u$, $\forall u$ and renomination [20], it is easy to see (by using a process analogous to the process of construction of the prenex normal form in the classical first-order logic) that there exists a predicate P expressible in $ARPr_{Q_1,...,Q_n}(V,W)$ such that $Q_0=\mathfrak {Q}^k_{m,\bar{v}}(P)$ for some integers $k \ge 0$, $m \in [0,2^k-1]$ and a tuple $\bar{v} \in V^k$. Since renomination distributes with $\vee$, $\wedge$, $\lnot$, and $\sim$ [20] (e.g. $R^{\bar{u}}_{\bar{v}}(P_1 \vee P_2) = R^{\bar{u}}_{\bar{v}}(P_1) \vee R^{\bar{u}}_{\bar{v}}(P_2)$), and the composition of renominations is again a renomination (i.e. $R^{\bar{u}}_{\bar{v}}(R^{\bar{u}'}_{\bar{v}'}(P))$ is equal to $R^{\bar{u}''}_{\bar{v}''}(P)$ for some $\bar{u}'', \bar{v}''$), there exists an integer $l \ge 1$, finite sequences of integers $k_j \ge 1$ and $n_j \in [1,n]$ for $j=1,2,...,l$, and finite sequences of tuples $\bar{u}_j \in V^{k_j}_{\ne }$, $\bar{v}_j \in V^{k_j}$ for $j=1,2,...,l$ such that P is expressible in $APr_{Q^1,...,Q^l}(V \,\tilde{\rightarrow }\, W)$, where $Q^j = R^{\bar{u}_j}_{\bar{v}_j}(Q_{n_j})$ for $j=1,2,...,l$. Then by Theorem 2, P is short w.r.t. $R^{\bar{u}_j}_{\bar{v}_j}(Q_{n_j})$ for $j=1,2,...,l$.    $\square$

7 Conclusion

We have investigated the expressibility of partial predicates in the Kleene algebra with predicate complement and have given a necessary and sufficient condition of this expressibility in terms of the existence of an optimal solution of an optimization problem. We have also investigated expressibility in the first-order Kleene algebra with predicate complement. The obtained results may be useful for software verification using an extension of the Floyd-Hoare logic for partial pre- and postconditions and “weak triple” interpretation.