Pith. sign in

REVIEW 2 major objections 4 minor 1 cited by

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics

T0 review · 2 major / 4 minor · reviewed 2026-08-08 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Synchronous sequential circuits, quotiented by observable behavior, are exactly the causal, finitely specified, bottom-preserving monotone stream functions, and operational and algebraic equivalence induce the same quotient.

desk verdict Solid, carefully-built categorical semantics for sequential circuits with non-delay-guarded feedback, but the headline isomorphism is conditional on functional completeness and is proven only for Belnap logic. read the letter →

arxiv 2502.08497 v1 pith:7XSIMEBT submitted 2025-02-12 cs.LO cs.PLmath.CTmath.LO

George Kaye This is my paper · ORCID
classification cs.LOcs.PLmath.CTmath.LO MSC 18M0568Q5568Q60
keywords sequentialcircuitsdenotationalsemanticsoperationalalgebraicstreamfunctionsMealymachinestracedmonoidalcategoriesBelnaplogic
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The thesis sets out to give synchronous sequential circuits a fully compositional meaning: a circuit's behavior should be fixed by its input/output interface, so circuits can be composed without inspecting their internals. It claims that every circuit determines a causal stream function (one whose $i$-th output depends only on inputs up to time $i$), that every causal, finitely specified, bottom-preserving ($\bot$-preserving) monotone stream function is realized by some circuit, and that three different semantic routes—denotational, operational, and algebraic—identify exactly the same pairs of circuits. If the claim holds, specifications, simulations, and equational optimizations of hardware are three views of one relation, and non-delay-guarded feedback no longer needs to be excluded from the theory.

What carries the argument

The central mechanism is a chain of traced PROPs. Circuits form the free symmetric traced monoidal category $\mathrm{SCirc}_{\Sigma}$, where the trace is feedback; monotone Mealy machines form a bridge category $\mathbf{Mealy}_I$; and stream functions form $\mathbf{Stream}_I$. The trace on $\mathbf{Stream}_I$ is computed as a least fixed point, supplied by the Kleene fixed-point theorem, and the unrolling rule for non-delay-guarded feedback uses the height of the value lattice as an iteration bound. For the Belnap four-valued logic (no signal, false, true, both), a functional-completeness argument lets every stream function be translated back into a circuit, completing the isomorphisms.

What would settle it

Take a finite value lattice and a gate set whose interpretations are all $\bot$-preserving and monotone but not functionally complete—for instance, monotone Boolean gates without a constant-true generator—and define the stream function that outputs true in every position regardless of input. If that constant stream behavior is not realizable by any circuit over the signature, the completeness half of the isomorphism fails for that interpretation.

Watch

Extended reading notes

Core claim

The load-bearing result is Corollary 4.100: the category $\mathrm{SCirc}_{\Sigma}$ of synchronous sequential circuits quotiented by denotational equivalence is isomorphic to the category $\mathbf{Stream}_I$ of causal, finitely specified, $\bot$-preserving monotone stream functions on the value lattice. The same quotient is isomorphic to the quotient by observational equivalence (circuits reduce to the same outputs for all inputs) and to the quotient by algebraic equivalence (circuits interderivable by the equations $E_I$). So, for a functionally complete interpretation, every circuit has a unique stream-function behavior, every such behavior is implemented by some circuit, and the operational and algebraic rules prove exactly the behavioral equalities.

Load-bearing premise

The interpretation of the gate set must be functionally complete: every $\bot$-preserving monotone function on the finite value lattice must be expressible as a circuit. The thesis proves this for the Belnap four-valued gates but not for arbitrary signatures, and without it the reverse direction of the isomorphism fails, leaving only soundness of the denotational semantics.

Editorial extensions

If this is right

  • Two circuits can be swapped freely in any context once their stream functions agree, so a library of verified components can be reused without re-verification.
  • The operational reduction strategy—global trace-delay form, Mealy form, then instant-feedback unrolling—gives a decision procedure for behavioral equivalence: reduce and compare output streams.
  • The algebraic equations are complete, so proof search for circuit identities can be organized as rewriting to a pseudo-normal form.
  • Every finitely specified causal monotone stream behavior is implementable and every implementation realizes exactly one such behavior, so specifications can be compiled to circuits without loss of behavior.
  • Non-delay-guarded feedback is handled instead of excluded, which keeps useful cyclic combinational circuits inside the theory.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural next question is to characterize, for arbitrary gate sets and value lattices, exactly when functional completeness holds; the gap between the Belnap case and a generic signature is where the full isomorphism either stands or falls.
  • The unrolling bound suggests a concrete complexity promise: evaluating a feedback loop on an $m$-bit value lattice needs at most $\mathrm{height}(V^m)+1$ iterations, which a simulator could measure directly.
  • The graph-rewriting machinery in the second half points toward an automatic proof assistant for circuits, where rewriting modulo traced comonoid structure implements the operational semantics as a hardware description language.
  • The same three-way semantic construction could be attempted for asynchronous or handshake circuits; a failure there would show which parts of the result depend on synchrony and the lattice order rather than on the categorical skeleton.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. Starting from a syntax of synchronous sequential circuits as morphisms of a freely generated traced monoidal category SCircΣ, the thesis develops three semantics: a denotational semantics into a category StreamI of causal, finitely specified, bottom-preserving monotone stream functions; an operational semantics based on global transformations followed by local reductions; and an algebraic semantics via a set of equations. The central technical result is Corollary 4.100, an isomorphism SCircΣ/≈I ≅ StreamI for functionally complete interpretations, obtained by passing through monotone Mealy machines, encoding states into words of values, and realizing every transition/output function as a normalized circuit. The second half of the thesis adapts hypergraph rewriting to traced comonoid structure and applies it to circuit rewriting and to a hardware description language.

