{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:24Z","timestamp":1753894404468,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Derived datasets can be defined implicitly or explicitly. An implicit\ndefinition (of dataset O in terms of datasets I) is a logical specification\ninvolving two distinguished sets of relational symbols. One set of relations is\nfor the \"source data\" I, and the other is for the \"interface data\" O. Such a\nspecification is a valid definition of O in terms of I, if any two models of\nthe specification agreeing on I agree on O. In contrast, an explicit definition\nis a transformation (or \"query\" below) that produces O from I. Variants of\nBeth's theorem state that one can convert implicit definitions to explicit\nones. Further, this conversion can be done effectively given a proof witnessing\nimplicit definability in a suitable proof system. We prove the analogous\nimplicit-to-explicit result for nested relations: implicit definitions, given\nin the natural logic for nested relations, can be converted to explicit\ndefinitions in the nested relational calculus (NRC). We first provide a\nmodel-theoretic argument for this result, which makes some additional\nconnections that may be of independent interest, between NRC queries,\ninterpretations, a standard mechanism for defining structure-to-structure\ntranslation in logic, and between interpretations and implicit to definability\n\"up to unique isomorphism\". The latter connection uses a variation of a result\nof Gaifman concerning \"relatively categorical\" theories. We also provide a\nproof-theoretic result that provides an effective argument: from a proof\nwitnessing implicit definability, we can efficiently produce an NRC definition.\nThis will involve introducing the appropriate proof system for reasoning with\nnested sets, along with some auxiliary Beth-type results for this system. As a\nconsequence, we can effectively extract rewritings of NRC queries in terms of\nNRC views, given a proof witnessing that the query is determined by the views.<\/jats:p>","DOI":"10.46298\/lmcs-20(3:7)2024","type":"journal-article","created":{"date-parts":[[2024,7,22]],"date-time":"2024-07-22T09:55:06Z","timestamp":1721642106000},"source":"Crossref","is-referenced-by-count":0,"title":["Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory"],"prefix":"10.46298","volume":"Volume 20, Issue 3","author":[{"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[]},{"given":"C\u00e9cilia","family":"Pradic","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Wernhard","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,7,22]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13964\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13964\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,22]],"date-time":"2024-07-22T09:55:07Z","timestamp":1721642107000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/10495"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,22]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(3:7)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2212.03085v6","asserted-by":"subject"},{"id-type":"arxiv","id":"2212.03085v5","asserted-by":"subject"},{"id-type":"arxiv","id":"2212.03085v4","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2212.03085","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2212.03085","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,7,22]]},"article-number":"10495"}}