On the almighty wand (Q418137)

This paper studies separation logic with one selector. Separation logic is a formalism for reasoning on linked lists. While a list will generally need two selectors, one to point to the next link and one for the data element, separation logic with one selector considers only the next link. Intuitively, in separation logic with one selector one reasons only on the list's structure and not on the list's content. NEWLINENEWLINENEWLINE NEWLINESeparation logic with two selectors is known to be undecidable [\textit{C. Calcagno} et al., Lect. Notes Comput. Sci. 2245, 108--119 (2001; Zbl 1052.68590)]. The authors address decidability, complexity, expressive power and minimality of first-order separation logic with one selector. NEWLINENEWLINENEWLINE NEWLINESeparation logic (SL) is interpreted over a memory state, which represents the memory state of a program manipulating lists. Formally, Loc is a countably infinite set of locations, which represents the set of addresses. The program variables are represented by a countably infinite set of variables Var. A memory state is then a pair \((s,h)\) (\textit{store} and \textit{heap}) such that \(s:\mathrm{Var}\to \mathrm{Loc}\) is a total function and \(h:\mathrm{Loc}\rightharpoonup \mathrm{Loc}\) a partial function with finite domain. Intuitively, Var represents the programming variables and \(s\) the variables' contents. Furthermore, the domain of \(h\) represents the set of addresses of allocated cells, while \(h(l)\) is the value held by the cell at address \(l\). NEWLINENEWLINENEWLINE NEWLINETwo heaps \(h_1, h_2\) are said to be disjoint if their domains are disjoint. In that case \(h_1*h_2\) represents the disjoint union of these two heaps. NEWLINENEWLINENEWLINE NEWLINEFormulas in first-order separation logic with one selector (SL) are built using the Boolean connectors, first-order quantification, equality and three further connectors denoted by \(\hookrightarrow\), \(*\) and \(-\!*\). SL is interpreted on memory states. For instance \((s,h)\) satisfies \(x\hookrightarrow y\) if \(h(s(x))=s(y)\). Furthermore \((s,h)\) satisfies \(\varphi_1*\varphi_2\) if there are two heaps \(h_1\), \(h_2\) such that \(h=h_1*h_2\), \((s,h_1)\models \varphi_1\) and \((s,h_2)\models \varphi_2\) hold. Finally \((s,h)\) satisfies \(\varphi_1-\!*\varphi_2\) if for every heap \(h'\) disjoint from \(h\), if \((s,h')\models \varphi_1\) then \((s,h'*h)\models \varphi_2\). The \(*\) connector is called \textit{the separating conjunction}, while \(-\!*\) is known as \textit{the separating implication} and also as \textit{the magic wand}. NEWLINENEWLINENEWLINE NEWLINEFurthermore, two fragments of SL are also considered: SL(\(*\)) and SL(\(-\!*\)), which are, respectively, the restrictions of SL without \(-\!*\) and without \(*\). NEWLINENEWLINENEWLINE NEWLINEThe authors finally consider second-order logic with second-order quantification on Loc. Besides Boolean connectors and first-order quantification, their second-order logic (SO) contains equality and the connective \(\hookrightarrow\). Two restrictions of this logic are considered: MSO, where second-order quantification is restricted to monadic (unary) variables, and DSO, where this quantification is restricted to binary second-order variables. NEWLINENEWLINENEWLINE NEWLINEThe major results of this paper are the following. SL's satisfiability problem is undecidable. Furthermore, there is equivalence in expressive power between SL(\(-\!*\)), SL, SO and DSO by logarithmic-space translations. The authors also show how to adapt their proofs to separation logic with \(k>1\) selectors. NEWLINENEWLINENEWLINE NEWLINEOn the other hand, the authors show that for SL(\(*\)) satisfiability is decidable, but with non-elementary recursive complexity (by reduction from the first-order theory of finite words). They furthermore also exhibit larger decidable fragments by restricting the use of \(-\!*\).