Significance. The monograph is careful and unusually complete in its technical development: it proves directly that the proposed stream-function category is closed under taking least fixed points (Theorem 4.47), verifies the trace axioms (Theorem 4.48), constructs both directions of the Mealy-machine bridge, and proves functional completeness of the Belnap signature (Theorem 4.113). If the main theorem is accepted under its stated hypothesis, this is a substantial contribution to compositional circuit semantics, and the graph-rewriting part extends existing hypergraph string-diagram rewriting to a structure class that includes feedback. The proofs are paper-and-pencil and do not appear to be accompanied by machine-checked artifacts; the reader must therefore rely on the usual mathematical checking of the written argument.

major comments (2)
  1. [§4.4, Cor. 4.100; §4.5] The central isomorphism SCircΣ/≈I ≅ StreamI is proved only under the functional-completeness hypothesis of Definition 4.87. For an interpretation whose gate set is not functionally complete, Corollary 4.98 fails and only the soundness direction survives. For example, take the Belnap value lattice with P = {AND} together with the structural generators and value generators: the Belnap negation is a bottom-preserving monotone function V → V, so the pointwise-negation stream function belongs to StreamI, but no circuit over this signature can realize it, since the available operations generate the lattice-polynomial clone, which omits ¬ on the Belnap diamond. Thus the advertised 'fully compositional theory' is not a theorem for arbitrary circuit signatures; the abstract and Chapter 1 should state the completeness claim as conditional on functional completeness, and the generalized-circuit extension in Section 4.6 should state that it inherits the same restriction.
  2. [§4.1.1, Def. 4.14] The definition of a monotone function as 'x ≤_A y if and only if f(x) ≤_B f(y)' is the definition of an order embedding, not the standard notion of monotonicity used elsewhere in the paper (e.g., Definitions 4.15–4.18, Lemma 4.33, Theorem 4.47, and Theorem 4.113). Under the stated 'iff' definition, FuncI excludes constant functions and every non-injective monotone map; Lemma 4.93, for instance, is not justified, because a monotone Mealy encoding may map two different states to the same encoded value on some input and therefore is not an order embedding. The intended definition is almost certainly the one-way implication. Because monotonicity is a load-bearing hypothesis throughout the completeness argument, this definitional error should be corrected and all subsequent monotonicity statements should be re-checked against the corrected definition.
minor comments (4)
  1. [§4.3.2, Thm. 4.97] In the proof, the sentence 'To show that !I(−) = J−K^S_I ◦ !I(−)' should read 'To show that !I(−) = J−K^S_I ◦ ||−||^≤_I'; as written the right-hand side duplicates the left side and omits the Mealy-to-circuit map.
  2. [§4.6, Def. 4.121] There is a typo in 'moprhisms', which should be 'morphisms'.
  3. [§3.3, Rem. 3.15] The phrase 'minimum obervable duration' contains a typo; it should be 'minimum observable duration'.
  4. [§5.1, Lem. 5.11] The soundness of the (Mealy) rule is dismissed as 'a simple exercise'; since this rule is a global transformation central to the operational semantics, a short explicit justification (or a reference to the matching equations in Section 6) would help the reader.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the completeness isomorphism is conditional on an explicit functional-completeness hypothesis, proved for Belnap logic, and no fitted parameter or self-citation is doing the work.

full rationale

The derivation is self-contained in the relevant sense. StreamI is defined independently of circuit syntax (Definition 4.34: causal, finitely specified, bottom-preserving monotone stream functions), and the denotational semantics is a PROP morphism from the freely generated SCircSigma, so the semantic category is not defined as whatever the syntax does. The completeness direction (Corollary 4.98, Corollary 4.100) is explicitly conditional: after translating a stream function to its minimal Mealy machine (Corollary 4.71) and encoding states, the final step requires every bottom-preserving monotone function to be realizable as a circuit. That is precisely the stated hypothesis of functional completeness (Definition 4.87), and Section 4.5 discharges it for the Belnap interpretation by a constructive DNF argument (Theorem 4.113) using standard Boolean functional completeness. The thesis itself flags the limitation: 'For an interpretation to admit a sound and complete denotational semantics it needs to be functionally complete.' For a non-complete gate set the isomorphism would fail, leaving only soundness; this is a scope caveat, not a circular step. No parameters are fitted: the unrolling bound c is the length of the longest chain in the finite lattice (Definition 5.18), not tuned to match outputs. The operational and algebraic semantics are checked for soundness against the denotational model and then proved complete, rather than being defined as denotational equivalence in disguise. Self-citations to [GKS24] and [GK23] are provenance and refinement remarks, not unverified load-bearing premises, and the standard coalgebra and fixed-point facts are cited externally to Rutten, Tarski, and others. I therefore find no step in which a prediction or first-principles result reduces to its own input by construction.

Assumptions & free parameters 0 free parameters · 5 assumptions · 4 invented entities

The framework is parameterized by the value lattice and the functional-completeness condition; no numbers are fitted to data. The main new mathematical constructs (monotone Mealy machines, partial monogamous cospans, traced boundary complements) are definitions justified by theorems inside the thesis, not entities with external empirical support.

assumptions (5)
  • domain assumption Circuit values form a finite lattice with least element • and every primitive is interpreted as a ⊥-preserving monotone function (Definition 4.16)
    The denotational, operational, and algebraic semantics all assume the value set V with order ⊑ is a finite lattice and the primitive components are monotone and ⊥-preserving. This is stated in Section 4.1.1.
  • domain assumption The interpretation I is functionally complete (Definition 4.87)
    Completeness of the denotational semantics needs a circuit for every monotone function on V. The paper proves this for Belnap logic (Section 4.5) but assumes such a map ||-|| exists for general signatures; without it, SCircΣ/≈I ≅ StreamI does not hold.
  • standard math Kleene fixed-point theorem for Scott-continuous functions on pointed directed-complete posets (Theorem 4.39)
    Used to construct the trace on StreamI (Lemma 4.45, Theorem 4.47) and to justify the IF unrolling rule (Lemma 5.16).
  • standard math Axioms of symmetric monoidal, traced monoidal, and Frobenius categories, plus the theory of PROPs and string diagrams
    The entire framework is built on these categorical foundations, introduced in Chapter 2.
  • standard math Double pushout rewriting theory for (coloured) hypergraphs, including adhesivity properties
    Part II builds on DPO rewriting and the Bonchi et al. results on hypergraph string diagram rewriting (Section 8.1, Chapter 9).
