{"id":"d742af1c-b91d-4778-a096-a9fd382fa5d5","arxiv_id":"2502.01295","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"SHACL, ShEx, and PG-Schema are recast on a single common graph model, and their shared core CoGSL is shown to be expressible in all three.","lead":"The paper gives formal definitions of the core of three graph schema languages, SHACL, ShEx, and PG-Schema, all placed on one shared graph model. Its comparison identifies the languages' common core and proves that core can be written in each language, helping users choose and translate between schema languages.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Claim 1 (ShEx abstraction equivalent to non-recursive standard ShEx) is explicitly unproved and load-bearing for all ShEx comparisons.","rationale":"The reader's conditional verdict is well-supported. I focused on the exact place where the central claim would fail. Proposition 1 itself is proven in detail (Appendix E), and the lemmas are constructive and plausible. However, Proposition 1 only shows that common schemas can be expressed in the paper's SHACL and ShEx abstractions, not in the standardized languages. For SHACL, Appendix B cites prior detailed correspondence [24]; for ShEx, the correspondence is Claim 1, explicitly unproved. The translations in C.4.5/C.4.6 are not obviously wrong: they handle intervals, extra, and closed modifiers via constructions that match standard practice. But the extra-elimination step (C.4.4) changes the neighbourhood language in a subtle way: it adds te*_q sub-expressions that allow extra triples only when they do not match existing constraints. If this construction is incomplete, e.g., for nested shapes or inverse predicates, the claimed equivalence fails. Similarly, the PG-Schema abstraction admits 'it is not hard to show' reductions for node/edge types and edge-type tests; these are not formal proofs. A concrete differential test against an existing ShEx implementation would settle Claim 1 empirically, though a proof-assistant formalization would be stronger. Because these gaps are explicitly acknowledged and localized, they do not warrant rejection, but they justify CONDITIONAL acceptance. I therefore leave the verdict unchanged.","tokens_in":38176,"tokens_out":14439,"duration_ms":132725,"concrete_test":"Differential test: implement the paper's ShEx semantics (Definition 6, Tables 3-4) and the s-ShEx semantics of [8] on common graphs, translate non-recursive s-ShEx schemas to ShEx using Tables 8-10 (including the extra-elimination of C.4.4), and check graph-validity equivalence on a suite of randomly generated schemas with extra/closed modifiers and random common graphs; any mismatch invalidates Claim 1. Alternatively, formalize the two translation lemmas in a proof assistant and prove semantic preservation, with the extra-elimination construction in C.4.4 as the critical case.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central comparison rests on Claim 1 (Appendix C): the paper's ShEx abstraction is expressively equivalent to non-recursive standard ShEx (s-ShEx) on common graphs. The paper states this claim is presented without a correctness proof, and the translations in C.4.5/C.4.6 rely on non-trivial steps: (i) the elimination of 'extra' from s-ShEx shapes (C.4.4), which rewrites te with te*_q constructions that must preserve the neighbourhood language; and (ii) the closed/open translation, which must correctly encode the semantics of closed and extra in the generative triple-expression formalism. A bug in either direction would mean Proposition 1's ShEx translation and all expressiveness separations (Examples 9-10, Proposition 2) are about a language that is not actual ShEx. The same unproved-reduction pattern appears for PG-Schema (Appendix D.3 uses 'it is not hard to show' for simulating node/edge types and eliminating edge-type tests), so two of the three language abstractions have fidelity gaps. Of these, Claim 1 is the most load-bearing because the paper itself flags it as unproved and because ShEx is used as the baseline for two of the three expressiveness separations.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a common graph data model and recasts non-recursive SHACL, ShEx, and PG-Schema as shape-based formalisms over this model. It then defines CoGSL, a fragment intended to capture the functionalities shared by the three languages, and proves (Proposition 1, Appendix E) that every common schema can be translated into equivalent SHACL and ShEx schemas. The appendices relate the paper's abstractions to the actual standards: Appendix B discusses SHACL deviations, Appendix C claims expressive equivalence between the paper's ShEx and non-recursive standard ShEx, and Appendix D compares shape-based PG-Schema with original PG-Schema. The central value of the paper is thus a formal framework for comparing the three schema languages and for explaining their common core.","tokens_in":38352,"tokens_out":6841,"duration_ms":65932,"significance":"If the fidelity claims hold, this is a valuable reference formalization for a community that currently lacks a uniform basis for comparing SHACL, ShEx, and PG-Schema. The paper's strengths are its precise definitions, the detailed constructive translations in Appendix E, the explicit running example expressed in all three formalisms, and the honest discussion of where the abstractions deviate from the standards. The proof of Proposition 1 is given in full, with per-lemma translations for SHACL and ShEx. However, the paper explicitly leaves the ShEx-to-standard-ShEx equivalence unproved, and the PG-Schema fidelity rests on informal 'it is not hard to show' reductions; these are load-bearing for the claim that CoGSL is a common core of the actual languages rather than merely of the paper's abstractions.","major_comments":[{"comment":"The central fidelity claim for ShEx is explicitly presented without a correctness proof. The text states that the semantics-preservation of the translations between non-recursive s-ShEx and the paper's ShEx 'is presented without a correctness proof', and the surrounding sections rely on this claim: Section 4 and Appendix C.5 use the ShEx abstraction for the expressiveness separations in Examples 9 and 10 and in Proposition 2. If the extra-elimination rewriting in C.4.4 or the closed/open encodings in C.4.5 and C.4.6 do not preserve validity, then the comparison is with a language that is not actual ShEx. The manuscript must supply a formal s-ShEx semantics and a semantic-preservation proof for each translation rule, or else explicitly restate which claims concern the abstraction rather than standard ShEx.","section":"Appendix C, Claim 1"},{"comment":"The faithfulness of the shape-based PG-Schema abstraction is asserted through informal reductions rather than proved. Section 5 says the abstraction 'faithfully captures the expressive power of the original PG-Schema' up to the query language, and Section 6 uses this abstraction to define CoGSL. The simulations in D.3.1 (node-type and edge-type coverage constraints) and D.3.2 (elimination of edge-type tests in path expressions, including the case analysis for negated edge types) are described as 'not hard to show' and 'not hard to see'. These reductions need precise statements and proofs; without them, the claim that CoGSL is common to the actual languages is unsupported for PG-Schema.","section":"Appendix D, especially D.3.1-D.3.2"},{"comment":"The paper itself notes in D.3.5 that the restriction to single-atom formulas 'limits the expressive power of PG-Schema'. This directly qualifies the 'faithfully captures' statement made in Section 5. If shape-based PG-Schema is strictly weaker than PG-Schema on Common Graphs, then Proposition 1's translations target a restricted abstraction. The paper should state precisely in which direction the equivalence with original PG-Schema is claimed, and should make explicit that features such as Key constraints and multi-variable counting are excluded from the common core by construction rather than because they are absent from the other two languages.","section":"Section 5 and Appendix D.3.5"}],"minor_comments":[{"comment":"The predicate 'hasAcccess' appears to be a typo for 'hasAccess'; please correct it consistently in the text and figures.","section":"Section 2.1 and Figure 1"},{"comment":"The sentence 'The semantics of PG-Schemas is defned just like in Section 2.4' contains a typo: 'defned' should be 'defined'.","section":"Definition 11"},{"comment":"The text says 'We show in Section C.4.2 that the two variants have equivalent expressive power,' but the section gives rewriting rules; please state the equivalence claim precisely and label the rules as such.","section":"Appendix C.4.1"},{"comment":"The proof of Lemma 1 is only a single sentence. Since the lemma underpins the ShEx/SHACL counting separation in Example 10, please expand the induction, especially for the semantics of triple expressions under disjoint union and repetition.","section":"Appendix C.5.2, Lemma 1"}],"recommendation":"major_revision","confidential_remarks":"The manuscript reads as a community-consensus document, and several load-bearing proof obligations are deferred with statements such as 'the claim is presented without a correctness proof' and 'it is not hard to show'. For a journal publication, these must be resolved in the submitted record rather than left as promises. The paper is a good fit for cs.DB and the formal framework is genuinely useful, but the unproved equivalence claims should be turned into theorems with proofs or the claims should be explicitly scoped to the abstractions."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is the first common formal framework for SHACL, ShEx, and PG-Schema, and it's a solid piece of work that deserves a serious referee. The common graph data model is simple and sensible; CoGSL is a clean fragment; Proposition 1's translations into SHACL and ShEx are detailed and credible; and the expressiveness separations (ShEx counts triples, SHACL counts nodes) are genuinely illuminating and come with proofs. The paper is also honest about its own gaps, which is why I trust it more, not less.\n\nThe real soft spot is Claim 1 in Appendix C: the equivalence between the paper's ShEx abstraction and non-recursive standard ShEx is stated without a correctness proof. The paper says so explicitly. That claim is load-bearing—if the abstraction is not faithful, then the ShEx translations and the expressiveness results are about a language that isn't actual ShEx. The same pattern appears for PG-Schema in Appendix D.3, where the reductions for node/edge types and edge-type tests are dismissed with 'it is not hard to show'. None of this invalidates the core framework, because CoGSL and Proposition 1 are defined internally and the proofs there hold up. But it does mean the paper's 'faithful capture of the standards' claim is currently a conjecture for two of the three languages.\n\nMy recommendation: accept for peer review, but the authors should either prove Claim 1 or explicitly scope the paper's claims to their own abstraction rather than standard ShEx. The PG-Schema reductions should get the same treatment. These are fixable in revision, and the paper's value—a common basis for comparing and translating the three languages—doesn't depend on those equivalence claims being true, only on them being clearly stated.\n\nFor the reading group: I'd bring it. It's a rare paper that lets you compare three languages on one sheet of paper, and the counting example (Example 10) is a great discussion trigger.","headline":"First common formal framework for the three graph schema languages; the load-bearing ShEx-to-standard equivalence is explicitly unproved and should be fixed or scoped.","tokens_in":39008,"tokens_out":2481,"would_cite":true,"duration_ms":22081,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Three graph schema languages are shown to share a single common core.","keywords":["SHACL","ShEx","PG-Schema","graph schema languages","common graph data model","schema validation","RDF","property graphs"],"falsifier":"Take any schema written in standard non-recursive ShEx (with shape names, extra predicates, closed shapes, and repetition intervals) and any common graph, and check whether the standard validation outcome matches the Section 4 abstraction; a single mismatch witness would refute Claim 1 and, with it, the ShEx half of Proposition 1.","tokens_in":37957,"feed_emoji":"🔗","tokens_out":7143,"duration_ms":62385,"temperature":0.7,"pith_summary":"The paper tries to establish that SHACL, ShEx, and PG-Schema — three schema languages built by different communities for different graph data models — can be studied on one common graph model, and that the functionality common to all three is exactly the language CoGSL. If true, any constraint written in CoGSL can be expressed in all three languages, with an explicit translation from CoGSL into SHACL and into ShEx. A reader would care because it replaces three apparently unrelated formalisms with one frame for comparing expressive power and for planning translations between RDF and property-graph schemas.","feed_headline":"Three graph schema languages are shown to share a single common core.","feed_subtitle":"A uniform data model plus a common-core language lets SHACL, ShEx, and PG-Schema be compared and translated.","key_machinery":"The Common Graph Data Model and the selector–shape pair are the two devices that carry the argument. A common graph is a pair $(E,\\rho)$ with $E$ a finite set of edges carrying predicates and $\\rho$ a finite-domain partial function assigning values to node–key pairs; a schema is a set of pairs $(\\mathit{sel},\\varphi)$ where $\\mathit{sel}$ selects focus nodes or values and $\\varphi$ is a shape, with a graph valid if every selected item satisfies its shape. On top of this, the paper defines CoGSL as a restricted grammar over PG-Schema whose shapes use only star-free path expressions, single-edge traversals, closed content types, and the closing operator $\\nexists\\neg P$, and proves the common-core property by translating CoGSL shapes into nested SHACL and ShEx shapes.","core_discovery":"The central claim is that a schema written in CoGSL, the Common Graph Schema Language, is exactly as strong as what SHACL, ShEx, and PG-Schema can all say about a graph. The paper defines a common graph as a finite set of predicate-labelled edges together with a partial function mapping node–key pairs to values, which embeds both RDF and property graphs, and recasts each language as a set of selector–shape pairs. It then proves, as Proposition 1, that every common schema has an equivalent SHACL schema and an equivalent ShEx schema. It also exhibits constraints that cannot cross the boundaries: ShEx counts triples rather than counting distinct nodes, so it cannot express SHACL-style counting of distinct ends of union paths, while SHACL and PG-Schema cannot express ShEx-style equality of counts of two edge labels; PG-Schema alone can quantify over all nodes with a universal selector. The upshot is a precise map of overlapping and distinctive functionality.","pith_inferences":["If Claim 1 of Appendix C were proved, CoGSL would also be a faithful common core for standard non-recursive ShEx; until then, the ShEx half of the comparison concerns the paper's abstraction rather than the standard language itself.","The selector–shape pair format is the same principle used in XML schema languages such as DTDs and Schematron, so the CoGSL grammar could plausibly be adapted to express a common core that spans XML and graph validators.","A practical test of the framework would be to implement the two Proposition 1 translations and check on a corpus of schemas that validation outcomes coincide; the proof sketches suggest the translations are simple enough to automate.","The common graph model deliberately omits node identity comparisons, edge properties, node labels, and parallel same-label edges, so the common-core result should not be read as a statement about schemas that rely on such features."],"forward_implications":["Every constraint expressible in CoGSL can be written in SHACL and in ShEx, so CoGSL can serve as a neutral notation for schema constraints that users know will carry over.","The three languages are not merely stylistic variants: ShEx's triple-counting semantics and the node-counting semantics of SHACL and PG-Schema give different expressive powers, so a schema must be chosen with the intended count in mind.","PG-Schema can close the entire graph by selecting all nodes with the true selector, whereas SHACL and ShEx schemas always leave some disconnected parts unconstrained, limiting what those languages can say about the whole dataset.","The common framework yields a written map of which constructs are safe to translate among the three languages and which are not, supporting future integration work and teaching."],"supporting_citations":[{"why":"W3C recommendation defining standard SHACL, the object of the Section 3 abstraction.","marker":"[27]"},{"why":"Supplies the formal ShEx semantics on RDF triples that the Section 4 abstraction is based on.","marker":"[8]"},{"why":"W3C Community Group report defining standard ShEx, the target of Claim 1's equivalence.","marker":"[43]"},{"why":"Defines original PG-Schema and the property graph model from which common graphs are distilled.","marker":"[2]"},{"why":"ShapeMaps, the selector–pair view of validation that the paper generalises to all three languages.","marker":"[42]"},{"why":"Shows how the formal SHACL abstraction corresponds to standard SHACL, used to justify the Section 3 formalisation.","marker":"[24]"},{"why":"Formal complexity and expressiveness analysis of ShEx, needed to argue that the abstraction preserves the language's semantics.","marker":"[50]"},{"why":"Analysis of SHACL features including the lemma about identity paths that supports the path-expression formalisation.","marker":"[7]"}],"fun_headline_variants":["One core to describe three graph schema languages","SHACL, ShEx, PG-Schema: same core, different dialects","CoGSL: the unified core of three graph schema systems","Common foundation revealed for three graph schema languages","Three schemas, one language: the core they all share"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The ShEx half of the common-core claim rests on Claim 1 in Appendix C — that the paper's ShEx abstraction is expressively equivalent to non-recursive standard ShEx on common graphs — which is asserted without a correctness proof; the PG-Schema comparison makes similarly informal reduction claims, so if any of these equivalences fails, the common core is not about the actual languages.","fun_headline_variants_meta":{"raw":{"variants":["One core to describe three graph schema languages","SHACL, ShEx, PG-Schema: same core, different dialects","CoGSL: the unified core of three graph schema systems","Common foundation revealed for three graph schema languages","Three schemas, one language: the core they all share"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000486,"raw_usage":{"total_tokens":2382,"prompt_tokens":917,"completion_tokens":1465,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":533,"completion_tokens_details":{"reasoning_tokens":1383}},"tokens_in":533,"tokens_out":1465,"duration_ms":12186,"temperature":1.0,"reasoning_tokens":1383,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T15:45:55.323583+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take any schema written in standard non-recursive ShEx (with shape names, extra predicates, closed shapes, and repetition intervals) and any common graph, and check whether the standard validation outcome matches the Section 4 abstraction; a single mismatch witness would refute Claim 1 and, with it, the ShEx half of Proposition 1.","supporting_citations":[{"cited_title":"Knublauch and D","cited_arxiv_id":null,"evidence_quote":"W3C recommendation defining standard SHACL, the object of the Section 3 abstraction."},{"cited_title":"Labra Gayo, and Eric G","cited_arxiv_id":null,"evidence_quote":"Supplies the formal ShEx semantics on RDF triples that the Section 4 abstraction is based on."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"W3C Community Group report defining standard ShEx, the target of Claim 1's equivalence."},{"cited_title":"2017.ShapeMap Structure and Language","cited_arxiv_id":null,"evidence_quote":"ShapeMaps, the selector–pair view of validation that the paper generalises to all three languages."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Shows how the formal SHACL abstraction corresponds to standard SHACL, used to justify the Section 3 formalisation."},{"cited_title":"Prud’hommeaux, and Harold R","cited_arxiv_id":null,"evidence_quote":"Formal complexity and expressiveness analysis of ShEx, needed to argue that the abstraction preserves the language's semantics."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Analysis of SHACL features including the lemma about identity paths that supports the path-expression formalisation."}],"review_version":1}