Modeling the Interaction of Computer Errors by Four-Valued Contaminating Logics

Abstract

Logics based on weak Kleene algebra (WKA) and related structures have been recently proposed as a tool for reasoning about flaws in computer programs. The key element of this proposal is the presence, in WKA and related structures, of a non-classical truth-value that is “contaminating” in the sense that whenever the value is assigned to a formula $\phi$, any complex formula in which $\phi$ appears is assigned that value as well. Under such interpretations, the contaminating states represent occurrences of a flaw. However, since different programs and machines can interact with (or be nested into) one another, we need to account for different kind of errors, and this calls for an evaluation of systems with multiple contaminating values. In this paper, we make steps toward these evaluation systems by considering two logics, $\mathsf {HYB}_{1}$ and $\mathsf {HYB}_{2}$, whose semantic interpretations account for two contaminating values beside classical values 0 and 1. In particular, we provide two main formal contributions. First, we give a characterization of their relations of (multiple-conclusion) logical consequence—that is, necessary and sufficient conditions for a set $\varDelta$ of formulas to logically follow from a set $\varGamma$ of formulas in $\mathsf {HYB}_{1}$ or $\mathsf {HYB}_{2}$. Second, we provide sound and complete sequent calculi for the two logics.

Appendix

Proof of Lemma 1: We start with the LTR direction. Suppose that $\varGamma \vDash _{\mathcal {M}_{\mathsf {HYB}_{1}}}\varDelta$. This means that, if $v(\psi )\in \{0,n_{2}\}$ for every $\psi \in \varDelta$, then $v(\phi )\in \{0,n_{2}\}$ for some $\phi \in \varGamma$ and every $v\in \mathrm {Hom}_{\mathbf {Fml},\mathbf {HYB}}$. Given the behavior of $n_{2}$ w.r.t. negation, this implies that, if $v(\theta ) = \{1,n_{2}\}$ for every $\theta \in \varDelta ^{\lnot }$, then $v(\zeta ) = \{1,n_{2}\}$ for some $\zeta \in \varGamma ^{\lnot }$ and every $v\in \mathrm {Hom}_{\mathbf {Fml},\mathbf {HYB}}$. Since $\mathcal {D}_{\mathsf {HYB}_{2}} = \{1,n_{2}\}$, this implies $\varDelta ^{\lnot }\,\models _{\mathcal {M}_{\mathsf {HYB}_{2}}}\,\varGamma ^{\lnot }$. The RTL direction is proved along the very same lines. $\blacksquare$

