Categorical foundations for structured specifications in Z
Why this work is in the frame
A frame that forgets how it found something cannot be audited. These are the routes that admitted this work.
Bibliographic record
Abstract
Abstract In this paper we present a formalization of the <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi mathvariant="sans-serif">Z</mml:mi> </mml:math> notation and its structuring mechanisms. One of the main features of our formal framework, based on category theory and the theory of institutions, is that it enables us to provide an abstract view of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi mathvariant="sans-serif">Z</mml:mi> </mml:math> and its related concepts. We show that the main structuring mechanisms of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi mathvariant="sans-serif">Z</mml:mi> </mml:math> are captured smoothly by categorical constructions. In particular, we provide a straightforward and clear semantics for promotion, a powerful structuring technique that is often not presented as part of the schema calculus. Here we show that promotion is already an operation over schemas (and more generally over specifications), that allows one to promote schemas that operate on a local notion of state to operate on a subsuming global state, and in particular can be used to conveniently define large specifications from collections of simpler ones. Moreover, our proposed formalization facilitates the combination of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi mathvariant="sans-serif">Z</mml:mi> </mml:math> with other notations in order to produce heterogeneous specifications, i.e., specifications that are obtained by using various different mathematical formalisms. Thus, our abstract and precise formulation of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi mathvariant="sans-serif">Z</mml:mi> </mml:math> is useful for relating this notation with other formal languages used by the formal methods community. We illustrate this by means of a known combination of formal languages, namely the combination of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi mathvariant="sans-serif">Z</mml:mi> </mml:math> with <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi mathvariant="sans-serif">CSP</mml:mi> </mml:math> .
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
Full frame distilled prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. Learned from the 10,348 direct Codex labels and 10,348 direct Gemma labels. Candidate is the union of thresholded teacher heads; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels or direct frontier model labels.
Codex and Gemma teacher scores by category
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.000 | 0.000 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.000 | 0.000 |
| Bibliometrics | 0.000 | 0.000 |
| Science and technology studies | 0.000 | 0.000 |
| Scholarly communication | 0.000 | 0.000 |
| Open science | 0.000 | 0.000 |
| Research integrity | 0.000 | 0.000 |
| Insufficient payload (model declined to judge) | 0.000 | 0.000 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from it