invented entities (4)
  • Monotone Mealy machine
    purpose: Bridge between circuits and causal stream functions; underlies the completeness proof of the denotational semantics
    Defined in Section 4.2.2 as an (A,B)-Mealy machine whose state space is a poset and whose transition/output functions are ⊥-preserving monotone. It has no experimental handle outside this paper; its justification is internal theorems.
  • Category of partial monogamous cospans of hypergraphs (PMCsp_D(Hyp_Σ))
    purpose: Represents traced monoidal terms as hypergraph cospans, enabling rewriting modulo traced structure
    Introduced in Section 8.5 as the cospan category between monogamous acyclic and Frobenius cospans. Internal to the paper.
  • Traced boundary complement / traced left-boundary complement
    purpose: Characterizes which pushout complements correspond to valid term rewrites for traced and traced-comonoid structures
    Defined in Chapter 9; used to characterize valid DPO rewriting contexts. No external falsifiable consequence.
  • Category of partial left-monogamous cospans (PLMCsp_D(Hyp_Σ))
    purpose: Cospan representation of traced comonoid terms for sequential circuits
    Introduced in Section 8.6. Internal.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics." pith.science (2026). https://pith.science/paper/7XSIMEBT

@misc{pith2026250208497,
  author       = {Pith},
  title        = {Pith review of: Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7XSIMEBT}},
  note         = {Machine review of arXiv:2502.08497}
}
read the original abstract

This thesis details a project to define a fully compositional theory of synchronous sequential circuits built from primitive components, motivated by applying techniques successfully used in programming languages to hardware. The first part of the thesis defines the syntactic foundations of sequential circuit morphisms, and then builds three different semantic theories: denotational, operational and algebraic. We characterise the denotational semantics of sequential circuits as certain causal stream functions, as well as providing a link to existing circuit methodologies by mapping between circuit morphisms, stream functions and Mealy machines. The operational semantics is defined as a strategy for applying some global transformations followed by local reductions to demonstrate how a circuit processes a value, leading to a notion of observational equivalence. The algebraic semantics consists of equations for bringing circuits into a pseudo-normal form, and then encoding between different state sets. This part of the thesis concludes with a discussion of some novel applications, such as those for using partial evaluation for digital circuits. While mathematically rigorous, the categorical string diagram formalism is not suited for reasoning computationally. The second part of this thesis details an extension of string diagram rewriting with hypergraphs so that it is compatible with the traced comonoid structure present in the category of digital circuits. We identify the properties that characterise cospans of hypergraphs corresponding to traced comonoid terms, and demonstrate how to identify rewriting contexts valid for rewriting modulo traced comonoid structure. We apply the graph rewriting framework to fixed point operators as well as the operational semantics from the first part, and present a new hardware description language based on these theoretical developments.

Figures

Figures reproduced from arXiv: 2502.08497 by the authors.

