Abstract
Spatial logics are used to reason locally about disjoint data structures. They consist of standard first-order logic constructs, spatial (structural) connectives and their corresponding adjuncts. Lozes has shown that the adjuncts add no expressive power to a spatial logic for analysing tree structures, a surprising and important result. He also showed that a related logic does not have this adjunct elimination property. His proofs yield little information on the generality of adjunct elimination. We present a new proof of these results based on model-comparison games, and strengthen Lozes’ results. Our proof is directed by the intuition that adjuncts can be eliminated when the corresponding moves are not useful in winning the game. The proof is modular with respect to the operators of the logic, providing a general technique for determining which combinations of operators admit adjunct elimination.
A preliminary version of this work was presented at the LICS’04 workshop LRPP.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
O’Hearn, P., Pym, D.: The logic of bunched implications. Bulletin of Symbolic Logic 5, 215–244 (1999)
Cardelli, L., Ghelli, G.: TQL: A query language for semistructured data based on the ambient logic. Mathematical Structures in Comp. Sci. 14, 285–327 (2004)
Cardelli, L., Gardner, P., Ghelli, G.: Manipulating trees with hidden labels. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 216–232. Springer, Heidelberg (2003)
Cardelli, L., Gordon, A.: Anytime, anywhere: modal logics for mobile ambients. In: Proc. of POPL 2000., pp. 365–377 (2000)
Ishtiaq, S., O’Hearn, P.: BI as an assertion language for mutable data structures. In: Proc. of POPL 2001., pp. 14–26 (2001)
Yang, H.: An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. In: Proc. of SPACE 2001 Workshop, London (2001)
Lozes, E.: Adjuncts elimination in the static ambient logic. In: Proc. of Express 2003, Marseille (2003)
Ebbinghaus, H.D., Flum, J.: Finite Model Theory, vol. 2. Springer, Heidelberg (1999)
Cardelli, L., Gordon, A.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Cardelli, L., Gordon, A.D.: Logical properties of name restriction. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 46–60. Springer, Heidelberg (2001)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing (2002)
Caires, L.: A specification logic for mobility. Technical Report 4/2000, DI/FCT/UNL (2000)
Caires, L., Cardelli, L.: A spatial logic for concurrency (Part I). In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 1–37. Springer, Heidelberg (2001)
Dawar, A., Ghelli, G., Gardner, P.: Adjunct elimination through games (unpublished)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dawar, A., Gardner, P., Ghelli, G. (2004). Adjunct Elimination Through Games in Static Ambient Logic. In: Lodaya, K., Mahajan, M. (eds) FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2004. Lecture Notes in Computer Science, vol 3328. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30538-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-30538-5_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24058-7
Online ISBN: 978-3-540-30538-5
eBook Packages: Computer ScienceComputer Science (R0)