Proof of Theorem 1: We start with the LTR direction. We first prove that if $\varGamma \,\models _{\mathsf {HYB}_{1}}\,\varDelta$, then $\varGamma '\,\models _{\mathsf {HYB}_{1}}\,\varDelta$ for at least a non-empty $\varDelta ' \subseteq \varDelta$ such that $var(\varDelta ')\ \subseteq var(\varGamma )$. Assume the antecedent as the initial hypothesis, and suppose that for every $\varDelta \subseteq \varDelta '$ such that $var(\varDelta ')\ \subseteq var(\varGamma )$. This implies that there is valuation $v\in \mathrm {Hom}_{\mathbf {Fml},\mathbf {HYB}}$ such that $v(\psi )\in \{n_{2},0\}$ for every $\psi \in \varDelta '$ and yet $v(\phi )\in \{1,n_{1}\}$ for every $\phi \in \varGamma$. By the contaminating behavior of $n_{2}$ from Table 2 and $var(\varDelta ')\subseteq var(\varGamma )$, this implies $v(\psi ) = 0$ for every $\psi \in \varDelta '$. More in general, we have $v(p) \ne n_{2}$ for every $p\in var(\varGamma )$, and by this, we have $v(q) \ne n_{2}$ for every $q\in var(\bigcup _{\varDelta '\in \mathbf {G}_{\varDelta ,\varGamma }})$. This implies that $v(\phi ) = \{n_{1},1\}$ for every $\phi \in \varGamma$. v can be extended to a valuation $v'\in \mathrm {Hom}_{\mathbf {Fml},\mathbf {HYB}}$ such that $v'(p) = v(p)$ if $p\in var(\varGamma )$, and $v'(p) = n_{2}$ otherwise. This implies that $v'(\phi ) \in \{1,n_{1}\}$ for every $\phi \in \varGamma$, $v'(\theta ) = n_{2}$ for every $\theta \in \varDelta \setminus \bigcup _{\varDelta '\in \mathbf {G}_{\varDelta ,\varGamma }}$, and $v(\psi ) = 0$ for every $\psi \in \varDelta$. But this in turn contradicts the initial hypothesis, given the definition of $\mathsf {HYB}_{1}$-consequence. Thus, we have that, if $\varGamma \,\models _{\mathsf {HYB}_{1}}\,\varDelta$, then $\varGamma \,\models _{\mathsf {HYB}_{2}}\,\varDelta '$ for at least a non-empty $\varDelta ' \subseteq \varDelta$ such that $var(\varDelta ')\ \subseteq var(\varGamma )$. Since $\mathsf {HYB}_{2}$ is a sublogic of $\mathsf {PWK}$, we conclude that $\varGamma \,\models _{\mathsf {HYB}_{1}}\,\varDelta$ implies $\varGamma \,\models _{\mathsf {PWK}}\,\varDelta '$ for at least a non-empty $\varDelta ' \subseteq \varDelta$ such that $var(\varDelta ')\ \subseteq var(\varGamma )$.

As for the RTL direction, assume as the initial hypothesis that $\varGamma \,\models _{\mathsf {PWK}}\,\varDelta '$ for at least a non-empty $\varDelta ' \subseteq \varDelta$ such that $var(\varDelta ')\ \subseteq var(\varGamma )$. To establish $\varGamma \,\models _{\mathsf {HYB}_{1}}\,\varDelta '$, fix any valuation $U\in \mathrm {Hom}_{}$ such that $v(\phi ) \in \{1,n_{1}\}$ for every $\phi \in \varGamma '$. Our goal is to show that $v(\psi ) \in \{1,n_{1}\}$ for some $\psi \in \varDelta$. We consider two cases:

Case (1): $v(\phi ) = n_{1}$ for some $\phi \in \varGamma$. Fix some formula $\theta \in \varGamma$ such that $v(\theta ) = n_{1}$. By the contaminating behavior of $n_{1}$ from Table 2, there is a $q\in var(\theta )$ such that $v(q)= n_{1}$. Remember that $var(\varDelta ')\subseteq var(\varGamma )$, and suppose that $q\in var(\varGamma )\cap var(\varDelta ')$. Since $var(\varDelta ')\subseteq var(\varGamma )$ and $v(p) \ne n_{2}$ for every $p\in var(\varGamma )$, we have $v(q) \ne n_{2}$ for every $q\in var(\varDelta ')$. Suppose now that $v(\phi ) \in \{1,n_{1}\}$ for every $\phi \in \varGamma$ and $v(\psi ) = 0$ for every $\psi \in \varDelta '$. This implies that there is a valuation $V\in \mathrm {Hom}_{}$ such that $v(\phi ) \in \{1,n_{\}}$ for every $\phi \in \varGamma$ and $v(\psi ) = 0$ for every $\psi \in \varDelta '$. But this contradicts the initial hypothesis that $\varGamma \,\models _{\mathsf {PWK}}\,\varDelta '$.

Case (2): $v(\phi ) \ne n_{1}$ for every $\phi \in \varGamma '$. This implies that $v(\phi ) = 1$ for every $\phi \in \varGamma$, and, by the contaminating behavior of $n_{1},n_{2}$ from Table 2, $v(p) = 1$ for every $p\in var(\varGamma )$. From this and $\varGamma \,\models _{\mathsf {CL}}\,\varDelta '$ (which follows from the initial hypothesis $\varGamma \,\models _{\mathsf {PWK}}\,\varDelta '$), we have that $v(\psi ) = 1$ for some $\psi \in \varDelta$, as desired.

Since these two cases are jointly exhaustive, we conclude $\varGamma \,\models _{\mathsf {HYB}_{1}}\,\varDelta '$. From this and the Definition of $\models _{\mathsf {HYB}_{1}}$, it follows that $\varGamma \,\models _{\mathsf {HYB}_{1}}\,\varDelta$. $\blacksquare$

Proof of Theorem 2: By Theorem 1 and Lemma 1. $\blacksquare$

Proof of Theorem 3: Any initial sequent has the form in which $\varGamma$ and $\varDelta$ are empty and $\varGamma '=\varDelta '=\lbrace p\rbrace$. In this case, the sequent enjoys the property that:⁷

It can be easily checked that this property is preserved under each of the foregoing rules. The case of the Exchange and Contraction rules, and Weakening (outside the scope of the square brackets) can be noted to preserve this property, since they correspond to properties that are valid in every Tarskian logic and $\mathsf {HYB}_{1}$ is a Tarskian logic, as every matrix logic is—see [19]. We notice that this property is preserved by the other rules as follows. Moreover, this can also be checked to apply straightforwardly to the “push” rules and the operational rules (in- and outside the square brackets). Hence, any derivable sequent enjoys the above tripartite property.

Now, we know that $\varXi \vDash _{\mathcal {M}_{\mathsf {HYB}_{2}}}\varTheta$ if and only if there exists a $\varXi '\subseteq \varXi$ and a $\varTheta '\subseteq \varTheta$ such that $Var(\varXi ')\subseteq Var(\varTheta ')\subseteq Var(\varXi )$ and $\varXi '\vDash _{\mathcal {M}_{\mathsf {CL}}}\varTheta '$. Because of soundness of $\mathbf {LK}$ (a presentation of which is described in [8]), the above tripartite property entails validity in $\mathcal {M}_{\mathsf {HYB}_{2}}$. Soundness of $\mathsf {HYB}_{2}$ with respect to $\mathcal {M}_{\mathsf {HYB}_{1}}$ is proved by similar reasoning. $\blacksquare$

Proof of Lemma 2: Assume $\varGamma \vDash _{\mathcal {M}_{\mathsf {HYB}_{2}}} \varDelta$. Then by Corollary 1 for $\mathcal {M}_{\mathsf {HYB}_{2}}$, we know that there are $\varGamma ' \subseteq \varGamma$, $\varDelta ' \subseteq \varDelta$, with $Var(\varGamma ')\subseteq Var(\varDelta ')\subseteq Var(\varGamma )$ and $\varGamma ' \vDash _{\mathcal {M}_{\mathsf {CL}}} \varDelta '$. By completeness of $\mathbf {LK}$, this implies that $\varGamma '\Rightarrow \varDelta '$ is provable in $\mathbf {LK}$. We also know that $Var(\varGamma ')\subseteq Var(\varDelta ')$. Hence, by [8, Lemma 21], these two observations jointly imply that $\varGamma '\Rightarrow \varDelta '$ is provable in the sequent calculus for $\mathsf {PWK}$. $\blacksquare$

Proof of Theorem 4: Assume that $\varGamma \vDash _{\mathcal {M}_{\mathsf {HYB}_{2}}}\varDelta$. Then, by Lemma 2, there is a $\mathsf {PWK}$ proof of $\varGamma '\Rightarrow \varDelta '$. Call this proof, i.e. a rooted binary tree, $\varPi$. We can design an algorithm to transform a $\mathsf {PWK}$ proof of this sequent into an $\mathsf {HYB}_{1}$ proof of .

First, replace every node $\varXi \Rightarrow \varTheta$ of $\varPi$ by a node . Then, place below each leaf, or axiom node, one instance of [Weak], such that from an axiom we infer in one step the sequent . After that, for each non-axiom node place $\varGamma$ to the left of the square brackets in the antecedent and $\varDelta$ to the left of the square brackets in the succedent. In the resulting proof, each $\mathsf {PWK}$ rule is applied within the scope of the square brackets. Moreover, we can check that every application of a $\mathsf {PWK}$ rule corresponds to a “bracketed rule” in $\mathsf {HYB}_{1}$ that respects the corresponding provisos.

Actually, since Weakening is not fully admissible within the scope of square brackets, something must be said about this case. Suppose in an H proof of $\varGamma '\Rightarrow \varGamma '$ there is an ineliminable application of Weakening that allows to go from a node $\varXi \Rightarrow \varTheta$ to a node $\varXi ,\varXi '\Rightarrow \varTheta ,\varTheta '$—whence we can legitimately call $\varXi '$ and $\varTheta '$ the active (sets of) formulas in this step. Then the current algorithm can be further specified by saying that if $\varPi$ is a proof which has no ineliminable application of Weakening, then we proceed as previously stated. However, if $\varPi$ has an ineliminable application of Weakening, then we enlarge every node (outside the square brackets) with $\varGamma$ and $\varXi '$, and $\varDelta$ and $\varTheta '$, in their respective sides. Finally, when the $\varPi$ requires the corresponding application of Weakening, we mimic this in $\mathsf {HYB}_{1}$ applying the [PushL] and [PushR] rules to $\varXi '$ and $\varTheta '$, as needed.

This renders a rooted binary tree $\varPi ^{*}$ with as its terminal sequent. We then proceed to apply the rules [PushL], [PushR] followed by elimination of duplicate formulas in $\varGamma '$ and $\varDelta '$. We end up with a $\mathsf {HYB}_{1}$ proof ending with , for which $\varGamma ''\cup \varGamma '=\varGamma$ and $\varDelta ''\cup \varDelta '=\varDelta$ and $Var(\varGamma ')\subseteq Var(\varDelta ')\subseteq Var(\varGamma ''\cup \varGamma ')=\varGamma$. $\blacksquare$

Proof of Theorem 5: By Theorem 3 and Lemma 1. $\blacksquare$

Proof of Theorem 6: By Theorem 4 and Lemma 1. $\blacksquare$