Path Predicate Modal Logic and its Comonadic Semantics

GOREN, GABRIEL; FIGUEIRA, SANTIAGO

Cambridge

Workshop; Structure Meets Power Workshop (ICALP 2022); 2022

University of Cambridge

The following work stems from an interest in exploring the applicability of the comonadicformalism [1] to data-aware logics. These are languages that reason on data-graphs studied inDatabase Theory, both exploring the topology of the structure and manipulating data-values.In particular, (in-)equality comparisons allow the expression of the data join, the mostimportant construct of a query language. This interest lead us to consider simple fragmentsof CoreDataXPath [4]; in particular, we focused on DataGL, a very simple data-aware logicto reason on data-trees, studied in [2] from a proof-theoretical point of view.DataGL captures a fragment of CoreDataXPath(↓+ ), and can be seen as a bi-modal logicwith the operators ♦= and ♦6= . However, multimodal logic cannot accommodate increasinglysophisticated fragments of CoreDataXPath such as those that express tests on intermediatesteps of a path. This lead us to consider DataGL as a particular case of a more generalfamily of logics that we call Path Predicate Modal Logic or PPML which, to the best of ourknowledge, have not been investigated.In this joint work with Santiago Figueira we introduce PPML and begin the developmentof its basic theory from the point of view of comonadic semantics.