In the 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 suficient condition of this expressibility in terms of the existence of an optimal solution of an optimization problem. The obtained results may be useful for development of (semi-)automatic deduction tools for an extension of the Floyd-Hoare logic for the case of partial pre- and postconditions.
Floyd-Hoare logic [1, 2] is a logic which is useful for proving partial correctness of sequential programs. It is based on properties of triples (assertions) of the p f {q}, where f is a program and p, q are predicates which specify preform { } and post-conditions. An assertion of this kind means that if the program’s input d satisfies the pre-condition p, and the program terminates on d, the program’s output satisfies the post-condition q. In the classical Floyd-Hoare logic the program is allowed to be non-terminating (or have an undefined result of execution), but the pre- and postconditions are assumed to be always defined (have a well defined truth value). In the presence of pre- and postconditions defined by partial predicates (which can be undefined on some data) the inference rules (in particular, the sequence rule) of the classical Floyd-Hoare logic become unsound p f {q} is understood in the following way: if a precondi[13, 14], when a triple { } tion p is defined and true on the program’s input, and the program f terminates with a result y, and the postcondition q is defined on y, then q is true on y.
In the previous works [15, 3, 4, 10, 12, 11, 8] we investigated an inference system for an extension of Floyd-Hoare logic which remains sound in the case of partial pre- and postconditions, assuming the above mentioned interpretation of Floyd-Hoare triples. The formulations of the rules of this inference system, however, require introduction of a new composition into the logical language used to express pre- and postconditions. Whereas the formulation of the rules of the classical Floyd-Hoare logic depends on the usual boolean compositions (¬, ∧) of pre- and postcondition predicates (which are assumed to be total), the mentioned extension depends on the compositions of negation (¬) and conjunction (∧) of partial predicates defined in accordance with the tables of Kleene’s strong 3-valued logic, and on one additional unary composition of partial predicates which we call the composition of predicate complement and denote as ∼. This composition extends the signature of the Kleene algebra of partial predicates [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 suficient condition of this expressibility in terms of the existence of an optimal solution of a special constrained optimization problem. The obtained results may be useful for development of (semi-)automatic deduction tools for the mentioned extension of the Floyd-Hoare logic for the case of partial pre- and postconditions. 2
We will use the following notation. The notation f : A→˜ B means that f is a partial function on a set A with values in a set B, and f : A → B means that f is a total function from A to B. For a function f : A→˜ B: – f (x) ↓ means that f is defined on x; – f (x) ↓= y means that f is defined on x and f (x) = y; – f (x) ↑ means that f is undefined on x; – dom(f ) = {x ∈ A | f (x) ↓} is the domain of a function.
We will denote as f1(x1) ∼= f2(x2) the strong equality, i.e. f1(x1) ↓ if and only if f2(x2) ↓, and if f1(x1) ↓, then f1(x1) = f2(x2).
The symbols T, F will denote the “true” and ”false” values of predicates.
We will denote Bool = {T, F }. The symbol ⊥ will denote a nowhere defined partial predicate.
Let D 6= ∅ be a set, and P0, P1, ... Pn be partial predicates on D.
Let AP rP1,...,Pn (D) = (D→˜ {T, F }; ∨, ∧, ¬, ∼, P1, P2, ..., Pn) be an algebra of partial predicates with constants P1, ..., Pn, where 1. ∨, ∧, ¬ are the operations of disjunction, conjunction and negation on partial predicates defined in accordance with Kleene’s strong three-valued logic as follows:
T, if P (d) ↓= T or Q(d) ↓= T ; (P ∨ Q)(d) = F, if P (d) ↓= F and Q(d) ↓= F ; undefined in other cases .
T, if P (d) ↓= T and Q(d) ↓= T ; (P ∧ Q)(d) = F, if P (d) ↓= F or Q(d) ↓= F ; undefined in other cases .
T, if P (d) ↓= F ; (¬P )(d) = F, if P (d) ↓= T ;
undefined in other case . 2. ∼ is the unary operation of predicate complement: (∼ P )(d) = (T,
if P (d) ↑; undefined , if P (d) ↓ .
We will call AP rP1,...,Pn (D) the Kleene algebra of partial predicates on D with predicate complement and constants P1, ..., Pn. 3
Let F (n) be the set of all n-ary functions (operations) f : {−1, 0, 1}n → {−1, 0, 1}. The elements of F (n) will represent functions of 3-valued logic P3 (where 1 corresponds to the “true” value and −1 corresponds to the “false” value, and 0 is an intermediate truth value).
Let F = Sn≥0 F (n).
We will denote as xˉ = (x1, x2, ..., xn) a tuple of values xi ∈ {−1, 0, 1}. Let us consider {−1, 0, 1}n as a metric space with Chebyshev distance: n ρn((x1, ..., xn), (y1, ..., yn)) = mi=a1x |xi − yi|.
We will say that a function f ∈ F (n) is short, if it is a short map, i.e. if for all xˉ, yˉ we have
|f (xˉ) − f (yˉ)| ≤ ρn(xˉ, yˉ).
For any predicate P : D →˜{T, F } denote by Φ(P ) a function D → {−1, 0, 1} such that for all d ∈ D:
1, if P (d) ↓= T, Φ(P )(d) = 0, if P (d) ↑, −1, if P (d) ↓= F.
Let D 6= ∅ be a set, P1, P2, ..., Pn : D→˜ {T, F } be partial predicates, and
AP rP1,...,Pn (D) = (D→˜ {T, F }; ∨, ∧, ¬, ∼, P1, P2, ..., Pn).
Let pi = Φ(Pi) for i = 0, 1, 2, ..., n.
Denote ||f || = Pxˉ∈{−1,0,1}n |f (xˉ)| for f ∈ F (n) and consider the following (constrained) optimization problem1:
||f || → min
f (p1(d), p2(d), ..., pn(d)) = p0(d), d ∈ D
(
¬x = −x ∼ x = 1 − |x| x[y] = x,
if y = 1 ∼ x, if y = 0 ¬x, if y = −1 Lemma 1. ρn(xˉ, yˉ) = 1 − minin=1 xi[yi] for every n ≥ 1 and xˉ, yˉ ∈ {−1,0,1}n. Proof. It is easy to see that for all x,y ∈ {−1,0,1}: Then ρn(xˉ, yˉ) = maxin=1 |xi − yi| = maxin=1(1 − x[iyi]) = 1 − minin=1 x[iyi]. tu Consider {−1,0,1} as a lattice with operations: x[y] = 1 − |x − y| x ∨ y = max(x,y); x ∧ y = min(x,y).
Below we will assume that in expressions involving operations on {−1,0,1} the operation x[y] has the highest priority, and is followed (by priority) by the usual, among ∧,∨, the operation ∧ has higher priority. unary operations ¬, ∼
, which are followed by the binary operations ∧ and ∨. As Lemma 2. For each short function f ∈ F(n) and xˉ ∈ {−1,0,1}n: f(xˉ) = fˆ(xˉ) ∧ f6=0(xˉ) ∨ ¬f6=0(xˉ) (Wyˉ:f(yˉ)=1 Vin=1 x[iyi], if ∃yˉ f(yˉ) = 1 otherwise f6=0(xˉ) =
0, Proof. It is easy to see that for each x,y ∈ {−1,0,1}: (Wyˉ:f(yˉ)6=0 Vin=1 ∼ (x[iyi]∧ ∼ x[iyi])∧ ∼∼ x[iyi], if ∃yˉ f(yˉ) 6= 0 . otherwise. where Then ∼ (x[y]∧ ∼ x[y])∧ ∼∼ x[y] = (1, if x = y
0, if x 6= y. f6=0(xˉ) = (1, if f(xˉ) 6= 0
0, if f(xˉ) = 0.
By Lemma 1, fˆ(xˉ) ∧ f6=0(xˉ) ∨ ¬f6=0(xˉ) = (fˆ(xˉ) ∧ 0) ∨ 0 = 0.
If f (xˉ) = 1, then fˆ(xˉ) = 1 and f6=0(xˉ) = 1, so fˆ(xˉ) ∧ f6=0(xˉ) ∨ ¬f6=0(xˉ) = 1.
Thus so fˆ(xˉ) ∧ f6=0(xˉ) ∨ ¬f6=0(xˉ) = −1.
If f (xˉ) = −1, then for each yˉ such that f (yˉ) = 1 we have ρn(xˉ, yˉ) ≥ |f (xˉ) − f (yˉ)| = 2 which implies that 1−ρn(xˉ, yˉ) = −1. Then fˆ(xˉ) = −1 and f6=0(xˉ) = 1, f4(x, y) = min(x, y).
Lemma 3. The set of all short functions from F is a precomplete class in F and
is the functional closure of the set {f0, f1, f2, f3, f4}, where f0 ∈ F (0), f1, f2 ∈
F (
F can be alternatively characterized as a of the sets Qn function {−1, 0, 1}n i=1{0, ai}, where a1, ..., an ∈ {−1, 1}n. In the terminology of [18], → {−1, 0, 1} (n ≥ 0) which does not change sign on each
f (xˉ) = fˆ(xˉ) ∧ f6=0(xˉ) ∨ ¬f6=0(xˉ).
Lemma 4. For each P, Q : D→˜ {T, F } and d ∈ D we have: {f0, f1, f2, f3, f4} ⊆
S. On the other hand, since the constant function with Thus S is the functional closure of {f0, f1, f2, f3, f4}. value −1 is expressible as f1 ◦ f2 ◦ f0, from Lemma 2 and the definition of it follows that each f ∈ S can be expressed as a composition of elements of such functions correspond to the precomplete class T 3 the image of the product of sets, 1-equivalent to E1 is a subset of a set, 1equivalent to E1, where two sets are 1-equivalent, if their symmetric diference has no more than 1 element. Thus S is a precomplete class in F . Obviously, E1,1 of functions for which Φ(⊥)(d) = 0 Φ(¬P )(d) = −(Φ(P )(d)) Φ(∼ P )(d) = 1 − |Φ(P )(d)| Φ(P ∨ Q)(d) = max(Φ(P )(d), Φ(Q)(d)) Φ(P ∧ Q)(d) = min(Φ(P )(d), Φ(Q)(d)) partial predicates.
Proof. Follows immediately from the definition Φ and operations ¬, ∼, ∨, ∧ on
Let M (n) be the set of all short functions from F (n).
tu
tu
Lemma 5. The problem (
Proof. “If”: assume that p0 is continuous in the initial topology on D induced
by p1, ..., pn. Then there exists f ∈ F (n) such that p0(d) = f (p1(d), ..., pn(d)) for
all d ∈ D. Then since the set F (n) is finite, the problem (
“Only if”: assume that the problem (
Then g ∈ M (n).
Lemma 7. Let f ∈ M (n), g ∈ F (n) and g(xˉ) ∈ {f (xˉ), 0} for each xˉ ∈ {−1, 0, 1}n. |g(xˉ) − g(yˉ)| = 0 ≤ ρ(xˉ, yˉ), if xˉ = yˉ. |g(xˉ) − g(yˉ)| = 0 ≤ ρ(xˉ, yˉ), if xˉ = yˉ.
Thus g ∈ M (n).
4) g(xˉ) = 0, g(yˉ) = 0. Then |g(xˉ) − g(yˉ)| ≤ ρ(xˉ, yˉ). that f (xˉ∗) 6= g(xˉ∗).
Proof. Assume that the problem (
Suppose that f 6= g. Then there exists xˉ∗ = (x1∗, ..., x∗n) ∈ {−1, 0, 1}n such
solution of (
Consider the case when f (xˉ∗) 6= 0. Let us define a function
follows: h(xˉ) = f (xˉ), if xˉ 6= xˉ∗, and h(xˉ) = 0, if xˉ = xˉ∗. Then for all d ∈ D,
(p1(d), ..., pn(d)) 6= xˉ∗, so h(p1(d), ..., pn(d)) = p0(d). Moreover, ||h|| = ||f || −
|f (xˉ∗)| = ||f || − 1 < ||f || which contradicts the assumption that f is an optimal
h ∈ F (n) as
tu
tu
tu
is an optimal solution of (
Consider the case when f (xˉ∗) = 0. Then |g(xˉ∗)| = 1. Let us define a function h ∈ F (n) as follows: h(xˉ) = g(xˉ), if xˉ 6= xˉ∗, and h(xˉ) = 0, if xˉ = xˉ∗. Then for all d ∈ D, (p1(d), ..., pn(d)) 6= xˉ∗, so h(p1(d), ..., pn(d)) = p0(d). Moreover, ||h|| = ||g|| − |g(xˉ∗)| = ||g|| − 1 < ||g|| which contradicts the assumption that g
Thus f = g. So if the problem (
Proof. Let xˉ, yˉ ∈ {−1, 0, 1}n. Consider the following cases.
1) g(xˉ) = f (xˉ), g(yˉ) = f (yˉ). Then |g(xˉ) − g(yˉ)| = |f (xˉ) − f (yˉ)| ≤ ρ(xˉ, yˉ). 2) g(xˉ) = f (xˉ), g(yˉ) = 0. Then |g(xˉ) − g(yˉ)| = |f (xˉ)| ≤ ρ(xˉ, yˉ), if xˉ 6= yˉ, and 3) g(xˉ) = 0, g(yˉ) = f (yˉ). Then |g(xˉ) − g(yˉ)| = |f (yˉ)| ≤ ρ(xˉ, yˉ), if xˉ 6= yˉ, and f belongs to M (n).
M (n).
Proof. “If”: assume that the problem (
g(p1(d), p2(d), ..., pn(d)) = p0(d) for all d ∈ D and ||g|| ≤ ||f ||. Let us define a
function h ∈ F (n) as follows: for each xˉ ∈ {−1, 0, 1}n, h(xˉ) = f (xˉ), if g(xˉ) 6= 0,
and h(xˉ) = g(xˉ), if g(xˉ) = 0. Then for all d ∈ D, h(p1(d), ..., pn(d)) = p0(d).
Moreover, h ∈ M (n) by Lemma 7. Then ||h|| = ||f ||, so for each xˉ such that
g(xˉ) = 0 we have f (xˉ) = 0. Then ||f || ≤ ||g||. Since ||g|| ≤ ||f || as mentioned
above, we have ||f || = ||g||. The f is an optimal solution of (
Now we can give a proof of the main Theorem 1 from the previous section.
Proof (of Theorem 1). “If”: assume that the problem (
≥ 1 and the predicate ⊥ can be expressed as ∼ P0 = P , so P0 is expressible in AP rP1,...,Pn (D).
P1∧ ∼∼ P1, we conclude that P is expressible in the algebra AP rP1,...,Pn (D).
Then Φ(P0)(d) = Φ(P )(d) for all d ∈ D. Then the definition of Φ implies that
“Only if”: assume that a predicate P0 is expressible in algebra AP rP1,...,Pn (D).
M (n)
Then Lemma 4 implies that Φ(P0)(d) = f (Φ(P1)(d), Φ(P2)(d), ..., Φ(Pn)(d)) for
all d ∈ D for some function f ∈ F (n) which belongs to the functional closure
of {f0, f1, f2, f3, f4}, where fi are defined as in Lemma 3. Then by Lemma 3,
f is a short function and p0(d) = f (p1(d), ..., pn(d)) for all d ∈ D. Then since
⊆ F (n) is a finite set, the problem (
Note that the problem (
Proof. Assume that f, g are optimal solutions of (
In this example of application of the main result of the paper we will use the notation and terminology of the composition-nominative approach to program formalization [16, 17] and [7, 6, 5].
Let v be a fixed name, V = {v}, A = {T, F }.
Let D = V A be the set of named sets on V which take values in A. Then Let P1 be a partial predicate on D such that
D = {[], [v 7→ T ], [v 7→ F ]}.
P1(d) ∼= (v ⇒ (d)) P0(d) = (T, if v ⇒ (d) ↑;
F, if v ⇒ (d) ↓ . where v ⇒ is the denaming operation [16, 17] (which has undefined value, if v ∈/ dom(d)).
Let P0 be a partial predicate on D such that
AP rP1 (D) = (D→˜ {T, F }; ∨, ∧, ¬, ∼, P1).
if Pi(d) ↑, −1, if Pi(d) ↓= F.
Let pi : D → {−1, 0, 1}, i = 0, 1 be functions such that
1, if Pi(d) ↓= T, pi(d) = 0, Then
1, p1(d) = 0, if v ⇒ (d) ↓= T, if v ⇒ (d) ↑, −1, if v ⇒ (d) ↓= F. −1, if v ⇒ (d) ↓= T, p0(d) = 1, if v ⇒ (d) ↑,
−1, if v ⇒ (d) ↓= F.
The initial topology on D induced by p1 is the power set of D, so p0 is continuous. We have p0({d ∈ D | p1(d) = −1}) = {−1} p0({d ∈ D | p1(d) = 0}) = {1} p0({d ∈ D | p1(d) = 1}) = {−1} Then a function with the graph
{(−1, −1), (
AP rP1 (D) = (D→˜ {T, F }; ∨, ∧, ¬, ∼, P1).
We have investigated the question of expressibility of partial predicates in the Kleene algebra extended with the composition of predicate complement and have given a necessary and suficient condition of this expressibility in terms of the existence of an optimal solution of a special optimization problem. The obtained results may be useful for development of (semi-)automatic deduction tools for an extension of the Floyd-Hoare logic for the case of partial pre- and postconditions.