Figure 1.1
Figure 1.1. A circuit of forks and joins with no other primitives [PITH_FULL_IMAGE:figures/full_fig_p011_1_1.png] view at source ↗
Figure 1.2
Figure 1.2. An analog circuit, using a voltmeter, an inductor, a capacitor, a resistor, and a voltage source as primitive components; and a digital circuit, using NAND gates as primitive components analog circuits requires manipulating equations relating quantities such as voltage, current and resistance; in a parallel line of work to our own, analog circuits have already been given a compositional mathematical treatment [BS22]… view at source ↗
Figure 1.3
Figure 1.3. Three types of composition: sequential, parallel (tensor) and using a trace operator 𝑓 = 𝑔 ℎ = 𝑔 𝑘 [PITH_FULL_IMAGE:figures/full_fig_p012_1_3.png] view at source ↗
Figures from the paper (52 more)
Figure 1.4
Figure 1.4. Figure 1.4: Decomposing a large circuit 𝑓 into smaller circuits 𝑔 and 𝑘 clock signal, whereas in asynchronous circuits the state changes as soon as the inputs do. The latter type of circuits is useful when speed is of the essence, but are harder to design because small differenc…
Figure 1.5
Figure 1.5. Figure 1.5: Example of a string diagram properties of composition; for this, we turn to category theory [Mac78] . A category is made up of objects and morphisms (‘arrows’) between them. Any two arrows 𝑓 : 𝐴 → 𝐵 and 𝑔 : 𝐵 → 𝐶 can be composed to make a new morphism 𝑔 ◦ 𝑓 : 𝐴 → 𝐶, …
Figure 1.6
Figure 1.6. Figure 1.6: Example of diagrammatic equational reasoning by ‘yank [PITH_FULL_IMAGE:figures/full_fig_p015_1_6.png]
Figure 1.7
Figure 1.7. Figure 1.7: Example of a circuit with non-delay-guarded feedback that [PITH_FULL_IMAGE:figures/full_fig_p015_1_7.png]
Figure 1.8
Figure 1.8. Figure 1.8: Two representations of digital circuits, the first by La [PITH_FULL_IMAGE:figures/full_fig_p016_1_8.png]
Figure 1.10
Figure 1.10. Figure 1.10: The copying equation, and its implications [PITH_FULL_IMAGE:figures/full_fig_p017_1_10.png]
Figure 1.11
Figure 1.11. Figure 1.11: Categories of digital circuits Chapter 4: Denotational semantics While the previous circuits work discussed assigning semantics to circuits in terms of streams, this model was not constructed in great detail. It was not even deemed important enough to appear in the …
Figure 1.12
Figure 1.12. Figure 1.12: Categories of terms and cospans of hypergraphs [PITH_FULL_IMAGE:figures/full_fig_p020_1_12.png]
Figure 2.1
Figure 2.1. Figure 2.1: Sequential and parallel composition of string diagrams [PITH_FULL_IMAGE:figures/full_fig_p025_2_1.png]
Figure 2.2
Figure 2.2. Figure 2.2: Equations of a category 2.4.1 Commutative diagrams Equations in category theory can be expressed using commutative diagrams. For exam￾ple, the unitality and associativity of composition can be illustrated as follows: 𝐴 𝐵 𝐴 𝐵 𝑓 id𝐴 𝑓 id𝐵 𝑓 𝐴 𝐵 𝐶 𝐷 𝑓 𝑔◦𝑓 ℎ◦𝑔 ℎ We say t…
Figure 2.3
Figure 2.3. Figure 2.3: Diagrammatic depiction of ‘functorial boxes’, and graphical [PITH_FULL_IMAGE:figures/full_fig_p035_2_3.png]
Figure 2.4
Figure 2.4. Figure 2.4: Naturality of transformations in string diagram notation [PITH_FULL_IMAGE:figures/full_fig_p041_2_4.png]
Figure 2.5
Figure 2.5. Figure 2.5: Commutative diagrams for monoidal categories [PITH_FULL_IMAGE:figures/full_fig_p043_2_5.png]
Figure 2.6
Figure 2.6. Figure 2.6: Equations of a strict monoidal category equations, as they do for regular composition in a category. With this in mind, it can be instructive to view a strict monoidal category in terms of equations: these are illustrated in [PITH_FULL_IMAGE:figures/full_fig_p044_2_6.png]
Figure 2.7
Figure 2.7. Figure 2.7: Commutative diagrams for symmetric monoidal categories [PITH_FULL_IMAGE:figures/full_fig_p045_2_7.png]
Figure 2.8
Figure 2.8. Figure 2.8: Equations of a strict symmetric monoidal category [PITH_FULL_IMAGE:figures/full_fig_p046_2_8.png]
Figure 2.9
Figure 2.9. Figure 2.9: Equations of STMCs in string diagram notation [PITH_FULL_IMAGE:figures/full_fig_p048_2_9.png]
Figure 2.10
Figure 2.10. Figure 2.10: Commutative diagrams of a compact closed category [PITH_FULL_IMAGE:figures/full_fig_p049_2_10.png]
Figure 4.1
Figure 4.1. Figure 4.1: Mealy machines for Belnap values and delays [PITH_FULL_IMAGE:figures/full_fig_p087_4_1.png]
Figure 4.2
Figure 4.2. Figure 4.2: Mealy machine for the SR NOR latch Mealy machines are a reasonable semantics for sequential circuits, but the image of [−]I does not always lead to minimal Mealy machines, and there are many Mealy machines that may correspond to the same behaviour. The ‘purest’ seman…
Figure 5.1
Figure 5.1. Figure 5.1: The SR NOR latch from Example 3.18 in global trace-delay form tions are sound, we turn to the denotational semantics; a reduction between circuits 𝑚 𝑓 𝑛 ⇝ 𝑚 𝑔 𝑛 is sound with respect to some interpretation I if and only if r 𝑚 𝑓 𝑛 zS I = r 𝑚 𝑔 𝑛 zS I . Remark 5.7. Th…
Figure 5.2
Figure 5.2. Figure 5.2: Applying the (Mealy) rule to the circuit in [PITH_FULL_IMAGE:figures/full_fig_p109_5_2.png]
Figure 5.3
Figure 5.3. Figure 5.3: A useful cyclic combinational circuit [MSB12, [PITH_FULL_IMAGE:figures/full_fig_p110_5_3.png]
Figure 5.4
Figure 5.4. Figure 5.4: Applying the (IF) rule to the circuit in [PITH_FULL_IMAGE:figures/full_fig_p112_5_4.png]
Figure 5.5
Figure 5.5. Figure 5.5: Applying the (IF) rule to the circuit in [PITH_FULL_IMAGE:figures/full_fig_p112_5_5.png]
Figure 5.6
Figure 5.6. Figure 5.6: Applying Str with inputs tf to the circuit from [PITH_FULL_IMAGE:figures/full_fig_p114_5_6.png]
Figure 5.7
Figure 5.7. Figure 5.7: Using the value rules to reduce the streamed SR NOR latch [PITH_FULL_IMAGE:figures/full_fig_p116_5_7.png]
Figure 6.1
Figure 6.1. Figure 6.1: Set of Mealy equations M. can test if the algebraic semantics are sufficient: are any two denotationally equal circuits identified by equations? When defining such an equational theory, there may be several different sound and complete formulations. Ideally, we want …
Figure 6.2
Figure 6.2. Figure 6.2: Set H of equations for encoding circuit states Proof. Let 𝑔 be defined as the map 𝑟 ↦→ t ||𝑓 || 𝑟 𝑥 ||encm|| ||decm|| |S I ; by Proposition 4.96 we know that 𝑔(𝑡) [𝑣] = 𝜋1 (𝑓 (dec(enc(𝑡)),𝑣)) and 𝑔(𝑡) 𝑣 = 𝑔(𝜋0 (𝑓 (dec(enc(𝑡)),𝑣))). As dec ◦ enc is a Mealy homomorphis…
Figure 6.3
Figure 6.3. Figure 6.3: Proof of Lemma 6.17 Lemma 6.17. For 𝑣 ∈ V, 𝑣 = 𝑣 𝑣 using the encoding equations. Proof. The proof is straightforward and is illustrated in [PITH_FULL_IMAGE:figures/full_fig_p129_6_3.png]
Figure 6.4
Figure 6.4. Figure 6.4: Proof of Lemma 6.18 for the join case Lemma 6.19. Let 𝑚 𝑓 𝑛 be a combinational circuit such that r 𝑓 zC I = 𝑔. Then 𝑣 𝑓 = 𝑔(𝑣) by the encoding equations. Proof. For the same reasoning as Lemma 5.29, the (PI), (F), (J) and (E) equations can be used to show that there …
Figure 6.5
Figure 6.5. Figure 6.5: The schema of restriction equations Example 6.22. Consider the following two circuits in SCircΣB : f t f t Both circuits have circuit states {tf}, but their combinational cores do not have the same semantics. They only act the same because they receive certain inputs…
Figure 6
Figure 6. Figure 6: a: First part of the set of [PITH_FULL_IMAGE:figures/full_fig_p135_6.png]
Figure 6
Figure 6. Figure 6: b: Second part of the set of [PITH_FULL_IMAGE:figures/full_fig_p137_6.png]
Figure 6.7
Figure 6.7. Figure 6.7: Set of normal form equations F. Proof. Repeatedly applying (AF) to 𝑓 propagates the components in the circuit as far to the right as possible, so all the fork and eliminate constructs are in the left half of the term. Using (FC), (FA) to rearrange the forks, and (FU)…
Figure 7.1
Figure 7.1. Figure 7.1: Rules for tidying up circuits in Mealy form [PITH_FULL_IMAGE:figures/full_fig_p143_7_1.png]
Figure 7.2
Figure 7.2. Figure 7.2: Rules for infinite waveforms 7.2.1 Shortcut rules It is often the case that we know that some of the inputs to a circuit are fixed. This can be modelled by precomposing the relevant input with an infinite waveform 𝑣 . We can propagate these waveforms across a circuit…
Figure 7.3
Figure 7.3. Figure 7.3: Belnap shortcut rules for waveforms perhaps they specify some sort of global circuit configuration. Consider the circuit 𝑔 𝑓 , in which the control signal to the multi￾plexer determines which of two subcircuits will become the output. We will assume that the control …
Figure 7.4
Figure 7.4. Figure 7.4: Examples of ‘instantaneous’ shortcut rules [PITH_FULL_IMAGE:figures/full_fig_p146_7_4.png]
Figure 7.5
Figure 7.5. Figure 7.5: Rules for uncertain values reduces the circuit to one with combinational behaviour. f|t ⇝ f|t f|t ⇝ t|f f|t ⇝ t|t ⇝ t ⇝ t ⇝ t ⇝ ⇝ [PITH_FULL_IMAGE:figures/full_fig_p148_7_5.png]
Figure 8.1
Figure 8.1. Figure 8.1: Example of an interfaced string graph 𝜙 𝜓 𝜙 [PITH_FULL_IMAGE:figures/full_fig_p155_8_1.png]
Figure 8.2
Figure 8.2. Figure 8.2: Example of an interfaced hypergraph string graphs is that a wire in a string diagram can be represented by arbitrarily many wire vertices connected together; all of these different depictions are identified by a notion of wire homeomorphism , in which adjacent wire v…
Figure 8.3
Figure 8.3. Figure 8.3: Illustration of the hypergraph from Example [PITH_FULL_IMAGE:figures/full_fig_p157_8_3.png]
Figure 8.4
Figure 8.4. Figure 8.4: Illustration of the coloured hypergraph signature from [PITH_FULL_IMAGE:figures/full_fig_p159_8_4.png]
Figure 8.5
Figure 8.5. Figure 8.5: Equations EFrob of a special commutative Frobenius algebra. Using the equations of EFrob, it can be shown that the latter two terms are equal: (MUL) = (FCM1) = (MA) = (FCM2) = Effectively, any terms in Frob with the same input-output connectivity are equal. 8.3.2 Col…
Figure 8.6
Figure 8.6. Figure 8.6: Equations of a hypergraph category Example 8.35. In Frob𝐶, there is a copy of the Frobenius structure for each colour in 𝐶. For example, when C := {•, •}, the following are terms in Frob𝐶. Although there are two different colours of wires, these wires cannot interact…
Figure 8.7
Figure 8.7. Figure 8.7: The cospan of Example 8.63 in the form of Theorem 8.62 This cospan can be assembled into the form detailed in the above proof as shown in [PITH_FULL_IMAGE:figures/full_fig_p176_8_7.png]
Figure 8.8
Figure 8.8. Figure 8.8: The cospan of Example 8.112 in the form of Theorem 8.111 Corollary 8.113. TΣ  PMCsp𝐷 (HypΣ ). This means that PMCsp𝐷𝐶 (Hyp𝐶,Σ ) is a suitable setting for interpreting terms in TΣ: every term has a corresponding cospan of hypergraphs, and every cospan has a correspon…
Figure 8.9
Figure 8.9. Figure 8.9: Equations ECComon of a commutative comonoid Definition 8.125. Let (ΣCComon, ECComon) be the symmetric monoidal theory of cocommutative comonoids, with ΣCComon := { , } and ECComon defined as in [PITH_FULL_IMAGE:figures/full_fig_p192_8_9.png]
Figure 10.1
Figure 10.1. Figure 10.1: Equations that hold in any Cartesian category [PITH_FULL_IMAGE:figures/full_fig_p220_10_1.png]
Figure 10.3
Figure 10.3. Figure 10.3: Interpretations of equations in Cart for generator 𝑒. closed category in which the tensor is the Cartesian product is trivial. However, Csp𝐷 (HypΣ ) is not subject to these equations: it is only a setting for performing graph rewrites. Using hypergraphs to reason ab…
Figure 10.4
Figure 10.4. Figure 10.4: Hypergraph interpretations of the value rules [PITH_FULL_IMAGE:figures/full_fig_p225_10_4.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Layered Monoidal Theories I: Diagrammatic Algebra and Applications

    cs.LO 2026-02 conditional novelty 6.0 of 10

    Layered monoidal theories let different abstraction levels of a system live in one string diagram with formal translations between layers.

Reference graph

Works this paper leans on

42 extracted references · 26 canonical work pages · cited by 1 Pith paper

  1. [1]

    Open Graphs and Computational Reasoning

    In: Electronic Proceedings in Theoretical Computer Science 26 (June 9, 2010), pp. 169–180. issn: 2075-2180. doi: 10.4204/EPTCS.26.16. arXiv: 1007.3794 (cit. on pp. 145, 188). [DK13] Lucas Dixon and Aleks Kissinger. “Open-Graphs and Monoidal Theories”. In: Mathematical Structures in Computer Science 23.2 (Apr. 2013), pp. 308–359. issn: 0960-1295, 1469-8072...

    work page Pith review arXiv 1945

  2. [2]

    A Structural and Nominal Syntax for Diagrams

    In: Electronic Proceedings in Theoretical Computer Science 266 (Feb. 27, 2018), pp. 71–83. issn: 2075-2180. doi: 10.4204/EPTCS.266.4. arXiv: 1702.01695 (cit. on p. 1). [GLZ23] Ella Gale, Leo Lobski, and Fabio Zanasi. “A Categorical Approach to Synthetic Chemistry”. In: Theoretical Aspects of Computing – ICTAC 2023 . Ed. by Erika Ábrahám, Clemens Dubslaff,...

    work page Pith review arXiv 2018

  3. [12]

    Categorical Semantics of Digital Circuits

    176 pp. isbn: 978-1-4832-2516-6. Google Books: MCijBQAAQBAJ (cit. on pp. 6, 72). [GJ16] Dan R. Ghica and Achim Jung. “Categorical Semantics of Digital Circuits”. In: 2016 Formal Methods in Computer-Aided Design (FMCAD) . 2016 Formal Methods in Computer-Aided Design (FMCAD). Oct. 2016, pp. 41–48. doi: 10.1109/FMCAD.2016.7886659 (cit. on pp. 7–8, 114, 210, ...

    arXiv 2016

  4. [15]

    A Structural and Nominal Syntax for Diagrams

    doi: 10.48550/arXiv.2201.10456. arXiv: 2201.10456 [cs, math] . preprint (cit. on pp. 8, 47, 56, 68, 99, 114). [GL18] Dan R. Ghica and Aliaume Lopez. “A Structural and Nominal Syntax for Diagrams”. Version

    arXiv doi:10.48550/arxiv.2201.10456

  5. [21]

    Decorated Cospans

    issn: 1572-9095. doi: 10.1007/s10485-023-09717-0 (cit. on p. 182). [Fon15] Brendan Fong. “Decorated Cospans”. In: Theory and Applications of Categories 30.33 (Aug. 11, 2015), pp. 1096–1120. arXiv: 1502.00872 (cit. on p. 159). [Fox76] Thomas Fox. “Coalgebras and Cartesian Categories”. In: Communications in Algebra 4.7 (Jan. 1, 1976), pp. 665–667. issn: 009...

    work page Pith review arXiv 2015

  6. [26]

    Feedback, Trace and Fixed-Point Semantics

    url: http://essay.utwente.nl/59381/1/scriptie_M_Kooijman.pdf (cit. on p. 218). [KSW02] P. Katis, Nicoletta Sabadini, and Robert F. C. Walters. “Feedback, Trace and Fixed-Point Semantics”. In: RAIRO - Theoretical Informatics and Applications 36.2 (Apr. 2002), pp. 181–194. issn: 0988-3754, 1290-385X. doi: 10.1051/ita:2002009 (cit. on p. 101). [KSW97] P. Kat...

    work page doi:10.1051/ita:2002009 2004

  7. [28]

    String Diagrams for Layered Explanations

    doi: 10.48550/arXiv.2207.03929. arXiv: 2207.03929 [cs, math] (cit. on pp. 140, 228). [Mac63] Saunders MacLane. “Natural Associativity and Commutativity”. In: Rice Institute Pamphlet-Rice University Studies 49.4 (1963) (cit. on pp. 4, 14). [Mac65] Saunders MacLane. “Categorical Algebra”. In: Bulletin of the American Mathematical Society 71.1 (1965), pp. 40...

    work page Pith review arXiv doi:10.48550/arxiv.2207.03929 1963

  8. [31]

    Rewriting for Symmetric Monoidal Categories with Commutative (Co)Monoid Structure

    doi: 10.48550/arXiv.2204.04274. arXiv: 2204.04274 [cs, math] . preprint (cit. on pp. 146, 182). [MS09] John MacDonald and Laura Scull. “Amalgamations of Categories”. In: Canadian Mathematical Bulletin 52.2 (June 2009), pp. 273–284. issn: 0008-4395, 1496-4287. doi: 10.4153/CMB-2009-030-5 (cit. on pp. 172–173). [MS98] Nicholas McKay and Satnam Singh. “Dynam...

    work page Pith review arXiv doi:10.48550/arxiv.2204.04274 2012

Show all 42 references
  1. [34]

    Call-by-Name, Call-by-Value and 𝜆-Calculus

    816 pp. isbn: 978-0-471-24186-7 (cit. on p. 142). [Plo75] G. D. Plotkin. “Call-by-Name, Call-by-Value and 𝜆-Calculus”. In: Theoretical Computer Science 1.2 (Dec. 1, 1975), pp. 125–159. issn: 0304-3975. doi: 10.1016/0304-3975(75)90017-1 (cit. on p. 97). [Plo81] Gordon Plotkin. ...

    1975 doi

  2. [35]

    The Synthesis of Cyclic Combinational Circuits

    doi: 10.48550/arXiv.2211.16484. arXiv: 2211.16484 [cs]. preprint (cit. on p. 14). [RB03] Marc D. Riedel and Jehoshua Bruck. “The Synthesis of Cyclic Combinational Circuits”. In: Proceedings of the 40th Annual Design Automation Conference . DAC ’03. New York, NY, USA: Associati...

    doi arXiv

  3. [36]

    Cyclic Combinational Circuits

    doi: 10.48550/arXiv.2312.15035. arXiv: 2312.15035 [cs]. preprint (cit. on p. 218). [Rie04] Marc D. Riedel. “Cyclic Combinational Circuits”. PhD thesis. United States – California: California Institute of Technology, May 27,

    doi arXiv

  4. [37]

    The Necessity of Feedback in Minimal Monotone Combinational Circuits

    112 pp. isbn: 9780496071005. url: https://www.proquest.com/ docview/305199547/abstract/B04FE380B2224E4DPQ/1 (cit. on p. 101). [Riv77] Rivest. “The Necessity of Feedback in Minimal Monotone Combinational Circuits”. In: IEEE Transactions on Computers C-26.6 (June 1977), pp. 606–...

    2005

  5. [38]

    A Survey of Graphical Languages for Monoidal Categories

    160 (Aug. 8, 2006), pp. 305–319.issn: 1571-0661. doi: 10.1016/j.entcs.2006.05.030 (cit. on pp. 6, 61–62, 70, 76). [Sco70] Dana Scott. Outline of a Mathematical Theory of Computation . PRG-2. Oxford: Oxford University Computing Laboratory, Programming Research Group, 1970 (cit....

    2006

  6. [39]

    A Lattice-Theoretical Fixpoint Theorem and Its Applications

    422 pp. isbn: 978-1-85233-195-5. doi: 10.1007/978-1-4471-0479-7 (cit. on p. 212). [Tar55] Alfred Tarski. “A Lattice-Theoretical Fixpoint Theorem and Its Applications”. In: Pacific Journal of Mathematics 5.2 (June 1, 1955), pp. 285–309. issn: 0030-8730, 0030-8730. doi: 10.2140/...

    1955

  7. [41]

    Interacting Hopf Algebras: The Theory of Linear Systems

    Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, 37:1–37:19. isbn: 978-3-95977-264-8. doi: 10.4230/LIPIcs.CSL.2023.37 (cit. on p. 53). [Zan15] Fabio Zanasi. “Interacting Hopf Algebras: The Th...

    2023 doi

  8. [42]

    Rewriting in Free Hypergraph Categories

    doi: 10.48550/arXiv.1805.03032.arXiv:1805.03032 (cit. on p. 14). [Zan17] Fabio Zanasi. “Rewriting in Free Hypergraph Categories”. In: Electronic Proceedings in Theoretical Computer Science 263 (Dec. 22, 2017), pp. 16–30. issn: 2075-2180. doi: 10.4204/EPTCS.263.2. arXiv: 1712.0...

    2017 doi arXiv

  9. [82]

    Diagrammatic Semantics for Digital Circuits (Technical Report)

    Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2017, 24:1–24:16. isbn: 978-3-95977-045-3. doi: 10.4230/LIPIcs.CSL.2017.24 (cit. on pp. 1, 7–9, 11, 114, 140, 225–226). Bibliography 240 [GJL17b] Dan ...

    2017 arXiv

  10. [85]

    ClaSH: Structural Descriptions of Synchronous Hardware Using Haskell

    Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017, 24:1–24:16. isbn: 978-3-95977-048-4. doi: 10.4230/LIPIcs.CONCUR.2017.24 (cit. on p. 14). [BKK+10] Christiaan Baaij, Matthijs Kooijman, Jan Kupe...

    2017 doi

  11. [172]

    Lambda-Calculus Models of Programming Languages

    Kyoto, Japan: Electronic Proceedings in Theoretical Computer Science, 2014, pp. 262–269. doi: https://dx.doi.org/10.4204/EPTCS.172.18 (cit. on p. 159). Bibliography 246 [Mor69] James Hiram Morris. “Lambda-Calculus Models of Programming Languages.” Thesis. Massachusetts Institu...

    2014 doi

  12. [252]

    Compositional Approach to Design of Digital Circuits

    Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, 6:1–6:20. isbn: 978-3-95977-264-8. doi: 10.4230/LIPIcs.CSL.2023.6 (cit. on p. 14). [Ale14] Arseniy Alekseyev. “Compositional Approach to Desig...

    2023 doi

  13. [260]

    Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, 14:1–14:21

    Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023, 14:1–14:21. isbn: 978-3-95977-277-8. doi: 10.4230/LIPIcs.FSCD.2023.14 (cit. on pp. 8, 146, 189). [GKS24] Dan R. Ghica, George Kaye, and David ...

    2023 doi

  14. [1973]

    The Calculi of Lambda-Nu-Cs Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages

    Bibliography 238 14th Annual Symposium on Switching and Automata Theory (Swat 1973). Oct. 1973, pp. 167–180. doi: 10.1109/SWAT.1973.11 (cit. on p. 190). [Fel87] Matthias Felleisen. “The Calculi of Lambda-Nu-Cs Conversion: A Syntactic Theory of Control and State in Imperative H...

    1973 doi

  15. [1976]

    String Diagrams for Non-Strict Monoidal Categories

    isbn: 978-3-540-07592-9 978-3-642-95279-1. doi: 10.1007/978-3-642-95279-1 (cit. on p. 96). [WGZ23] Paul Wilson, Dan Ghica, and Fabio Zanasi. “String Diagrams for Non-Strict Monoidal Categories”. In: 31st EACSL Annual Conference on Computer Science Logic (CSL

    doi

  16. [1978]

    Analysis of Cyclic Combinational Circuits

    isbn: 978-1-4419-3123-8 978-1-4757-4721-8. doi: 10.1007/978-1-4757-4721-8 (cit. on pp. 4, 27, 29). [Mal94] S. Malik. “Analysis of Cyclic Combinational Circuits”. In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 13.7 (July 1994), pp. 950–956. is...

  17. [1985]

    Operational Equivalences for Untyped and Polymorphic Object Calculi

    doi: 10.48456/tr-77 (cit. on p. 6). [Gor98] Andrew D. Gordon. “Operational Equivalences for Untyped and Polymorphic Object Calculi”. In: Higher Order Operational Techniques in Semantics . Publications of the Newton Institute. Cambridge University Press, Jan. 22, 1998, pp. 9–54...

    doi

  18. [1987]

    A Reduction Semantics for Imperative Higher-Order Languages

    247 pp. isbn: 9798206205855. url: https://www.proquest.com/docview/ 303475687/abstract/255169B355CB43A2PQ/1 (cit. on p. 97). [FF87] Matthias Felleisen and Daniel P. Friedman. “A Reduction Semantics for Imperative Higher-Order Languages”. In: PARLE Parallel Architectures and La...

    1987 doi

  19. [1988]

    url: https://standards.ieee.org/ieee/1076/1609/ (cit. on p. 218). [IEE96] IEEE Computer Society. IEEE Standard Hardware Description Language Based on the Verilog(R) Hardware Description Language . 1364-1996. Oct. 14,

    1996

  20. [1994]

    Graphical Piecewise-Linear Algebra

    isbn: 978-0-521-44178-0. doi: 10.1017/CBO9780511525858 (cit. on p. 173). [BP22] Guillaume Boisseau and Robin Piedeleu. “Graphical Piecewise-Linear Algebra”. In: Foundations of Software Science and Computation Structures: 25th International Conference, FOSSACS 2022, Held as Par...

  21. [1996]

    An Introduction to Partial Evaluation

    url: https://standards.ieee.org/ieee/1364/2051/ (cit. on p. 218). [Jon96] Neil D. Jones. “An Introduction to Partial Evaluation”. In: ACM Computing Surveys 28.3 (Sept. 1, 1996), pp. 480–503. issn: 0360-0300. doi: 10.1145/243439.243447 (cit. on p. 134). [JS91] André Joyal and R...

    1991

  22. [1999]

    Construction of Pushout Complements in the Category of Hypergraphs

    isbn: 978-1-4471-1221-1 978-1-4471-0865-8. doi: 10.1007/978-1-4471-0865-8 (cit. on p. 213). Bibliography 242 [HJKS11] Marvin Heumüller, Salil Joshi, Barbara König, and Jan Stückrath. “Construction of Pushout Complements in the Category of Hypergraphs”. In: Electronic Communica...

    doi

  23. [2000]

    Modular Hardware Design with Timeline Types

    444 pp. isbn: 978-0-471-31931-3. Google Books: UsJu9IDN2H4C (cit. on p. 142). [NAS23] Rachit Nigam, Pedro Henrique Azevedo de Amorim, and Adrian Sampson. “Modular Hardware Design with Timeline Types”. In: Proceedings of the ACM on Programming Languages 7 (PLDI June 6, 2023), 1...

    2023 doi

  24. [2004]

    A Category-Theoretic Approach to the Semantics of Programming Languages

    MEMOCODE ’04. June 2004, pp. 69–70. doi: 10.1109/MEMCOD.2004.1459818 (cit. on p. 218). [Ole82] Frank J. Oles. “A Category-Theoretic Approach to the Semantics of Programming Languages”. University of Syracuse, Aug

    2004 arXiv

  25. [2005]

    Simple Word Problems in Universal Algebras

    608 pp. isbn: 978-0-201-30857-0 (cit. on p. 1). [KB70] Donald E. Knuth and Peter B. Bendix. “Simple Word Problems in Universal Algebras”. In: Computational Problems in Abstract Algebra . Ed. by John Leech. Pergamon, Jan. 1, 1970, pp. 263–297. isbn: 978-0-08-012975-4. doi: 10.1...

    1970 doi

  26. [2009]

    Coherence for Compact Closed Categories

    630 pp. isbn: 978-1-139-48308-7. doi: 10.1017/CBO9780511816239 (cit. on pp. 9, 80). [KL80] G. M. Kelly and M. L. Laplaza. “Coherence for Compact Closed Categories”. In: Journal of Pure and Applied Algebra 19 (Dec. 1, 1980), pp. 193–213. issn: 0022-4049. doi: 10.1016/0022-4049(...

    1980 doi

  27. [2012]

    Abstract Tensor Systems as Monoidal Categories

    doi: 10.48550/arXiv.1203.0202. arXiv: 1203.0202 [quant-ph] (cit. on pp. 11, 145, 188, 196–197). [Kis14] Aleks Kissinger. “Abstract Tensor Systems as Monoidal Categories”. In: Categories and Types in Logic, Language, and Physics: Essays Dedicated to Jim Lambek on the Occasion o...

    doi arXiv

  28. [2014]

    Feedback and Generalized Logic

    url: http://theses.ncl.ac.uk/jspui/handle/10443/2590 (cit. on p. 5). [Bai76] E. S. Bainbridge. “Feedback and Generalized Logic”. In: Information and Control 31.1 (May 1, 1976), pp. 75–96. issn: 0019-9958. doi: 10.1016/S0019-9958(76)90390-9 (cit. on p. 214). [BCR18] John C. Bae...

    1976 doi arXiv

  29. [2015]

    arXiv: 1406.5942 (cit. on p. 159). [KJ09] Zvi Kohavi and Niraj K. Jha. Switching and Finite Automata Theory . Cambridge University Press, Oct. 22,

    arXiv

  30. [2020]

    Interacting Quantum Observables

    doi: 10.4230/LIPIcs.CSL.2020.18 (cit. on p. 14). [CD08] Bob Coecke and Ross Duncan. “Interacting Quantum Observables”. In: Automata, Languages and Programming. Ed. by Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz...

    2020 doi

  31. [2021]

    Cartesian Bicategories I

    New York, NY, USA: Association for Computing Machinery, June 18, 2021, pp. 175–189. isbn: 978-1-4503-8391-2. doi: 10.1145/3453483.3454037 (cit. on p. 5). [CW87] A. Carboni and R. F. C. Walters. “Cartesian Bicategories I”. In: Journal of Pure and Applied Algebra 49.1 (Nov. 1, 1...

    2021

  32. [2022]

    5th International Conference on Applied Category Theory (ACT 2022). Vol

    2022

  33. [2023]

    On Traced Monoidal Closed Categories

    doi: 10.48550/arXiv.2305.18945. arXiv: 2305.18945 [cs, math] . preprint (cit. on p. 14). [Has09] Masahito Hasegawa. “On Traced Monoidal Closed Categories”. In: Mathematical Structures in Computer Science 19.2 (Apr. 2009), pp. 217–244. issn: 1469-8072, 0960-1295. doi: 10.1017/S...

    2009 doi arXiv

  34. [2024]

    Categories in Control

    doi: 10.48550/arXiv.2401.07055. arXiv: 2401.07055 [cs, math] . preprint (cit. on p. 14). [BE15] John C. Baez and Jason Erbele. “Categories in Control”. In: Theory and Applications of Categories 30.24 (May 20, 2015), pp. 836–881. doi: 10.48550/arXiv.1405.6881 (cit. on p. 14). [...

    2015 doi arXiv

Pith tools

Reviewed August 8, 2026 · model on record in the stance chip above.