Towards Verifiable Declarative Mappings: A Vision Paper

Declarative mapping languages such as RML improve the quality of knowledge graph construction by providing an abstraction layer through a domain-specific language. This language allows the user to focus on the mapping task without dealing with the minutiae of writing transformations in a full programming languages, thus improving the quality of the mapping. However, they do not formally guarantee correctness of the resulting knowledge graph, e.g., w.r.t. graph shapes: it is not guaranteed that every constructed graph will adhere to a set of given shapes. Consequently, a time-consuming validation step has to be applied after generation, and bugs in the knowledge graph construction are caught only late in the development process. In this paper, we present our vision of validated-by-construction knowledge graphs: By giving declarative mapping languages a verifiable semantics in terms of a functional language, we are able to use program logics to verify whether the mapping ensures correctness w.r.t. given graph shapes. We present an example how RML and SHACL can be given a formal semantics as OCaml functions and gospel specification and verify that the shape indeed ensures correctness. We furthermore describe how we envision a functional semantics for declarative languages to systematically enable verifiable mappings, and how this semantics related to existing semantics.