Context logic and tree update
Seminar Room 1, Newton Institute
Spatial logics have been used to describe properties of tree-like structures (Ambient Logic) and in a Hoare style to reason about dynamic updates of heap-like structures (Separation Logic). A natural question is whether the Ambient Logic can be used to reason about tree update (XML update). Calcagno, Zarfaty and I have shown that this is not possible. Instead, we had to fundamentally change the way we reason about structured data by introducing Context Logic. Local data update typically identifies the portion of data to be replaced, removes it, and inserts the new data in the same place. With Context Logic, we can reason about both data and this place of insertion (contexts). We have shown that Context Logic can be used to develop local Hoare reasoning about tree update, heap update (analogous to Separation Logic reasoning), and term rewriting (which escaped reasoning using Separation Logic).
In this talk, I will motivate Context Logic using our local Hoare reasoning about tree update (XML update). However, my main goal is to explain some expressivity results. With our style of Hoare reasoning, certain so-called adjunct connectives play an essential role in describing the weakest preconditions (important for both the theory and tool development). These connectives can be eliminated in the tree case (without quantifiers). This result follows previous results on Separation Logic and Ambient Logic, by Lozes first and then Dawar, Gardner and Ghelli. Such results are interesting, since there is typically no simple translation from a formula to its adjunct-free equivalent and, in the case of the Ambient Logic with hiding, the task of finding the adjunct-free formulae is not computable.
Despite these elimination results, our intuition has always been that the adjunct connectives are essential for Hoare reasoning. The point is that the weakest preconditions are parametric with respect to a formula variable. We have recently developed inexpressibility results, which characterise what it means for a logic to be unable to express such parametric properties. We have not seen this style of parametric inexpressibility result before, and believe it is an important general concept that will be applicable to other styles of logical reasoning.