Logics of conditional computations with errors

Abstract

The conditional operator \(\textbf{if } A \textbf{ then } S \textbf{ else } T \textbf{ fi}\) is a "Scheffer" for programming: McCarthy shoved that computable functions can be represented as recursive schemes using conditional expressions. This approach needs to consider errors. Thus in modern computer science data types are enriched by the error \(\bot\). This error is considered as fatal but in praxis many errors are recoverable. Thus we considered recoverable error \(\mathfrak{u}\) as fourth logical value and investigate logics of various disciplines to handle \(\mathfrak{u}\). Another logical interpretation of \(\mathfrak{u}\) is the unsolved problem \(\{\mathfrak{t},\mathfrak{f}\}\). This treatment of \(\{\mathfrak{t},\mathfrak{f}\}\) differs from usual as overdefined [Anderson et al., 2017]. Four disciplines of handling conditional statements and induced logics are considered. All they can be viewed as extensions of three-valued logics by lisp logic for fragment \(\mathfrak{t},\mathfrak{f},\bot\). Logic \(\textbf{if}_1\) of standard sequential computation is extension of lisp logic. Logic of parallel computations where \(\textbf{if}_2\ \mathfrak{u}\ \textbf{ then } \mathfrak{x} \textbf{ else } \mathfrak{x}\ \textbf{ fi}=\mathfrak{x}\) is extended \(\text{Ł}_3\). Logic of maximal conditional when \(\mathfrak{x}\) occurring in both alternatives is accepted: \(\textbf{if}_3\ \mathfrak{u}\ \textbf{ then } \mathfrak{z} \textbf{ else } \mathfrak{y}\ \textbf{ fi}=\mathfrak{x}\) is extended Pcont. Logic of Prolog where \(\textbf{if}_4\ \mathfrak{u}\) is the first occurring definite value \(\mathfrak{t},\ \mathfrak{f}\) has its own implication and negation but is equivalent to logic of \(\textbf{if}_3\). Operators \(\textbf{if}_3\) and \(\textbf{if}_4\) are logically complete: each continuous in \(\{\mathfrak{t},\mathfrak{f}, u, \bot\}\) function is expressible. Operators \(\textbf{if}_2\) and \(\textbf{if}_3\) induce strategies for parallel and distributed processes. \(\textbf{if}_1\) corresponds to traditional sequential programs, \(\textbf{if}_4\) to Prolog.