Graph-Series Semantics and Abel Regularization for Recursive Hybrid Quantum Programs


Abstract

We introduce a graded graph-series semantics for recursive hybrid quantum programs interpreted in the quantum orchestra monad. Finite terminating executions are represented by directed paths whose edges carry normal completely positive subunital maps and whose terminal vertices carry classical results. Path concatenation defines a graded execution category, while continuation grafting models outcome-dependent sequential composition. We construct a semantic evaluation from admissible execution-graph series to quantum orchestras and prove that it is compatible with both channel composition and Kleisli composition.

For finitary recursive programs, the truncation of the execution series at degree \(n\) is shown to coincide with the \(n\)-th Kleene approximant of the associated Scott-continuous recursion functional. Consequently, evaluation of the complete graph series recovers the ordinary least-fixed-point denotation. Weighting a graph of degree \(n\) by \(q^n\), with \(0<q<1\), yields an Abel-regularised semantics whose Scott limit as \(q\to 1^{-}\) is the unregularised recursive denotation. Equivalently, the parametrisation \(q=e^{-t}\) exponentially suppresses long executions and reconstructs the denotation as \(t\to 0^{+}\).

In a supplementary linear feedback sector, repeated recursion is represented by the execution resolvent \((I-qST)^{-1}\). We identify \(I-qST\) with an algebraic cross-ratio of graph subspaces. Under Hilbert–Schmidt assumptions, the associated return operator is trace class and defines the Fredholm feedback determinant \(\operatorname{det}_{F}(I-qST),\) whose zeros detect singular feedback configurations and whose logarithmic expansion records closed loop traversals.

denotational semantics ,hybrid quantum programs ,recursion ,quantum instruments ,graph series ,Abel regularization ,feedback

1 Introduction↩︎

Quantum programming languages must combine two qualitatively different forms of computation. Quantum data evolve through completely positive maps, while classical control selects subsequent operations, stores measurement outcomes, and determines whether a computation terminates or recurses. Early categorical and type-theoretic models established the basic interaction between quantum operations and classical control [1], [2], and scalable language design subsequently made this interaction explicit at the level of circuit generation and higher-order programming [3]. More recent semantic accounts have treated quantum computation through algebraic effects [4], operator algebras [5], categorical completions of quantum channels [6], information effects [7], and domain-theoretic models supporting continuous or variational parameters [8]. The operator-algebraic background for the present work is the standard theory of \(C^*\)- and \(W^*\)-algebras [9].

A central technical issue is the semantic treatment of measurement-dependent recursion. Quantum measurements are represented by instruments, which jointly encode the classical outcome and the corresponding quantum state transformation [10]. Their compositional structure has recently been clarified from complementary perspectives. Fritz constructs a quantum instrument monad [11], while Booth, Leichtle, Rice, and Worrall study the composition of quantum instruments and the interaction between outcome-dependent control and quantum channels [12]. Building on this analysis, Rice, Leichtle, Worrall, and Booth introduce quantum orchestras, a continuation-based semantics for recursive hybrid programs [13]. Quantum orchestras form a pointed directed-complete semantic domain in which recursive programs are interpreted as least fixed points of Scott-continuous maps. They provide the semantic starting point of the present paper. The use of monads to represent computational effects originates in Moggi’s seminal formulation of notions of computation [14]. Parameterised monads refine this framework by allowing the effectful interface to change across a computation [15], while related indexed constructions model environments and state-dependent interfaces [16]. Effect systems can be interpreted through parametric effect monads [17], and graded monads provide a flexible means of recording quantitative or structural information about computation [18]. The graph degree used in this paper is not introduced as an additional effect system. Instead, it is a combinatorial refinement of an already defined quantum-orchestra denotation: it records the length of finite execution histories before those histories are summed in the semantic domain.

The treatment of recursion relies on the classical order-theoretic theory of fixed points. Tarski’s lattice-theoretic theorem provides the general fixed point principle for monotone maps on complete lattices [19], while domain theory identifies Scott continuity and directed completeness as the appropriate structures for denotational approximation [20], [21]. Iteration theories axiomatise the equational properties of recursive and iterative processes [22]. In probabilistic semantics, the Giry monad [23], probabilistic powerdomains [24], and mixed powerdomains combining probability and nondeterminism [25] show how infinite behaviour can be recovered from ordered families of finite approximations. Quantum orchestras extend this order-theoretic pattern to measurement-dependent quantum computations. The present paper asks whether the individual finite histories underlying the Kleene chain can themselves be organised into a compositional formal series.

Our answer is based on execution graphs. A terminating run is represented by a finite directed path whose edges carry normal completely positive subunital maps and whose terminal vertex carries a classical result. Concatenation of paths is compatible with composition of quantum channels, and the path length defines an additive grading. Formal sums of such paths therefore form a complete graded algebra of the type considered in the theory of generalised formal series indexed by graded categories [26]. The idea of refining a nonlinear or recursive object by a formal expansion is also reminiscent of Taylor expansions of lambda terms [27] and of their coherent organisation by monadic and bimonadic structures [28]. The construction developed here is different in purpose and coefficient semantics: its coefficients are quantum execution histories, and evaluation sends them to quantum orchestras. Nevertheless, these works motivate the systematic separation between a formal expansion and the semantic operation that resums it.

The first main result is a compositional graph-series semantics. Finite graph polynomials are evaluated by summing the Dirac orchestras associated with their terminating paths. Path concatenation evaluates to channel composition, while grafting a continuation graph after a terminating path evaluates to Kleisli composition in the quantum orchestra monad. For a finitary recursive program, the degree-\(n\) truncation of its execution series is exactly the \(n\)-th Kleene approximant. Consequently, semantic evaluation of the complete graph series recovers the ordinary least-fixed-point denotation. The graph series is therefore a conservative refinement: it retains individual histories and their degrees, but forgetting this extra information gives the original quantum-orchestra semantics.

The grading also provides a canonical regularisation. For \(0<q<1\), a graph of degree \(n\) is multiplied by \(q^n\). The resulting positive family is monotone in \(q\), and its Scott supremum as \(q\to 1^{-}\) is the unregularised recursive denotation. Equivalently, with \(q=e^{-t}\), the parameter \(t>0\) exponentially suppresses long executions and the limit \(t\to 0^{+}\) removes the cutoff. The relation between exact-depth contributions and cumulative Kleene approximants yields the Abel identity \[\sum_{n=0}^{\infty} q^n D_n = (1-q)\sum_{n=0}^{\infty} q^n A_n,\] where \(D_n\) is the contribution of histories of exact degree \(n\) and \(A_n\) is the \(n\)-th cumulative approximant. This is an order-theoretic form of Abel summation. Its classical analytic foundations belong to the theory of divergent series [29] and to Tauberian theory [30], but the basic reconstruction theorem proved here does not require norm convergence or a Tauberian converse.

A second, supplementary part of the paper concerns linear feedback. Traced monoidal categories provide an abstract language for feedback [31], and their relation with cyclic sharing and recursion was developed by Hasegawa [32]. Guarded traced categories distinguish well-founded feedback from unrestricted cyclicity [33]. Geometry-of-interaction models interpret computation through the circulation of information along feedback paths [34], including higher-order quantum computation [35]. In the linear sector considered here, an open computation is represented by \(T:C\to R\) and the return interface by \(S:R\to C\). Repeated feedback is then governed by the formal or analytic resolvent \[(I_C-qST)^{-1} = \sum_{n=0}^{\infty} q^n (ST)^n.\] This series is the direct linear image of repeated loop traversals. The same operator is an algebraic cross-ratio of two graph decompositions of \(C\oplus R\), in the sense suggested by the general theory of noncommutative cross-ratio mappings and infinite-dimensional splittings [36]. No smooth Grassmannian structure is needed for the algebraic identity used in this paper.

When \(C\) and \(R\) are Hilbert spaces and the return operator \(ST\) is trace class, the feedback operator has the Fredholm determinant \[\Delta_{T,S}(q) = \operatorname{det}_{\mathrm F}(I_C-qST).\] The relevant trace-ideal and determinant theory is classical [37], [38]. The zeros of this determinant detect singular feedback configurations, while \[\log\Delta_{T,S}(q) = -\sum_{m=1}^{\infty} \frac{q^m}{m} \operatorname{Tr}\bigl((ST)^m\bigr)\] organises traces of closed loop traversals. This determinant is a secondary invariant requiring additional Hilbert–Schmidt or trace-class assumptions; it is not part of the general dcpo semantics. In particular, we do not claim that it is a tau function or that it satisfies Pl"ucker or Hirota relations.

Repeat-until-success circuits provide a basic test case for the interaction between recursion, measurement, and feedback. Such circuits implement a desired quantum operation by repeating a probabilistic subroutine until a success outcome is obtained [39]. In this example, the execution series is geometric, its Abel sum is explicit, and the graph-series denotation agrees with the least fixed point. More elaborate examples show that the dcpo limit may remain meaningful even when norm convergence is not the primary notion, whereas Fredholm determinants require separate analytic control.

The contributions of the paper can be summarised as follows.

  1. We define a graded execution category and a complete algebra of formal execution-graph series for finitary hybrid quantum programs.

  2. We construct a semantic evaluation into quantum orchestras and prove that graph concatenation and continuation grafting are compatible with channel composition and Kleisli composition.

  3. We prove that finite degree truncations coincide with Kleene approximants and that the complete graph-series denotation equals the original least-fixed-point denotation.

  4. We introduce the degree regularisation \(q^{|\Gamma|}\) and prove an Abel reconstruction theorem in the Scott order, together with norm estimates under additional geometric convergence assumptions.

  5. In a linear feedback sector, we identify the execution resolvent with the inverse of an algebraic cross-ratio and construct a Fredholm determinant under trace-class hypotheses.

The paper is organised as follows. Section 2 recalls quantum orchestras, instruments, and recursive denotational semantics. Section 3 introduces finite execution graphs and their graded formal series. Section 4 defines compositional semantic evaluation. Section 5 proves the finite-unfolding correspondence and the Abel reconstruction theorem. Section 6 develops the algebraic feedback resolvent and its cross-ratio interpretation. Section 7 studies the trace-class sector and the Fredholm invariant. Section 8 contains explicit examples, and Section 9 discusses the scope, limitations, and possible extensions of the construction.

2 Quantum orchestras and recursive denotational semantics↩︎

This section recalls the semantic framework on which the constructions of the following sections are based. We use the quantum orchestra monad introduced in [13] to model hybrid computations in which a classical program interacts with an evolving quantum state, receives classical outcomes from measurements, and uses these outcomes to determine both the subsequent quantum operations and the termination behaviour. The construction combines the operator-algebraic formalism of quantum instruments with the order-theoretic treatment of recursion by directed-complete partial orders. Throughout the paper, quantum transformations are written in the Heisenberg picture.

2.1 Quantum channels and domain-theoretic structure↩︎

Let \(\mathcal{A}\) and \(\mathcal{B}\) be von Neumann algebras. We write \[W^{*}(\mathcal{B},\mathcal{A})\] for the set of normal completely positive subunital maps \[\Phi:\mathcal{B}\longrightarrow\mathcal{A}.\] Thus, \(\Phi\) is ultraweakly continuous, every matrix amplification of \(\Phi\) is positive, and \[\Phi(1_{\mathcal{B}})\leq 1_{\mathcal{A}}.\] Composition of such maps is again normal, completely positive, and subunital. The resulting category of von Neumann algebras and normal completely positive subunital maps is symmetric monoidal for the spatial tensor product. In the Heisenberg convention used here, a morphism \(\Phi:\mathcal{B}\to\mathcal{A}\) represents a quantum process from the system described by \(\mathcal{A}\) to the system described by \(\mathcal{B}\); observables are pulled backwards along \(\Phi\). We refer to [5], [9] for the operator-algebraic background.

The hom-set \(W^{*}(\mathcal{B},\mathcal{A})\) is equipped with the completely positive order \[\Phi\leq\Psi \quad\Longleftrightarrow\quad \Psi-\Phi\text{ is completely positive}.\] Its least element is the zero map. A fundamental fact used in the quantum orchestra construction is that \(W^{*}(\mathcal{B},\mathcal{A})\) is a pointed directed-complete partial order and that composition is Scott-continuous in each variable [5], [13].

We recall the domain-theoretic terminology. A subset \(D\) of a partially ordered set \(X\) is directed if every finite subset of \(D\) has an upper bound in \(D\). A directed-complete partial order, abbreviated as dcpo, is a partially ordered set in which every directed subset has a supremum. A dcpo is pointed if it has a least element, denoted by \(\bot\). A map \(f:X\to Y\) between dcpos is Scott-continuous if it preserves directed suprema. We denote by \(\mathbf{DCPO}\) the category of dcpos and Scott-continuous maps.

The order-theoretic interpretation of recursion is supplied by the Kleene fixed-point theorem [20], [21]. If \(X\) is a pointed dcpo and \(F:X\to X\) is Scott-continuous, then \(F\) has a least fixed point given by \[\operatorname{fix}(F) = \sup_{n\in\mathbb{N}}F^{n}(\bot).\] The sequence \[\bot\leq F(\bot)\leq F^{2}(\bot)\leq\cdots\] is called the Kleene chain of \(F\). Its elements will later be related to finite execution graphs and to the coefficients of the graph-series semantics.

2.2 Finite quantum instruments↩︎

A quantum measurement produces both a classical outcome and a transformed quantum state. Quantum instruments provide the standard operator-algebraic representation of this joint behaviour [10].

Definition 1. Let \(X\) be a set and let \(\mathcal{A}\) and \(\mathcal{B}\) be von Neumann algebras. A finite quantum instrument from \(\mathcal{A}\) to \(\mathcal{B}\) with classical outcomes in \(X\) is a family \[\Phi=(\Phi_x)_{x\in X}, \qquad \Phi_x\in W^{*}(\mathcal{B},\mathcal{A}),\] such that \[\operatorname{supp}(\Phi) = \{x\in X\mid \Phi_x\neq 0\}\] is finite and the map \[\sum_{x\in X}\Phi_x\] is subunital.

The component \(\Phi_x\) describes the quantum evolution conditioned on the classical outcome \(x\). If \(\rho\) is a normal state on \(\mathcal{A}\), then \[\rho\bigl(\Phi_x(1_{\mathcal{B}})\bigr)\] is the probability of observing \(x\), while \[\sum_{x\in X}\rho\bigl(\Phi_x(b)\bigr)\] is the expectation of an observable \(b\in\mathcal{B}\) when the classical outcome is discarded.

For \(x\in X\) and \(\Phi\in W^{*}(\mathcal{B},\mathcal{A})\), the associated Dirac instrument is denoted by \(\delta(x,\Phi)\) and is defined by \[\delta(x,\Phi)_y = \begin{cases} \Phi, & y=x,\\ 0, & y\neq x. \end{cases}\] Every finite instrument is a finite sum of Dirac instruments. This notation also makes sequential composition transparent. If an instrument first returns \(x\in X\) and the continuation selected by this outcome is an instrument \(f(x)\), then the appropriate composition is the Kleisli composition of the first instrument with the outcome-dependent family \(f\), rather than composition with a single fixed channel. This is the mechanism by which measurement-dependent classical control is represented.

Finite instruments are sufficient for finite classical outcome spaces and bounded computations. They are not, however, closed under general recursion. For example, a program returning the number of iterations performed before termination may have nonzero components at every natural number. Moreover, a pointwise order on outcome-indexed families does not provide a satisfactory continuous unit when the outcome space itself carries a nontrivial dcpo structure. These difficulties motivate the continuation-based completion by quantum orchestras.

2.3 The quantum orchestra monad↩︎

The quantum orchestra construction is parameterised by an input algebra, an output algebra, and a classical result dcpo. The algebra parameters encode the quantum interface, while the dcpo parameter carries the classical return values and their approximation order. The parameterised form is in the spirit of Atkey’s parameterised monads [15]; the underlying interpretation of computational effects follows the monadic approach of [14].

Definition 2. Let \(\mathcal{A}\) and \(\mathcal{B}\) be von Neumann algebras and let \(X\) be a dcpo. A quantum orchestra \[\xi\in\mathsf{Q}(\mathcal{A},\mathcal{B},X)\] is a family of maps \[\xi_{\mathcal{K}}: \mathbf{DCPO}\bigl(X,W^{*}(\mathcal{K},\mathcal{B})\bigr) \longrightarrow W^{*}(\mathcal{K},\mathcal{A}),\] indexed by von Neumann algebras \(\mathcal{K}\), satisfying the following conditions.

  1. For every \(\mathcal{K}\), the map \[k\longmapsto\xi_{\mathcal{K}}(k)\] is Scott-continuous.

  2. For all \(\theta,\rho\in\mathbb{R}_{+}\) with \(\theta+\rho\leq 1\) and all \[k,k'\in\mathbf{DCPO}\bigl(X,W^{*}(\mathcal{K},\mathcal{B})\bigr),\] one has \[\xi_{\mathcal{K}}(\theta k+\rho k') = \theta\xi_{\mathcal{K}}(k)+\rho\xi_{\mathcal{K}}(k').\]

  3. For every \[\chi\in W^{*}(\mathcal{K}',\mathcal{K})\] and every \[k\in\mathbf{DCPO}\bigl(X,W^{*}(\mathcal{K},\mathcal{B})\bigr),\] one has \[\xi_{\mathcal{K}'} \bigl(x\mapsto k(x)\circ\chi\bigr) = \xi_{\mathcal{K}}(k)\circ\chi.\]

When no confusion can arise, we write \(\xi_k\) instead of \(\xi_{\mathcal{K}}(k)\). The continuation \[k:X\longrightarrow W^{*}(\mathcal{K},\mathcal{B})\] assigns to every classical return value a subsequent quantum computation. The orchestra evaluates the whole continuation and returns a channel in \(W^{*}(\mathcal{K},\mathcal{A})\). The compositionality axiom states that a channel attached after the continuation can be moved outside the orchestra. The subconvexity axiom is the noncommutative analogue of the linearity satisfied by integration against a subprobability valuation.

The order on \(\mathsf{Q}(\mathcal{A},\mathcal{B},X)\) is defined pointwise: \[\xi\leq\zeta \quad\Longleftrightarrow\quad \xi_k\leq\zeta_k \quad\text{for every admissible continuation }k.\] Directed suprema are also computed pointwise: \[\left(\sup_{i\in I}\xi_i\right)_k = \sup_{i\in I}(\xi_i)_k.\] Consequently, \(\mathsf{Q}(\mathcal{A},\mathcal{B},X)\) is a pointed dcpo. Its least element is the orchestra \[\bot_k=0\] for every continuation \(k\).

For \(x\in X\) and \(\Phi\in W^{*}(\mathcal{B},\mathcal{A})\), the Dirac quantum orchestra is defined by \[\delta(x,\Phi)_k = \Phi\circ k(x).\] In particular, the unit of the monad is \[\eta_X^{\mathcal{A}}(x) = \delta(x,\operatorname{id}_{\mathcal{A}}),\] or equivalently \[\eta_X^{\mathcal{A}}(x)_k = k(x).\]

Let \[f:X\longrightarrow\mathsf{Q}(\mathcal{B},\mathcal{C},Y)\] be Scott-continuous. Its Kleisli extension is the Scott-continuous map \[f^{\sharp}: \mathsf{Q}(\mathcal{A},\mathcal{B},X) \longrightarrow \mathsf{Q}(\mathcal{A},\mathcal{C},Y)\] defined by \[f^{\sharp}(\xi)_k = \xi_{x\mapsto f(x)_k},\] where \[k\in\mathbf{DCPO}\bigl(Y,W^{*}(\mathcal{K},\mathcal{C})\bigr).\] For a Dirac orchestra this reduces to \[f^{\sharp}\bigl(\delta(x,\Phi)\bigr)_k = \Phi\circ f(x)_k.\] Thus, the first computation produces \(x\) and the channel \(\Phi\), after which the continuation \(f(x)\) selected by the classical outcome is executed. The unit and Kleisli extension satisfy the monad laws, and the construction is a strong parameterised monad on \(\mathbf{DCPO}\) [13].

Every finite quantum instrument \[(\Phi_x)_{x\in X}\] embeds into the orchestra monad through \[\iota(\Phi) = \sum_{x\in\operatorname{supp}(\Phi)}\delta(x,\Phi_x).\] Its action on a continuation is \[\iota(\Phi)_k = \sum_{x\in\operatorname{supp}(\Phi)}\Phi_x\circ k(x).\] Hence, on finite classical outcome spaces, the continuation-based construction recovers the usual composition of quantum instruments.

2.4 Recursive terms and Kleene approximants↩︎

A recursive program is interpreted by a Scott-continuous endomap on an appropriate orchestra dcpo. For simplicity, consider a recursive term whose quantum input and output interfaces are both represented by the same von Neumann algebra \(\mathcal{A}\), and whose classical result type is interpreted by a dcpo \(X\). Its recursion functional has the form \[F:\mathsf{Q}(\mathcal{A},\mathcal{A},X) \longrightarrow \mathsf{Q}(\mathcal{A},\mathcal{A},X).\] The denotation of the recursive term is the least fixed point \[\llbracket \operatorname{fix}F\rrbracket = \operatorname{fix}(F) = \sup_{n\in\mathbb{N}}F^n(\bot).\] We write \[A_n(F)=F^n(\bot)\] for the \(n\)-th Kleene approximant. The sequence \((A_n(F))_{n\in\mathbb{N}}\) is increasing and represents the behaviour obtained by unfolding the recursion at most \(n\) times. This interpretation of finite unfoldings is the point of departure for the graph expansion developed below: execution graphs of degree \(n\) will encode the contributions appearing at the \(n\)-th stage of the Kleene construction.

The restriction to identical input and output quantum interfaces is natural for a loop. More generally, recursive allocation may be handled by choosing a sufficiently large, possibly infinite-dimensional, von Neumann algebra, or by a refined parameterised type system. These issues are independent of the graph-series construction considered in this paper, and we shall work with a fixed quantum interface whenever recursion is involved.

2.5 A repeat-until-success computation↩︎

We conclude with the standard repeat-until-success example, which will also serve as a test case for the graph-series and Abel constructions. Let \(\mathcal{A}=\mathcal{B}(H)\) and let \(U:H\to H\) be unitary. We denote by \[\mathcal{U}:\mathcal{A}\longrightarrow\mathcal{A}, \qquad \mathcal{U}(M)=U^{*}MU,\] the corresponding Heisenberg channel. Suppose that a computation \(C\) returns a Boolean outcome and has denotation \[\llbracket C\rrbracket = \delta(\mathsf{true},p\mathcal{U}) + \delta(\mathsf{false},(1-p)\operatorname{id}_{\mathcal{A}}), \qquad 0<p<1.\] The outcome \(\mathsf{true}\) indicates success and applies \(\mathcal{U}\), while \(\mathsf{false}\) leaves the quantum state unchanged and requests another iteration. The corresponding recursion functional is \[F(\xi) = \delta((),p\mathcal{U})+(1-p)\xi, \qquad \xi\in\mathsf{Q}(\mathcal{A},\mathcal{A},1).\] Its Kleene approximants are \[F^n(\bot) = \delta\bigl((),\bigl(1-(1-p)^n\bigr)\mathcal{U}\bigr), \qquad n\in\mathbb{N}.\] Indeed, the coefficient \(1-(1-p)^n\) is the probability that at least one of the first \(n\) trials succeeds. Since \[\sup_{n\in\mathbb{N}}\bigl(1-(1-p)^n\bigr)=1,\] Scott-continuity gives \[\operatorname{fix}(F) = \sup_{n\in\mathbb{N}}F^n(\bot) = \delta((),\mathcal{U}).\] Thus, although the number of iterations is unbounded, the recursive program denotes the desired unitary channel. The finite approximants retain the complete unfolding information, whereas the least fixed point records only the resummed behaviour. The purpose of the next sections is to organise the finite unfoldings into a graded graph series and to compare its Abel limit with the dcpo supremum above.

3 Execution graphs and graded series↩︎

The least-fixed-point semantics recalled in Section 2 describes a recursive computation as the supremum of its finite unfoldings. In order to retain the combinatorial information that is lost after taking this supremum, we associate finite execution graphs with the individual histories of a hybrid program. Branching behaviour is represented by a family of such graphs rather than by a single branching tree. Every graph then carries an unambiguous quantum transformation, and its length is additive under concatenation. This provides the grading required for the formal-series construction.

We first work with a fixed quantum store represented by a von Neumann algebra \(\mathcal{A}\). This includes the recursive examples considered in this paper. A version with varying quantum interfaces can be obtained by assigning a von Neumann algebra to each control location and requiring the channels attached to consecutive edges to have compatible domains and codomains.

3.1 Finitary hybrid control systems↩︎

Definition 3. A finitary hybrid control system over \(\mathcal{A}\) is a tuple \[\Sigma=(L,L_{\mathrm{term}},X,r,\mathcal{C})\] with the following data.

  1. \(L\) is a set of control locations, and \(L_{\mathrm{term}}\subseteq L\) is the set of terminal locations.

  2. \(X\) is the classical result set, and \[r:L_{\mathrm{term}}\longrightarrow X\] assigns a result to every terminal location.

  3. \(\mathcal{C}\) is a set of commands. Every command \(c\in\mathcal{C}\) has a source location \(s(c)\in L\setminus L_{\mathrm{term}}\), a finite nonempty outcome set \(O_c\), a target map \[\tau_c:O_c\longrightarrow L,\] and a family of channels \[\Phi_{c,o}\in W^{*}(\mathcal{A},\mathcal{A}), \qquad o\in O_c,\] such that \[\sum_{o\in O_c}\Phi_{c,o}\] is subunital.

The family \((\Phi_{c,o})_{o\in O_c}\) is a finite quantum instrument. The classical outcome \(o\) determines the next control location \(\tau_c(o)\). Unitary commands, measurements, classically controlled gates, and failing operations are all covered by this definition. Purely classical control can be represented by channels equal to either \(\operatorname{id}_{\mathcal{A}}\) or the zero map.

A control system describes the elementary transitions available to a program. The program syntax determines which command is selected at each reachable nonterminal execution prefix.

3.2 Finite execution graphs↩︎

Definition 4. A finite execution graph in \(\Sigma\) is a finite directed path \[\Gamma= \bigl( \ell_0\xrightarrow{(c_1,o_1)}\ell_1 \xrightarrow{(c_2,o_2)}\cdots \xrightarrow{(c_n,o_n)}\ell_n \bigr),\] where, for every \(j\in\{1,\ldots,n\}\), \[s(c_j)=\ell_{j-1}, \qquad \tau_{c_j}(o_j)=\ell_j.\] Its source, target, and degree are respectively \[s(\Gamma)=\ell_0, \qquad t(\Gamma)=\ell_n, \qquad |\Gamma|=n.\] For every \(\ell\in L\), the empty graph at \(\ell\) is denoted by \(\mathbf{1}_{\ell}\) and has degree zero.

The quantum weight of an execution graph is the channel obtained by composing the channels encountered along the path in execution order: \[\Phi_{\Gamma} = \Phi_{c_1,o_1}\circ\Phi_{c_2,o_2}\circ\cdots\circ\Phi_{c_n,o_n}.\] For the empty graph, we set \[\Phi_{\mathbf{1}_{\ell}}=\operatorname{id}_{\mathcal{A}}.\] The order of composition follows the Heisenberg convention: the first command pulls back the observable produced by the continuation of the path.

If \(t(\Gamma_1)=s(\Gamma_2)\), their concatenation is denoted by \[\Gamma_1\star\Gamma_2.\] It is obtained by first following \(\Gamma_1\) and then \(\Gamma_2\). One has \[|\Gamma_1\star\Gamma_2| = |\Gamma_1|+|\Gamma_2|\] and \[\Phi_{\Gamma_1\star\Gamma_2} = \Phi_{\Gamma_1}\circ\Phi_{\Gamma_2}.\]

Proposition 1. The control locations form the objects of a category \(\mathsf{Exec}(\Sigma)\) whose morphisms are finite execution graphs and whose composition is concatenation. The degree map \[|\cdot|:\mathsf{Exec}(\Sigma)\longrightarrow\mathbb{N}\] is additive under composition. Moreover, the assignment \[\Gamma\longmapsto\Phi_{\Gamma}\] preserves identities and composition.

Proof. Associativity follows from associativity of path concatenation, and the empty graphs are its identity elements. Additivity of the degree is immediate from the definition. Compatibility of the quantum weights follows from associativity of channel composition. ◻

An execution graph is terminating if its target belongs to \(L_{\mathrm{term}}\). In that case, its classical result is \[\operatorname{res}(\Gamma)=r(t(\Gamma)).\] Nonterminating behaviour is not represented by an infinite graph at this stage. It appears through arbitrarily long finite prefixes and is recovered by the directed-complete semantics.

3.3 Finite unfoldings as prefix-closed graph families↩︎

Definition 5. Let \(\ell_0\in L\) be an initial location. A finite unfolding rooted at \(\ell_0\) is a finite set \(E\subseteq\mathsf{Exec}(\Sigma)\) satisfying the following conditions.

  1. Every \(\Gamma\in E\) has source \(\ell_0\).

  2. The empty graph \(\mathbf{1}_{\ell_0}\) belongs to \(E\).

  3. The set \(E\) is prefix-closed: if \(\Gamma_1\star\Gamma_2\in E\), then \(\Gamma_1\in E\).

  4. For every nonterminal graph \(\Gamma\in E\) that is not maximal in \(E\), there exists a command \(c_{\Gamma}\) with \[s(c_{\Gamma})=t(\Gamma)\] such that the immediate extensions of \(\Gamma\) in \(E\) are precisely \[\Gamma\star \bigl( t(\Gamma) \xrightarrow{(c_{\Gamma},o)} \tau_{c_{\Gamma}}(o) \bigr), \qquad o\in O_{c_{\Gamma}}.\]

Thus, a finite unfolding is equivalently a finite rooted execution tree, but we identify it with the prefix-closed family of its path graphs. We denote by \(\operatorname{Term}(E)\) the set of terminating maximal graphs of \(E\). Maximal graphs ending at nonterminal locations are unresolved prefixes created by the finite truncation and do not contribute to the terminating instrument.

Definition 6. The terminating instrument associated with a finite unfolding \(E\) is \[\mathcal{I}_E = \sum_{\Gamma\in\operatorname{Term}(E)} \delta\bigl(\operatorname{res}(\Gamma),\Phi_{\Gamma}\bigr).\]

Proposition 2. For every finite unfolding \(E\), the family of channels occurring in \(\mathcal{I}_E\) has a subunital sum. Consequently, \(\mathcal{I}_E\) is a finite quantum instrument.

Proof. We argue by induction on the number of expanded nonterminal prefixes. If no nonterminal prefix is expanded, then either the root is terminal, in which case the only contribution is the identity channel, or the root is nonterminal and unresolved, in which case the terminating instrument is zero. Both cases are subunital.

Assume that the root is expanded by a command \(c\). For every \(o\in O_c\), let \(E_o\) denote the unfolding following outcome \(o\), and let \(\Psi_o\) be the sum of the channels attached to its terminating paths. By the induction hypothesis, \[\Psi_o(1_{\mathcal{A}})\leq 1_{\mathcal{A}}.\] Since \(\Phi_{c,o}\) is positive, \[\Phi_{c,o}\bigl(\Psi_o(1_{\mathcal{A}})\bigr) \leq \Phi_{c,o}(1_{\mathcal{A}}).\] Summing over the outcomes gives \[\sum_{o\in O_c} \Phi_{c,o}\bigl(\Psi_o(1_{\mathcal{A}})\bigr) \leq \sum_{o\in O_c}\Phi_{c,o}(1_{\mathcal{A}}) \leq 1_{\mathcal{A}}.\] This is the required subunitality condition. ◻

Suppose that \(E\subseteq E'\) and that \(E'\) is obtained from \(E\) by expanding some unresolved maximal prefixes. Then \[\mathcal{I}_E\leq\mathcal{I}_{E'}\] in the completely positive order. Hence an increasing sequence of finite unfoldings determines a directed family of finite instruments. Its relation to the Kleene approximants of the corresponding recursive term will be established in Sections 4 and 5.

3.4 The graded algebra of execution-graph series↩︎

Let \[\mathbb{C}\langle\!\langle\mathsf{Exec}(\Sigma)\rangle\!\rangle\] denote the vector space of all formal sums \[a = \sum_{\Gamma\in\mathsf{Exec}(\Sigma)}a_{\Gamma}[\Gamma], \qquad a_{\Gamma}\in\mathbb{C}.\] The symbol \([\Gamma]\) records the execution graph and is not identified with its quantum weight. Multiplication is first defined on basis elements by \[[\Gamma_1][\Gamma_2] = \begin{cases} [\Gamma_1\star\Gamma_2], & t(\Gamma_1)=s(\Gamma_2),\\ 0, & t(\Gamma_1)\neq s(\Gamma_2), \end{cases}\] and is then extended by the Cauchy rule \[(ab)_{\Gamma} = \sum_{\Gamma=\Gamma_1\star\Gamma_2} a_{\Gamma_1}b_{\Gamma_2}.\]

Proposition 3. The Cauchy product above is well defined and associative. The space \(\mathbb{C}\langle\!\langle\mathsf{Exec}(\Sigma)\rangle\!\rangle\) is a complete graded algebra, with homogeneous component of degree \(n\) given by \[\mathscr A_n = \prod_{\substack{\Gamma\in\mathsf{Exec}(\Sigma)\\|\Gamma|=n}} \mathbb{C}[\Gamma].\] Its degree-zero component is generated by the empty graphs \([\mathbf{1}_{\ell}]\), with \(\ell\in L\).

Proof. A graph of degree \(n\) has exactly \(n+1\) decompositions into an initial segment and a final segment. Therefore, every coefficient in the Cauchy product is a finite sum. Associativity follows from associativity of concatenation. Additivity of the degree under concatenation gives the graded decomposition. Completeness refers to the product decomposition \[\mathbb{C}\langle\!\langle\mathsf{Exec}(\Sigma)\rangle\!\rangle = \prod_{n\in\mathbb{N}}\mathscr A_n.\] ◻

This construction is a special case of formal series indexed by an \(\mathbb{N}\)-graded small category, as considered in [26]. No differential structure on the series space is required in the present paper. We shall use only the grading, the local finiteness of the Cauchy product, and completeness with respect to increasing degree.

For a formal parameter \(q\), define the degree-weighting operator \[R_q\left( \sum_{\Gamma}a_{\Gamma}[\Gamma] \right) = \sum_{\Gamma}q^{|\Gamma|}a_{\Gamma}[\Gamma].\] Since the degree is additive, \(R_q\) is an algebra endomorphism: \[R_q(ab)=R_q(a)R_q(b).\] With the parametrisation \[q=e^{-t}, \qquad t>0,\] we write \(R_t=R_{e^{-t}}\). Then \[R_{t+s}=R_tR_s, \qquad s,t>0,\] so that \((R_t)_{t>0}\) is the semigroup generated by the graph-degree operator \[N[\Gamma]=|\Gamma|[\Gamma].\] The limit \(t\to 0^{+}\), equivalently \(q\to 1^{-}\), removes the exponential suppression of long execution graphs. Its semantic meaning will be analysed in Section 5.

3.5 The repeat-until-success graph family↩︎

Consider the repeat-until-success computation of Section 2.5. It has one nonterminal location \(\ell\) and one terminal location \(\ell_{\mathrm{done}}\). The unique command has outcomes \(\mathsf{false}\) and \(\mathsf{true}\), with channels \[\Phi_{\mathsf{false}} = (1-p)\operatorname{id}_{\mathcal{A}}, \qquad \Phi_{\mathsf{true}} = p\mathcal{U}.\] For every \(n\in\mathbb{N}\), there is exactly one terminating execution graph with \(n\) failures followed by one success. Denote it by \(\Gamma_n\). Its degree and quantum weight are \[|\Gamma_n|=n+1\] and \[\Phi_{\Gamma_n} = p(1-p)^n\mathcal{U}.\] The associated formal execution series is \[\mathscr G_{\mathrm{RUS}}(q) = \sum_{n\geq 0}q^{n+1}[\Gamma_n].\] After evaluation of the graph weights, its channel-valued generating series is \[\sum_{n\geq 0}q^{n+1}\Phi_{\Gamma_n} = \frac{pq}{1-(1-p)q}\mathcal{U}, \qquad |q|<(1-p)^{-1}.\] In particular, the Abel limit exists and satisfies \[\lim_{q\to 1^{-}} \sum_{n\geq 0}q^{n+1}\Phi_{\Gamma_n} = \mathcal{U},\] in agreement with the least-fixed-point calculation of Section 2.5. The general relation between graph-series evaluation and recursive denotational semantics is the subject of the next two sections.

4 Compositional graph-series semantics↩︎

The graph algebra introduced in Section 3 records finite execution histories independently of their denotational interpretation. We now define an evaluation of execution graphs in the quantum orchestra monad and show that graph concatenation and continuation grafting reproduce ordinary channel composition and Kleisli composition, respectively. The resulting construction gives a compositional semantics for finite unfoldings and, after completion with respect to the graph degree, for locally finite execution series.

Throughout this section, the quantum store is represented by a fixed von Neumann algebra \(\mathcal{A}\). All execution graphs are assumed to belong to a finitary hybrid control system \(\Sigma\) as in Definition 3.

4.1 Evaluation of terminating graph polynomials↩︎

Let \(X\) be the classical result set of \(\Sigma\). A terminating graph polynomial is a finite sum \[a = \sum_{\Gamma\in F}a_{\Gamma}[\Gamma],\] where \(F\) is a finite set of terminating execution graphs and \(a_{\Gamma}\in\mathbb{R}_{+}\). We call \(a\) semantically admissible if \[\sum_{\Gamma\in F}a_{\Gamma}\Phi_{\Gamma}\] is subunital.

Definition 7. The semantic evaluation of an admissible terminating graph polynomial is the finite quantum instrument \[\operatorname{ev}_{X}(a) = \sum_{\Gamma\in F} a_{\Gamma}\, \delta\bigl(\operatorname{res}(\Gamma),\Phi_{\Gamma}\bigr).\] Through the canonical embedding of finite instruments into quantum orchestras, we also regard \[\operatorname{ev}_{X}(a)\] as an element of \(\mathsf{Q}(\mathcal{A},\mathcal{A},X)\).

The admissibility condition is exactly the condition required for the sum in Definition 7 to be a quantum instrument. In particular, the characteristic polynomial of the terminating paths of a finite unfolding, \[\mathscr G_{E} = \sum_{\Gamma\in\operatorname{Term}(E)}[\Gamma],\] is admissible by Proposition 2, and \[\operatorname{ev}_{X}(\mathscr G_{E}) = \mathcal{I}_{E}.\]

The evaluation is compatible with nonnegative linear combinations whenever the resulting polynomial remains admissible. More precisely, if \(a\) and \(b\) are admissible and if \(\alpha,\beta\in\mathbb{R}_{+}\) satisfy \(\alpha+\beta\leq 1\), then \[\operatorname{ev}_{X}(\alpha a+\beta b) = \alpha\operatorname{ev}_{X}(a) + \beta\operatorname{ev}_{X}(b).\] This is the graph-level counterpart of the subconvexity axiom for quantum orchestras.

4.2 Open graph polynomials and channel composition↩︎

For control locations \(\ell,m\in L\), let \[\mathscr P_{+}(\ell,m)\] denote the cone of finite graph polynomials with nonnegative coefficients, supported on execution graphs with source \(\ell\) and target \(m\). Their evaluation is defined by \[\operatorname{ev}_{\ell,m} \left( \sum_{\Gamma\in F}a_{\Gamma}[\Gamma] \right) = \sum_{\Gamma\in F}a_{\Gamma}\Phi_{\Gamma},\] whenever the right-hand side is a normal completely positive subunital map. Thus, \[\operatorname{ev}_{\ell,m}(a) \in W^{*}(\mathcal{A},\mathcal{A}).\]

If \(a\in\mathscr P_{+}(\ell,m)\) and \(b\in\mathscr P_{+}(m,n)\), their Cauchy product is supported on paths from \(\ell\) to \(n\). The order of the factors agrees with execution order: the paths represented by \(a\) are executed first, and the paths represented by \(b\) are executed afterwards.

Proposition 4. Let \(a\in\mathscr P_{+}(\ell,m)\) and \(b\in\mathscr P_{+}(m,n)\) be semantically admissible. Then \(ab\) is semantically admissible and \[\operatorname{ev}_{\ell,n}(ab) = \operatorname{ev}_{\ell,m}(a) \circ \operatorname{ev}_{m,n}(b).\]

Proof. Write \[a=\sum_{\Gamma}a_{\Gamma}[\Gamma] \qquad\text{and}\qquad b=\sum_{\Delta}b_{\Delta}[\Delta].\] By definition of the Cauchy product, \[ab = \sum_{\Gamma,\Delta} a_{\Gamma}b_{\Delta}[\Gamma\star\Delta].\] Using \[\Phi_{\Gamma\star\Delta} = \Phi_{\Gamma}\circ\Phi_{\Delta},\] we obtain \[\begin{align} \operatorname{ev}_{\ell,n}(ab) &= \sum_{\Gamma,\Delta} a_{\Gamma}b_{\Delta} \bigl(\Phi_{\Gamma}\circ\Phi_{\Delta}\bigr) \\ &= \left(\sum_{\Gamma}a_{\Gamma}\Phi_{\Gamma}\right) \circ \left(\sum_{\Delta}b_{\Delta}\Phi_{\Delta}\right) \\ &= \operatorname{ev}_{\ell,m}(a) \circ \operatorname{ev}_{m,n}(b). \end{align}\] The composition of two normal completely positive subunital maps is again normal, completely positive, and subunital. Hence \(ab\) is semantically admissible. ◻

Thus, graph-series multiplication is not merely a combinatorial operation: it is a refinement of sequential composition in the denotational model.

4.3 Continuation grafting and Kleisli composition↩︎

Sequential composition of hybrid computations is more general than ordinary channel composition because the second computation may depend on the classical result of the first one. We now express this dependence by grafting continuation graphs onto terminating execution graphs.

Let \(X\) and \(Y\) be classical result sets. For every \(x\in X\), choose an initial control location \(\kappa(x)\) for a continuation computation returning values in \(Y\). Let \(a\) be an admissible terminating graph polynomial with results in \(X\), and let \[b_x = \sum_{\Delta}b_{x,\Delta}[\Delta]\] be an admissible terminating graph polynomial rooted at \(\kappa(x)\) and with results in \(Y\).

For a terminating graph \(\Gamma\) with \[\operatorname{res}(\Gamma)=x,\] and a graph \(\Delta\) occurring in \(b_x\), we denote by \[\Gamma\diamond\Delta\] the execution graph obtained by grafting \(\Delta\) after \(\Gamma\), identifying the result interface \(x\) with the continuation input \(\kappa(x)\). Its degree, quantum weight, and result are defined by \[|\Gamma\diamond\Delta| = |\Gamma|+|\Delta|,\] \[\Phi_{\Gamma\diamond\Delta} = \Phi_{\Gamma}\circ\Phi_{\Delta},\] and \[\operatorname{res}(\Gamma\diamond\Delta) = \operatorname{res}(\Delta).\]

Definition 8. The continuation grafting of \(a\) with the family \(b=(b_x)_{x\in X}\) is the graph polynomial \[a\diamond b = \sum_{\Gamma} \sum_{\Delta} a_{\Gamma}b_{\operatorname{res}(\Gamma),\Delta} [\Gamma\diamond\Delta].\]

Assume that \(X\) is a dcpo and define \[f:X\longrightarrow\mathsf{Q}(\mathcal{A},\mathcal{A},Y)\] by \[f(x)=\operatorname{ev}_{Y}(b_x).\]

Theorem 5. Assume that \(a\) and every \(b_x\) are semantically admissible and that \(f\) is Scott-continuous. Then \(a\diamond b\) is semantically admissible and \[\operatorname{ev}_{Y}(a\diamond b) = f^{\sharp}\bigl(\operatorname{ev}_{X}(a)\bigr).\]

Proof. Let \[a = \sum_{\Gamma}a_{\Gamma}[\Gamma].\] By Definition 7, \[\operatorname{ev}_{X}(a) = \sum_{\Gamma} a_{\Gamma} \delta\bigl(\operatorname{res}(\Gamma),\Phi_{\Gamma}\bigr).\] Kleisli extension is subconvex-linear on finite instruments. Hence \[f^{\sharp}\bigl(\operatorname{ev}_{X}(a)\bigr) = \sum_{\Gamma} a_{\Gamma} f^{\sharp} \left( \delta\bigl(\operatorname{res}(\Gamma),\Phi_{\Gamma}\bigr) \right).\] For a Dirac instrument, the Kleisli composition formula gives \[f^{\sharp} \left( \delta\bigl(\operatorname{res}(\Gamma),\Phi_{\Gamma}\bigr) \right) = \sum_{\Delta} b_{\operatorname{res}(\Gamma),\Delta} \delta \left( \operatorname{res}(\Delta), \Phi_{\Gamma}\circ\Phi_{\Delta} \right).\] Using the defining properties of the grafted graph \(\Gamma\diamond\Delta\), the right-hand side becomes \[\sum_{\Delta} b_{\operatorname{res}(\Gamma),\Delta} \delta \left( \operatorname{res}(\Gamma\diamond\Delta), \Phi_{\Gamma\diamond\Delta} \right).\] Summing over \(\Gamma\) yields exactly \[\operatorname{ev}_{Y}(a\diamond b).\] Since the right-hand side is a quantum orchestra, the graph polynomial \(a\diamond b\) is semantically admissible. ◻

Theorem 5 is the fundamental compositionality result for finite graph semantics. It states that grafting execution histories is a combinatorial refinement of Kleisli composition in the quantum orchestra monad.

4.4 Degree weighting and compositionality↩︎

The graph-degree weighting introduced in Section 3.4 is compatible with both concatenation and continuation grafting. For a graph polynomial \(a\), recall that \[R_q(a) = \sum_{\Gamma}q^{|\Gamma|}a_{\Gamma}[\Gamma].\] For a family \(b=(b_x)_{x\in X}\), write \[R_q(b) = \bigl(R_q(b_x)\bigr)_{x\in X}.\]

Proposition 6. For every formal parameter \(q\), \[R_q(a\diamond b) = R_q(a)\diamond R_q(b).\] Whenever the graph polynomials involved are semantically admissible, one has \[\operatorname{ev}_{Y}\bigl(R_q(a\diamond b)\bigr) = f_q^{\sharp} \left( \operatorname{ev}_{X}\bigl(R_q(a)\bigr) \right),\] where \[f_q(x) = \operatorname{ev}_{Y}\bigl(R_q(b_x)\bigr).\]

Proof. For every pair of composable graphs, \[|\Gamma\diamond\Delta| = |\Gamma|+|\Delta|.\] Therefore, \[q^{|\Gamma\diamond\Delta|} = q^{|\Gamma|}q^{|\Delta|},\] which proves the first identity coefficient by coefficient. The second identity follows from Theorem 5 applied to the weighted graph polynomials. ◻

With \(q=e^{-t}\), the proposition says that exponential damping by execution length is compositional. The regularisation can therefore be applied locally to program components before they are combined.

4.5 Locally finite execution series↩︎

We now pass from finite graph polynomials to infinite execution series. A terminating execution series with results in \(X\) is a formal sum \[\mathscr G = \sum_{\Gamma}a_{\Gamma}[\Gamma], \qquad a_{\Gamma}\in\mathbb{R}_{+},\] supported on terminating execution graphs. It is called locally finite if, for every \(n\in\mathbb{N}\), only finitely many graphs of degree at most \(n\) have a nonzero coefficient. Its degree-\(n\) truncation is \[\mathscr G_{\leq n} = \sum_{|\Gamma|\leq n}a_{\Gamma}[\Gamma].\]

Definition 9. A locally finite terminating execution series \(\mathscr G\) is semantically admissible if every truncation \(\mathscr G_{\leq n}\) is admissible.

For a semantically admissible series, the sequence \[\left( \operatorname{ev}_{X}(\mathscr G_{\leq n}) \right)_{n\in\mathbb{N}}\] is increasing in the quantum orchestra order. We define \[\operatorname{ev}_{X}(\mathscr G) = \sup_{n\in\mathbb{N}} \operatorname{ev}_{X}(\mathscr G_{\leq n}).\] The supremum exists because \(\mathsf{Q}(\mathcal{A},\mathcal{A},X)\) is a pointed dcpo.

For \(q\in(0,1]\), define \[R_q(\mathscr G) = \sum_{\Gamma}q^{|\Gamma|}a_{\Gamma}[\Gamma].\] Since multiplication by \(q^{|\Gamma|}\) decreases every nonnegative coefficient, the truncations of \(R_q(\mathscr G)\) remain admissible whenever the truncations of \(\mathscr G\) are admissible. We therefore obtain the \(q\)-weighted denotation \[\mathcal{Z}_{\mathscr G}(q) = \operatorname{ev}_{X}\bigl(R_q(\mathscr G)\bigr).\] For \(q=e^{-t}\), we also write \[\mathcal{Z}_{\mathscr G}(t) = \operatorname{ev}_{X}\bigl(R_t(\mathscr G)\bigr).\]

Proposition 7. Let \(\mathscr G\) be a semantically admissible execution series. If \[0<q\leq q'\leq 1,\] then \[\mathcal{Z}_{\mathscr G}(q) \leq \mathcal{Z}_{\mathscr G}(q').\] Equivalently, the family \[t\longmapsto\mathcal{Z}_{\mathscr G}(t)\] is decreasing with respect to \(t>0\).

Proof. For every graph \(\Gamma\), \[q^{|\Gamma|} \leq (q')^{|\Gamma|}.\] The difference between the corresponding finite truncations is therefore a finite sum of completely positive maps with nonnegative coefficients. Hence \[\operatorname{ev}_{X} \bigl(R_q(\mathscr G_{\leq n})\bigr) \leq \operatorname{ev}_{X} \bigl(R_{q'}(\mathscr G_{\leq n})\bigr).\] Taking directed suprema over \(n\) proves the result. ◻

4.6 Graph-series semantics of a program↩︎

Let \(P\) be a closed finitary hybrid program with initial control location \(\ell_P\) and classical result set \(X\). Denote by \[\operatorname{Term}(P)\] the set of all finite terminating execution graphs generated by \(P\). The formal execution series of \(P\) is \[\mathscr G_P = \sum_{\Gamma\in\operatorname{Term}(P)}[\Gamma].\] Its degree-\(n\) truncation is \[\mathscr G_{P,\leq n} = \sum_{\substack{\Gamma\in\operatorname{Term}(P)\\|\Gamma|\leq n}} [\Gamma].\] For a finitary program, each truncation is finite. Moreover, it is the characteristic polynomial of the terminating paths in the depth-\(n\) unfolding of \(P\). Consequently, \[\operatorname{ev}_{X}(\mathscr G_{P,\leq n}) = \mathcal{I}_{E_n(P)},\] where \(E_n(P)\) denotes the depth-\(n\) unfolding.

Definition 10. The graph-series denotation of \(P\), whenever \(\mathscr G_P\) is semantically admissible, is \[\llbracket P\rrbracket_{\mathrm{gr}} = \operatorname{ev}_{X}(\mathscr G_P).\] Its Abel-regularised graph denotation is \[\llbracket P\rrbracket_{q} = \operatorname{ev}_{X}\bigl(R_q(\mathscr G_P)\bigr), \qquad 0<q<1.\] Equivalently, for \(q=e^{-t}\), \[\llbracket P\rrbracket_{t} = \operatorname{ev}_{X}\bigl(R_t(\mathscr G_P)\bigr), \qquad t>0.\]

The constructions above separate two issues that are conflated by the final least-fixed-point denotation. The formal series \(\mathscr G_P\) records the finite execution histories and their degrees, while semantic evaluation forgets the individual graphs and sums their quantum effects. The next section proves that, for recursive programs generated by Scott-continuous recursion functionals, the truncations of \(\mathscr G_P\) coincide with the Kleene approximants and that the limit \(q\to 1^{-}\) reconstructs the ordinary denotation.

5 Kleene approximants and Abel reconstruction↩︎

The graph-series semantics of Section 4 separates a recursive computation into its finite terminating execution histories. We now show that this decomposition is compatible with the least-fixed-point semantics of quantum orchestras. The main result identifies the depth truncations of the execution series with the Kleene approximants and proves that exponential degree damping, with \(q=e^{-t}\), reconstructs the recursive denotation in the limit \(t\to 0^{+}\).

The arguments are order-theoretic. No norm convergence is required for the basic reconstruction theorem. Analytic convergence estimates are given at the end of the section under additional Banach-space assumptions.

5.1 The one-step semantic functional↩︎

Let \(P\) be a closed finitary hybrid program represented by a control system \(\Sigma\) as in Definition 3. We assume that the syntax of \(P\) selects a unique command \(c_{\ell}\) at every reachable nonterminal control location \(\ell\). This does not restrict the branching caused by quantum measurements: the command \(c_{\ell}\) may still have several classical outcomes. A program with several syntactic commands available at one location can always be refined by replacing that location with sufficiently many control locations.

Set \[L^{\circ}=L\setminus L_{\mathrm{term}}\] and consider the product dcpo \[\mathcal{D}_{P} = \prod_{\ell\in L^{\circ}} \mathsf{Q}(\mathcal{A},\mathcal{A},X),\] equipped with the pointwise order. Its least element is denoted by \(\bot_{P}\).

For \[\Phi\in W^{*}(\mathcal{A},\mathcal{A})\] and \[\xi\in\mathsf{Q}(\mathcal{A},\mathcal{A},X),\] define the left action of \(\Phi\) on \(\xi\) by \[(\Phi\triangleright\xi)_{k} = \Phi\circ\xi_{k}.\]

Lemma 1. The assignment \[(\Phi,\xi) \longmapsto \Phi\triangleright\xi\] is well defined. For fixed \(\Phi\), the map \[\xi\longmapsto\Phi\triangleright\xi\] is Scott-continuous and preserves the least element and directed suprema.

Proof. Normality, complete positivity, and subunitality are preserved by composition. The continuity, subconvexity, and compositionality axioms of a quantum orchestra are also preserved by left composition with \(\Phi\). If \((\xi_i)_{i\in I}\) is directed, then directed suprema in the hom-sets of \(W^{*}\) are computed pointwise and composition is Scott-continuous. Hence \[\Phi\triangleright\left(\sup_{i\in I}\xi_i\right) = \sup_{i\in I}(\Phi\triangleright\xi_i).\] The statement concerning the least element is immediate. ◻

For \(\boldsymbol{\xi}=(\xi_{\ell})_{\ell\in L^{\circ}}\in\mathcal{D}_P\), define \(F_P(\boldsymbol{\xi})\in\mathcal{D}_P\) by \[F_P(\boldsymbol{\xi})_{\ell} = \sum_{o\in O_{c_{\ell}}} B_{\ell,o}(\boldsymbol{\xi}),\] where \[B_{\ell,o}(\boldsymbol{\xi}) = \begin{cases} \delta\bigl(r(\tau_{c_{\ell}}(o)),\Phi_{c_{\ell},o}\bigr), & \tau_{c_{\ell}}(o)\in L_{\mathrm{term}}, \\[4pt] \Phi_{c_{\ell},o}\triangleright \xi_{\tau_{c_{\ell}}(o)}, & \tau_{c_{\ell}}(o)\in L^{\circ}. \end{cases}\] The sum is well defined because each continuation orchestra is subunital and \[\sum_{o\in O_{c_{\ell}}} \Phi_{c_{\ell},o}(1_{\mathcal{A}}) \leq 1_{\mathcal{A}}.\]

Proposition 8. The map \[F_P:\mathcal{D}_P\longrightarrow\mathcal{D}_P\] is Scott-continuous. Consequently, it has a least fixed point \[\operatorname{fix}(F_P) = \sup_{n\in\mathbb{N}}F_P^{n}(\bot_P).\]

Proof. Every component of \(F_P\) is a finite sum of constant Dirac orchestras and maps obtained by composing a coordinate projection with the Scott-continuous action of Lemma 1. Finite sums preserve directed suprema in the present subconvex domain. Hence every component of \(F_P\) is Scott-continuous, and so is \(F_P\). The fixed-point formula follows from the Kleene fixed-point theorem. ◻

For an initial nonterminal location \(\ell_P\), the ordinary recursive denotation of the program is \[\llbracket P\rrbracket = \operatorname{fix}(F_P)_{\ell_P}.\] If the initial location is terminal, the denotation is simply \(\eta_X^{\mathcal{A}}(r(\ell_P))\) and no fixed-point construction is needed.

5.2 Execution depth and Kleene approximation↩︎

For \(\ell\in L^{\circ}\) and \(n\in\mathbb{N}\), let \[\mathscr G_{P,\ell,\leq n} = \sum_{\substack{\Gamma\in\operatorname{Term}(P)\\ s(\Gamma)=\ell,\;|\Gamma|\leq n}} [\Gamma]\] be the polynomial formed by all terminating execution graphs starting at \(\ell\) and having degree at most \(n\). We set \[A_{\ell,n} = \operatorname{ev}_{X} \bigl(\mathscr G_{P,\ell,\leq n}\bigr).\] Since no terminating path can start at a nonterminal location and have degree zero, one has \[A_{\ell,0}=\bot.\]

Theorem 9 (Finite-unfolding correspondence). For every \(\ell\in L^{\circ}\) and every \(n\in\mathbb{N}\), \[F_P^{n}(\bot_P)_{\ell} = A_{\ell,n}.\] Thus, the \(n\)-th Kleene approximant is exactly the semantic evaluation of the terminating execution graphs of degree at most \(n\).

Proof. We argue by induction on \(n\). For \(n=0\), both sides are the least orchestra. Assume that the statement holds at depth \(n\). A terminating path of degree at most \(n+1\) starting at \(\ell\) begins with an outcome \(o\) of the command \(c_{\ell}\). If \(\tau_{c_{\ell}}(o)\) is terminal, this first transition already defines the Dirac orchestra \[\delta\bigl(r(\tau_{c_{\ell}}(o)),\Phi_{c_{\ell},o}\bigr).\] If \(\tau_{c_{\ell}}(o)\) is nonterminal, the remainder of the path is a terminating path of degree at most \(n\) starting at \(\tau_{c_{\ell}}(o)\). By the induction hypothesis, the sum of the semantic weights of all such remainders is \[F_P^{n}(\bot_P)_{\tau_{c_{\ell}}(o)}.\] Prepending the first transition acts by \[\Phi_{c_{\ell},o}\triangleright F_P^{n}(\bot_P)_{\tau_{c_{\ell}}(o)}.\] Summing over the outcomes gives \[A_{\ell,n+1} = F_P\bigl(F_P^{n}(\bot_P)\bigr)_{\ell} = F_P^{n+1}(\bot_P)_{\ell}.\] This completes the induction. ◻

Corollary 1 (Graph-series adequacy). For every initial nonterminal location \(\ell_P\), \[\llbracket P\rrbracket_{\mathrm{gr}} = \llbracket P\rrbracket.\] More explicitly, \[\operatorname{ev}_{X}(\mathscr G_P) = \sup_{n\in\mathbb{N}} \operatorname{ev}_{X}(\mathscr G_{P,\ell_P,\leq n}) = \operatorname{fix}(F_P)_{\ell_P}.\]

Proof. By Definition 10, the graph-series denotation is the supremum of the denotations of its finite degree truncations. Theorem 9 identifies these truncations with the Kleene approximants. Their supremum is the least fixed point of \(F_P\). ◻

The result shows that the graph-series semantics is a conservative refinement of the quantum orchestra semantics. It retains the degree and the individual execution histories, but forgetting this extra information by semantic evaluation recovers the original denotation.

5.3 Exact-depth contributions↩︎

For \(n\in\mathbb{N}\), define the exact-depth graph polynomial \[\mathscr G_{P,\ell,n} = \sum_{\substack{\Gamma\in\operatorname{Term}(P)\\ s(\Gamma)=\ell,\;|\Gamma|=n}} [\Gamma]\] and its semantic contribution \[D_{\ell,n} = \operatorname{ev}_{X}(\mathscr G_{P,\ell,n}).\] The exact-depth contributions are positive in the quantum orchestra order and satisfy \[A_{\ell,n} = \sum_{j=0}^{n}D_{\ell,j}.\] Equivalently, \[D_{\ell,n} = A_{\ell,n}-A_{\ell,n-1}, \qquad n\geq 1,\] where the difference is taken pointwise in the ambient vector spaces of normal linear maps and is completely positive. We use the graph definition of \(D_{\ell,n}\) as the primary one, so no subtraction operation is required in the dcpo itself.

For \(0<q<1\), define the degree-damped denotation \[Z_{\ell}(q) = \operatorname{ev}_{X} \bigl(R_q(\mathscr G_{P,\ell})\bigr) = \sup_{N\in\mathbb{N}} \sum_{n=0}^{N}q^{n}D_{\ell,n}.\] Every finite partial sum is subunital because it is bounded above by the corresponding unweighted truncation. Hence the directed supremum is a well-defined quantum orchestra.

Proposition 10 (Abel identity). For every \(0<q<1\), \[Z_{\ell}(q) = (1-q) \sum_{n=0}^{\infty}q^{n}A_{\ell,n},\] where the series on the right is defined as the directed supremum of its finite partial sums.

Proof. Using \[A_{\ell,n} = \sum_{j=0}^{n}D_{\ell,j},\] positivity allows us to rearrange the directed sums and obtain \[\begin{align} (1-q) \sum_{n=0}^{\infty}q^{n}A_{\ell,n} &= (1-q) \sum_{n=0}^{\infty}q^{n} \sum_{j=0}^{n}D_{\ell,j} \\ &= \sum_{j=0}^{\infty} \left( (1-q) \sum_{n=j}^{\infty}q^{n} \right) D_{\ell,j} \\ &= \sum_{j=0}^{\infty}q^{j}D_{\ell,j} \\ &= Z_{\ell}(q). \end{align}\] All rearrangements are justified by monotonicity: each side is the supremum of the same directed family of finite positive sums. ◻

Proposition 10 distinguishes two generating series. The increment series \[\sum_{n=0}^{\infty}q^{n}D_{\ell,n}\] has a direct semantic interpretation as the degree-weighted sum of terminating histories. The cumulative series \[\sum_{n=0}^{\infty}q^{n}A_{\ell,n}\] contains the same contribution repeatedly and therefore carries a universal geometric divergence as \(q\to 1^{-}\). The factor \(1-q\) is the canonical Abel normalisation that removes this repeated counting in the sense of classical Abel summation [29].

5.4 Order-theoretic Abel reconstruction↩︎

We now prove that the regularised denotations recover the least-fixed-point semantics without any norm-convergence assumption.

Theorem 11 (Abel reconstruction). Let \(P\) be a closed finitary hybrid program and let \(\ell\in L^{\circ}\). Then the family \[\bigl(Z_{\ell}(q)\bigr)_{0<q<1}\] is increasing in \(q\) and bounded above by \(\operatorname{fix}(F_P)_{\ell}\). Moreover, \[\sup_{0<q<1}Z_{\ell}(q) = \operatorname{fix}(F_P)_{\ell}.\] Equivalently, \[\lim_{q\to 1^{-}}^{\mathrm{Scott}}Z_{\ell}(q) = \operatorname{fix}(F_P)_{\ell}.\]

Proof. If \(0<q\leq q'<1\), then \[q^{n}D_{\ell,n} \leq (q')^{n}D_{\ell,n}\] for every \(n\), and therefore \[Z_{\ell}(q) \leq Z_{\ell}(q').\] Since \(q^{n}\leq 1\), one also has \[Z_{\ell}(q) \leq \sup_{N\in\mathbb{N}} \sum_{n=0}^{N}D_{\ell,n} = \sup_{N\in\mathbb{N}}A_{\ell,N} = \operatorname{fix}(F_P)_{\ell}.\]

Let \[Z_{\ell}^{*} = \sup_{0<q<1}Z_{\ell}(q).\] Fix \(N\in\mathbb{N}\). For every \(0<q<1\), positivity gives \[Z_{\ell}(q) \geq \sum_{n=0}^{N}q^{n}D_{\ell,n} \geq q^{N} \sum_{n=0}^{N}D_{\ell,n} = q^{N}A_{\ell,N}.\] Taking the supremum over \(q\in(0,1)\) yields \[Z_{\ell}^{*} \geq A_{\ell,N},\] because \[\sup_{0<q<1}q^{N}A_{\ell,N} = A_{\ell,N}.\] Since this holds for every \(N\), \[Z_{\ell}^{*} \geq \sup_{N\in\mathbb{N}}A_{\ell,N} = \operatorname{fix}(F_P)_{\ell}.\] Combined with the opposite inequality proved above, this gives the result. ◻

Corollary 2. Let \(\mathcal{K}\) be a von Neumann algebra, let \[k:X\longrightarrow W^{*}(\mathcal{K},\mathcal{A})\] be a Scott-continuous continuation, and let \(b\in\mathcal{K}\) be positive. Then \[\bigl(Z_{\ell}(q)_{k}(b)\bigr)_{0<q<1}\] is an increasing net in \(\mathcal{A}_{+}\) and \[Z_{\ell}(q)_{k}(b) \longrightarrow \bigl(\operatorname{fix}(F_P)_{\ell}\bigr)_{k}(b)\] ultraweakly as \(q\to 1^{-}\).

Proof. The order on quantum orchestras is pointwise, and directed suprema in the hom-sets of \(W^{*}\) are computed pointwise in the ultraweak topology. The claim therefore follows directly from Theorem 11. ◻

5.5 The heat parameter \(q=e^{-t}\)↩︎

Set \[q=e^{-t}, \qquad t>0,\] and write \[Z_{\ell}(t) = Z_{\ell}(e^{-t}).\] The exact-depth expansion becomes \[Z_{\ell}(t) = \sum_{n=0}^{\infty}e^{-tn}D_{\ell,n},\] while the Abel identity takes the form \[Z_{\ell}(t) = (1-e^{-t}) \sum_{n=0}^{\infty}e^{-tn}A_{\ell,n}.\] The factor \(e^{-tn}\) suppresses long execution histories, and the limit \(t\to 0^{+}\) removes this suppression. Theorem 11 can therefore be rewritten as \[\lim_{t\to 0^{+}}^{\mathrm{Scott}}Z_{\ell}(t) = \operatorname{fix}(F_P)_{\ell}.\]

Since \[1-e^{-t} \sim t \qquad \text{as }t\to 0^{+},\] the cumulative generating series is renormalised by a factor asymptotic to \(t\). This renormalisation is not an additional choice: it is forced by the relation between exact-depth contributions and cumulative Kleene approximants.

5.6 Norm estimates under geometric convergence↩︎

The order-theoretic theorem is sufficient for denotational semantics. In some applications, however, the relevant orchestras are represented in a Banach space of linear maps and the Kleene approximants converge in norm. The Abel reconstruction then also holds in norm, with an explicit estimate.

Proposition 12. Suppose that the sequence \((A_{\ell,n})_{n\in\mathbb{N}}\) and its supremum \[A_{\ell}=\operatorname{fix}(F_P)_{\ell}\] belong to a Banach space with norm \(\lVert\cdot\rVert\). Assume that there exist constants \(C>0\) and \(0\leq r<1\) such that \[\lVert A_{\ell}-A_{\ell,n}\rVert \leq Cr^{n}\] for every \(n\in\mathbb{N}\). Then, for \(0<q<1\), \[\lVert A_{\ell}-Z_{\ell}(q)\rVert \leq C\frac{1-q}{1-qr}.\] Consequently, \[Z_{\ell}(q) \longrightarrow A_{\ell}\] in norm as \(q\to 1^{-}\).

Proof. Since \[(1-q)\sum_{n=0}^{\infty}q^{n}=1,\] Proposition 10 gives \[A_{\ell}-Z_{\ell}(q) = (1-q) \sum_{n=0}^{\infty}q^{n} \bigl(A_{\ell}-A_{\ell,n}\bigr).\] Therefore, \[\begin{align} \lVert A_{\ell}-Z_{\ell}(q)\rVert &\leq (1-q) \sum_{n=0}^{\infty}q^{n} \lVert A_{\ell}-A_{\ell,n}\rVert \\ &\leq C(1-q) \sum_{n=0}^{\infty}(qr)^{n} \\ &= C\frac{1-q}{1-qr}. \end{align}\] The right-hand side tends to zero as \(q\to 1^{-}\). ◻

5.7 Repeat-until-success revisited↩︎

For the repeat-until-success computation of Sections 2.5 and 3.5, the exact-depth contributions are \[D_{0}=0\] and \[D_{n} = p(1-p)^{n-1}\mathcal{U}, \qquad n\geq 1.\] The Kleene approximants are \[A_n = \sum_{j=0}^{n}D_j = \bigl(1-(1-p)^n\bigr)\mathcal{U}.\] Consequently, \[\begin{align} Z(q) &= \sum_{n=1}^{\infty}q^{n}p(1-p)^{n-1}\mathcal{U} \\ &= \frac{pq}{1-(1-p)q}\mathcal{U} \\ &= (1-q) \sum_{n=0}^{\infty} q^{n} \bigl(1-(1-p)^n\bigr)\mathcal{U}. \end{align}\] It follows that \[\lim_{q\to 1^{-}}Z(q) = \mathcal{U}.\] With \(q=e^{-t}\), this becomes \[Z(t) = \frac{pe^{-t}}{1-(1-p)e^{-t}}\mathcal{U},\] and \[\lim_{t\to 0^{+}}Z(t) = \mathcal{U}.\] Thus, in this elementary example, the graph expansion, the Abel regularisation, and the least-fixed-point semantics can all be computed explicitly and give the same result.

6 Algebraic feedback and execution resolvents↩︎

The preceding sections reconstruct recursive denotations from finite execution histories by means of degree-weighted graph series. We now isolate the algebraic mechanism underlying a feedback loop. In a linear sector, one pass through an open computation is represented by an operator \[T:C\longrightarrow R,\] while the return of the result to the continuation interface is represented by an operator \[S:R\longrightarrow C.\] One complete traversal of the loop is therefore governed by the endomorphism \[K=ST:C\longrightarrow C.\] The regularised feedback equation involves the operator \[I_C-qST,\] where the factor \(q\) records one additional loop traversal. Its inverse, when it exists, resums all finite returns through the feedback interface. We first construct this inverse formally, then relate it to least fixed points and to an algebraic cross-ratio.

The present section is independent of any differential or Grassmannian structure. Only linear algebra, formal series, and, in the analytic part, standard operator theory are used. The relation with traced feedback and the geometry of interaction is discussed in [31], [32], [34], [35].

6.1 Linear feedback configurations↩︎

Let \(C\) and \(R\) be vector spaces over \(\mathbb{C}\). We interpret \(C\) as a continuation interface and \(R\) as a result interface.

Definition 11. A linear feedback configuration is a quadruple \[(C,R,T,S),\] where \[T:C\longrightarrow R \qquad\text{and}\qquad S:R\longrightarrow C\] are linear maps. Its return operator is \[K=ST\in\operatorname{End}(C).\] For a scalar parameter \(q\), the associated feedback operator is \[D_q(T,S)=I_C-qST.\]

Given an initial continuation value \(u\in C\), the \(q\)-regularised feedback equation is \[c=u+qSTc.\] Whenever \(D_q(T,S)\) is invertible, this equation has the unique solution \[c=D_q(T,S)^{-1}u.\] The corresponding result at the output interface is \[r=TD_q(T,S)^{-1}u.\] This motivates the following notation.

Definition 12. Whenever \(I_C-qST\) is invertible, the feedback response is the linear map \[\operatorname{Fb}_q(T,S) = T(I_C-qST)^{-1}:C\longrightarrow R.\]

The parameter \(q\) is central. In the simplest grading, one complete return through the loop has degree one, and the term of degree \(n\) represents an execution that crosses the feedback interface exactly \(n\) times. When the degree counts elementary execution steps instead, the scalar operator \(qST\) is replaced by a positively graded return series \(K(q)\), as described below.

6.2 Formal execution resolvents↩︎

We first work in the formal power-series algebra \[\operatorname{End}(C)[[q]].\] No topology on \(C\) is needed.

Proposition 13 (Formal Neumann resolvent). Let \(K\in\operatorname{End}(C)\). Then \(I_C-qK\) is invertible in \(\operatorname{End}(C)[[q]]\), with inverse \[\mathcal{R}_K(q) = (I_C-qK)^{-1} = \sum_{n=0}^{\infty}q^nK^n.\] Consequently, \[\operatorname{Fb}_q(T,S) = \sum_{n=0}^{\infty}q^nT(ST)^n = \sum_{n=0}^{\infty}q^n(TS)^nT\] as an element of \(\operatorname{Hom}(C,R)[[q]]\).

Proof. For every \(N\in\mathbb{N}\), \[(I_C-qK) \sum_{n=0}^{N}q^nK^n = I_C-q^{N+1}K^{N+1}.\] Hence the coefficient of every fixed power of \(q\) agrees with the corresponding coefficient of the identity when \(N\) is sufficiently large. This proves \[(I_C-qK) \sum_{n=0}^{\infty}q^nK^n = I_C.\] The same computation on the other side gives the two-sided inverse. Finally, \[T(ST)^n=(TS)^nT\] for every \(n\in\mathbb{N}\), which proves the formula for the feedback response. ◻

The construction extends directly to a return operator that is itself a graded execution series.

Proposition 14 (Graded formal resolvent). Let \[K(q)=\sum_{n=1}^{\infty}q^nK_n \in q\operatorname{End}(C)[[q]].\] Then \(I_C-K(q)\) is invertible, with \[(I_C-K(q))^{-1} = \sum_{m=0}^{\infty}K(q)^m.\] For \(N\geq 1\), the coefficient of \(q^N\) in this inverse is \[\sum_{m=1}^{N} \sum_{\substack{n_1+\cdots+n_m=N\\ n_1,\ldots,n_m\geq 1}} K_{n_1}K_{n_2}\cdots K_{n_m}.\]

Proof. Since \(K(q)\) has strictly positive valuation, the coefficient of \(q^N\) in \(K(q)^m\) vanishes whenever \(m>N\). Thus every coefficient of \[\sum_{m=0}^{\infty}K(q)^m\] is a finite sum. The usual geometric-series computation is therefore valid coefficient by coefficient. Expanding \(K(q)^m\) gives the stated coefficient formula. ◻

Suppose that \(K_n\) is the total semantic weight of all elementary return cycles of degree \(n\). Then the ordered product \[K_{n_1}K_{n_2}\cdots K_{n_m}\] is the weight of a feedback execution obtained by concatenating \(m\) return cycles of respective degrees \(n_1,\ldots,n_m\). Therefore, Proposition 14 states that the inverse of \(I_C-K(q)\) is precisely the formal sum of all finite feedback executions. Local finiteness at each total degree is inherited from the positive valuation of \(K(q)\).

6.3 Analytic resolvents↩︎

Assume now that \(C\) and \(R\) are Banach spaces and that \(T\) and \(S\) are bounded operators. The formal resolvent becomes an analytic operator-valued function inside its disk of convergence.

Proposition 15. Let \(K\in\mathcal{L}(C)\), where \(\mathcal{L}(C)\) denotes the Banach algebra of bounded operators on \(C\). If \[|q|\,\lVert K\rVert<1,\] then \[(I_C-qK)^{-1} = \sum_{n=0}^{\infty}q^nK^n\] with convergence in operator norm. More generally, \(I_C-qK\) is invertible if and only if \[q^{-1}\notin\operatorname{Spec}(K)\] for \(q\neq 0\).

Proof. The first statement is the Neumann-series theorem in the Banach algebra \(\mathcal{L}(C)\). For \(q\neq 0\), one has \[I_C-qK = -q\bigl(K-q^{-1}I_C\bigr),\] so invertibility is equivalent to \(q^{-1}\) belonging to the resolvent set of \(K\). ◻

With the parametrisation \[q=e^{-t}, \qquad t>0,\] the feedback operator and its resolvent become \[D_t(T,S) = I_C-e^{-t}ST\] and \[\mathcal{R}_t(T,S) = (I_C-e^{-t}ST)^{-1}.\] The damping factor \(e^{-tn}\) assigns an exponential penalty to an execution that traverses the feedback loop \(n\) times.

Proposition 16. Assume that \(I_C-ST\) is invertible. Then there exists \(t_0>0\) such that \(I_C-e^{-t}ST\) is invertible for every \(t\in[0,t_0)\), and \[\lim_{t\to 0^{+}} (I_C-e^{-t}ST)^{-1} = (I_C-ST)^{-1}\] in operator norm. If, in addition, the spectral radius satisfies \[r(ST)<1,\] then \[(I_C-ST)^{-1} = \sum_{n=0}^{\infty}(ST)^n\] in operator norm.

Proof. The invertible group of a unital Banach algebra is open, and inversion is continuous. Since \[I_C-e^{-t}ST \longrightarrow I_C-ST\] in operator norm as \(t\to 0^{+}\), the first assertion follows. If \(r(ST)<1\), the spectral-radius formula implies that the Neumann series converges in operator norm. ◻

The distinction between the two assumptions in Proposition 16 is important. Invertibility of \(I_C-ST\) guarantees a regular limit of the analytic resolvent, but the unweighted execution series \[\sum_{n=0}^{\infty}(ST)^n\] converges in operator norm only under the stronger spectral-radius condition.

6.4 Feedback as a least fixed point↩︎

The execution resolvent has a direct domain-theoretic interpretation. Let \(C\) be a pointed dcpo cone whose least element is \(0\). Assume that addition and multiplication by scalars in \([0,1]\) preserve directed suprema in each variable. Let \[K:C\longrightarrow C\] be Scott-continuous, additive, and positively homogeneous, and let \(u\in C\).

For \(0\leq q\leq 1\), define \[F_{q,u}(c) = u+qKc.\]

Proposition 17. The map \(F_{q,u}\) is Scott-continuous, and its Kleene approximants satisfy \[F_{q,u}^{n}(\bot) = \sum_{j=0}^{n-1}q^jK^ju\] for every \(n\geq 1\). Consequently, \[\operatorname{fix}(F_{q,u}) = \sup_{n\geq 1} \sum_{j=0}^{n-1}q^jK^ju.\] If \(C\) is embedded in a vector space in which \(I_C-qK\) is invertible and the right-hand side converges to an element of \(C\), then \[\operatorname{fix}(F_{q,u}) = (I_C-qK)^{-1}u.\]

Proof. Scott-continuity follows from the assumptions on addition, scalar multiplication, and \(K\). The formula for the Kleene approximants is proved by induction. For \(n=1\), \[F_{q,u}(\bot)=u,\] because \(K(0)=0\). If the formula holds for \(n\), then \[\begin{align} F_{q,u}^{n+1}(\bot) &= u+qK \left( \sum_{j=0}^{n-1}q^jK^ju \right) \\ &= \sum_{j=0}^{n}q^jK^ju. \end{align}\] The fixed-point formula follows from the Kleene theorem. Finally, any limit \(c\) of the partial sums satisfies \[c=u+qKc,\] and therefore \[(I_C-qK)c=u.\] Invertibility gives the last formula. ◻

In the setting of Sections 4 and 5, the terms \(K^ju\) are the semantic contributions of executions that return through the feedback interface exactly \(j\) times. Proposition 17 therefore identifies the formal Neumann series with the Kleene chain of the linear feedback functional.

6.5 The cross-ratio of two graph decompositions↩︎

The feedback operator \(I_C-qST\) also has an intrinsic algebraic description. Set \[V=C\oplus R\] and identify \(C\) and \(R\) with the coordinate subspaces \[C_0=C\oplus\{0\}, \qquad R_0=\{0\}\oplus R.\] For a linear map \(T:C\to R\), define \[\Gamma(T) = \{(c,Tc)\mid c\in C\},\] and, for \(S:R\to C\), define \[\Gamma(S) = \{(Sr,r)\mid r\in R\}.\] One always has \[V=\Gamma(T)\oplus R_0 \qquad\text{and}\qquad V=C_0\oplus\Gamma(S).\]

If \(V=A\oplus B\), let \[p_{A,B}:V\longrightarrow A\] denote the projection onto \(A\) parallel to \(B\).

Definition 13. The algebraic cross-ratio associated with the two graph decompositions is the endomorphism of \(C_0\) defined by \[\operatorname{CR}(C_0,R_0;\Gamma(T),\Gamma(S)) = p_{C_0,\Gamma(S)} \circ p_{\Gamma(T),R_0} \big|_{C_0}.\] Through the canonical identification \(C_0\simeq C\), it is regarded as an endomorphism of \(C\).

Proposition 18. For every pair of linear maps \(T:C\to R\) and \(S:R\to C\), \[\operatorname{CR}(C_0,R_0;\Gamma(T),\Gamma(S)) = I_C-ST.\] More generally, \[\operatorname{CR}(C_0,R_0;\Gamma(qT),\Gamma(S)) = I_C-qST.\]

Proof. For \(c\in C\), identified with \((c,0)\in C_0\), one has \[p_{\Gamma(T),R_0}(c,0) = (c,Tc).\] Moreover, \[(c,Tc) = (c-STc,0)+(STc,Tc),\] and the second term belongs to \(\Gamma(S)\). Therefore, \[p_{C_0,\Gamma(S)}(c,Tc) = (c-STc,0).\] This proves the first formula. Replacing \(T\) with \(qT\) gives the second one. ◻

The definition above is purely algebraic. The more general smooth cross-ratio construction studied in [36] is not needed for the present semantic application.

Theorem 19 (Transversality criterion). The following conditions are equivalent:

  1. \(V=\Gamma(qT)\oplus\Gamma(S)\);

  2. \(I_C-qST\) is invertible on \(C\);

  3. \(I_R-qTS\) is invertible on \(R\).

When these conditions hold, \[(I_R-qTS)^{-1} = I_R+qT(I_C-qST)^{-1}S\] and \[(I_C-qST)^{-1} = I_C+qS(I_R-qTS)^{-1}T.\]

Proof. Given \((c,r)\in C\oplus R\), a decomposition \[(c,r) = (x,qTx)+(Sy,y)\] is equivalent to \[c=x+Sy, \qquad r=qTx+y.\] Eliminating \(y\) gives \[(I_C-qST)x = c-Sr.\] Thus every vector has a unique such decomposition if and only if \(I_C-qST\) is invertible. This proves the equivalence of the first two conditions. The equivalence with the third condition and the inverse formulas follow from direct multiplication. For example, \[(I_R-qTS) \left(I_R+qT(I_C-qST)^{-1}S\right) = I_R.\] The reverse product is verified in the same way, and the second identity is symmetric. ◻

Corollary 3. Whenever the graph subspaces \(\Gamma(qT)\) and \(\Gamma(S)\) are complementary, the inverse cross-ratio is the execution resolvent: \[\operatorname{CR}(C_0,R_0;\Gamma(qT),\Gamma(S))^{-1} = (I_C-qST)^{-1}.\] Consequently, \[\operatorname{Fb}_q(T,S) = T\, \operatorname{CR}(C_0,R_0;\Gamma(qT),\Gamma(S))^{-1}.\]

Thus, loss of invertibility of the feedback operator is exactly the failure of transversality between the two graph subspaces. This algebraic observation will be used in Section 7 to define a determinant that detects singular feedback configurations.

6.6 Covariance under changes of interface coordinates↩︎

A feedback invariant should not depend on the choice of coordinates used to represent the continuation and result interfaces. Let \[U:C\longrightarrow C' \qquad\text{and}\qquad V:R\longrightarrow R'\] be linear isomorphisms, and define \[T'=VTU^{-1}, \qquad S'=USV^{-1}.\]

Proposition 20. For every scalar \(q\), \[I_{C'}-qS'T' = U(I_C-qST)U^{-1}.\] Whenever these operators are invertible, \[(I_{C'}-qS'T')^{-1} = U(I_C-qST)^{-1}U^{-1}\] and \[\operatorname{Fb}_q(T',S') = V\operatorname{Fb}_q(T,S)U^{-1}.\]

Proof. The first identity follows from \[S'T' = USV^{-1}VTU^{-1} = USTU^{-1}.\] The remaining identities follow by inversion and multiplication by \(T'\). ◻

Hence the execution resolvent and the feedback response are covariant under interface isomorphisms. In particular, spectral and determinant quantities constructed from \(I_C-qST\) depend only on the represented feedback semantics, not on a choice of bases. The trace-class sector and the corresponding Fredholm determinant are studied next.

7 Fredholm invariants of feedback↩︎

The execution resolvent of Section 6 detects whether a linear feedback equation has a unique solution. In a Hilbert-space sector, a stronger scalar invariant is available. If the return operator is trace class, the Fredholm determinant of the feedback operator records its singularities, is invariant under changes of interface coordinates, and admits an expansion in traces of closed loop iterates. This section develops that construction.

No integrable-systems interpretation is assumed. In particular, the Fredholm determinant introduced below is a feedback invariant and is not claimed to satisfy Plücker or Hirota identities.

7.1 The trace-class feedback sector↩︎

Let \(C\) and \(R\) be separable complex Hilbert spaces. We denote by \(\mathcal{L}(C,R)\) the space of bounded operators from \(C\) to \(R\), by \(\mathfrak{S}_{2}(C,R)\) the Hilbert–Schmidt class, and by \(\mathfrak{S}_{1}(C)\) the trace class on \(C\). We use the standard inclusions and ideal properties \[\mathfrak{S}_{1}(C) \subseteq \mathfrak{S}_{2}(C) \subseteq \mathcal{L}(C)\] and \[\mathfrak{S}_{2}(R,C)\,\mathfrak{S}_{2}(C,R) \subseteq \mathfrak{S}_{1}(C).\] We refer to [37], [38] for the theory of trace ideals and Fredholm determinants.

Assumption 1. The feedback configuration \((C,R,T,S)\) satisfies \[T\in\mathfrak{S}_{2}(C,R) \qquad\text{and}\qquad S\in\mathfrak{S}_{2}(R,C).\]

Under Assumption 1, the return operators \[K_C=ST\in\mathfrak{S}_{1}(C) \qquad\text{and}\qquad K_R=TS\in\mathfrak{S}_{1}(R)\] are trace class.

Definition 14. For \(q\in\mathbb{C}\), the Fredholm feedback determinant of \((T,S)\) is \[\Delta_{T,S}(q) = \operatorname{det}_{\mathrm F}\bigl(I_C-qST\bigr).\] With the heat parametrisation \(q=e^{-t}\), where \(t>0\), we write \[\Delta_{T,S}(t) = \operatorname{det}_{\mathrm F}\bigl(I_C-e^{-t}ST\bigr).\]

Since \(ST\) is trace class, the map \[q\longmapsto\Delta_{T,S}(q)\] is entire and satisfies \[\Delta_{T,S}(0)=1.\] The determinant is therefore defined even at values of \(q\) for which the feedback operator is not invertible. At such values, it vanishes.

Theorem 21. Under Assumption 1, the following statements hold.

  1. For every \(q\in\mathbb{C}\), \[\Delta_{T,S}(q)=0\] if and only if \(I_C-qST\) is not invertible.

  2. If \((\lambda_j)_{j\geq 1}\) is the sequence of nonzero eigenvalues of \(ST\), repeated according to algebraic multiplicity, then \[\Delta_{T,S}(q) = \prod_{j\geq 1}(1-q\lambda_j).\]

  3. One has the Sylvester identity \[\operatorname{det}_{\mathrm F}\bigl(I_C-qST\bigr) = \operatorname{det}_{\mathrm F}\bigl(I_R-qTS\bigr).\]

Proof. The first two assertions are standard properties of the Fredholm determinant of a trace-class perturbation of the identity. For the third assertion, the nonzero eigenvalues of \(ST\) and \(TS\) coincide with the same algebraic multiplicities. Their Fredholm products are therefore equal. ◻

By Theorem 19, the zeros of \(\Delta_{T,S}(q)\) are exactly the values of \(q\) for which the graph subspaces \(\Gamma(qT)\) and \(\Gamma(S)\) fail to be complementary. Thus, the determinant is a scalar detector of singular feedback.

7.2 Trace expansion and closed loop executions↩︎

For sufficiently small \(q\), the logarithm of the feedback determinant has the convergent expansion \[\log\Delta_{T,S}(q) = -\sum_{m=1}^{\infty} \frac{q^m}{m} \operatorname{Tr}\bigl((ST)^m\bigr).\] More precisely, this formula is valid whenever \[|q|\,\lVert ST\rVert<1,\] and it extends by analytic continuation on every simply connected component of the set on which \(\Delta_{T,S}\) does not vanish.

The term \[\operatorname{Tr}\bigl((ST)^m\bigr)\] is the trace of an execution that traverses the feedback interface \(m\) times and is then closed at the continuation interface. The factor \(1/m\) removes the choice of a marked starting point on the resulting cyclic execution. In this sense, \(\log\Delta_{T,S}\) is a generating function for closed connected feedback loops, whereas \(\Delta_{T,S}\) contains arbitrary finite collections of such loops.

Proposition 22. Let \(\Omega\) be an open subset of \(\mathbb{C}\) on which \(I_C-qST\) is invertible. Then \[\frac{d}{dq}\log\Delta_{T,S}(q) = -\operatorname{Tr}\left( (I_C-qST)^{-1}ST \right)\] for every \(q\in\Omega\). Equivalently, for \(q=e^{-t}\), \[\frac{d}{dt}\log\Delta_{T,S}(t) = e^{-t} \operatorname{Tr}\left( (I_C-e^{-t}ST)^{-1}ST \right).\]

Proof. For a differentiable trace-class family \(A(q)\), the Fredholm determinant satisfies \[\frac{d}{dq} \log\operatorname{det}_{\mathrm F}\bigl(I_C+A(q)\bigr) = \operatorname{Tr}\left( \bigl(I_C+A(q)\bigr)^{-1}A'(q) \right)\] whenever \(I_C+A(q)\) is invertible. Apply this identity to \[A(q)=-qST.\] The formula in the variable \(t\) follows from the chain rule. ◻

7.3 Formal determinants of graded return series↩︎

The graph semantics generally produces a positively graded return series rather than a single return operator. Let \[K(q) = \sum_{n=1}^{\infty}q^nK_n, \qquad K_n\in\mathfrak{S}_{1}(C).\] We first regard this as a formal series in \(\mathfrak{S}_{1}(C)[[q]]\).

Definition 15. The formal feedback determinant associated with \(K(q)\) is \[\Delta_{K}^{\mathrm{form}}(q) = \exp\left( -\sum_{m=1}^{\infty} \frac{1}{m} \operatorname{Tr}\bigl(K(q)^m\bigr) \right).\]

The expression is well defined in \(\mathbb{C}[[q]]\). Indeed, \(K(q)\) has strictly positive valuation, so the coefficient of \(q^N\) receives contributions only from terms with \(m\leq N\). Each such coefficient is a finite sum of traces of ordered products \[\operatorname{Tr}\bigl(K_{n_1}\cdots K_{n_m}\bigr), \qquad n_1+\cdots+n_m=N.\] This is the determinant-level analogue of the local finiteness used for the graded execution resolvent in Proposition 14. It is also an instance of the general formal-series mechanism described in [26].

Proposition 23. Assume that there exists \(r>0\) such that \[\sum_{n=1}^{\infty} |q|^n\lVert K_n\rVert_1 < \infty\] for every \(q\in\mathbb{C}\) with \(|q|<r\). Then \(K(q)\) converges in trace norm on the disk \(|q|<r\), and \[\Delta_{K}^{\mathrm{form}}(q) = \operatorname{det}_{\mathrm F}\bigl(I_C-K(q)\bigr)\] as analytic functions on that disk.

Proof. The stated summability condition gives trace-norm convergence of \(K(q)\) and locally uniform convergence on compact subdisks. For \(q\) sufficiently close to zero, one has \[\lVert K(q)\rVert<1,\] and the standard logarithmic expansion of the Fredholm determinant gives \[\operatorname{det}_{\mathrm F}\bigl(I_C-K(q)\bigr) = \exp\left( -\sum_{m=1}^{\infty} \frac{1}{m} \operatorname{Tr}\bigl(K(q)^m\bigr) \right).\] Both sides are analytic on \(|q|<r\), so the identity theorem proves the result throughout the disk. ◻

If \(K_n\) is the total weight of elementary return cycles of degree \(n\), the coefficient of \(q^N\) in \[\log\Delta_{K}^{\mathrm{form}}(q)\] is a finite sum over closed cyclic concatenations of total degree \(N\). Thus, the formal determinant retains the grading of the execution semantics while producing a scalar invariant.

7.4 Covariance and semantic invariance↩︎

Let \[U:C\longrightarrow C' \qquad\text{and}\qquad V:R\longrightarrow R'\] be bounded invertible operators, and define \[T'=VTU^{-1}, \qquad S'=USV^{-1}.\] As shown in Proposition 20, one has \[S'T'=U(ST)U^{-1}.\]

Proposition 24. Under Assumption 1, \[\Delta_{T',S'}(q) = \Delta_{T,S}(q)\] for every \(q\in\mathbb{C}\).

Proof. The trace-class operators \(ST\) and \(S'T'\) are similar. The Fredholm determinant is invariant under bounded similarity transformations, and hence \[\operatorname{det}_{\mathrm F}\bigl(I_{C'}-qS'T'\bigr) = \operatorname{det}_{\mathrm F}\bigl(I_C-qST\bigr).\] ◻

Consequently, the determinant does not depend on bases or on equivalent choices of coordinates at the continuation and result interfaces. More generally, suppose that two closed program presentations induce feedback configurations whose return operators are intertwined by a bounded isomorphism. Their Fredholm feedback determinants coincide. This is the precise invariance statement used here. A stronger assertion for arbitrary program equivalences would require the extraction of the Hilbert-space feedback configuration to be canonical with respect to the chosen notion of denotational equivalence.

7.5 Removal of the damping parameter↩︎

The value \(q=1\) removes the exponential damping of repeated feedback. If \(ST\) is trace class, no renormalisation is needed to define the endpoint value: \[\Delta_{T,S}(1) = \operatorname{det}_{\mathrm F}(I_C-ST).\] It may vanish, in which case the unregularised feedback equation is singular.

Proposition 25. Under Assumption 1, \[\lim_{q\to 1^{-}} \Delta_{T,S}(q) = \operatorname{det}_{\mathrm F}(I_C-ST).\] Equivalently, \[\lim_{t\to 0^{+}} \Delta_{T,S}(t) = \operatorname{det}_{\mathrm F}(I_C-ST).\]

Proof. One has \[qST\longrightarrow ST\] in trace norm as \(q\to 1^{-}\). The Fredholm determinant is continuous with respect to the trace norm, which proves the first limit. The second follows from \(q=e^{-t}\). ◻

For a genuinely graded family \(K(t)\), the same conclusion holds whenever there exists \(K_0\in\mathfrak{S}_{1}(C)\) such that \[K(t)\longrightarrow K_0\] in trace norm as \(t\to 0^{+}\). Then \[\operatorname{det}_{\mathrm F}\bigl(I_C-K(t)\bigr) \longrightarrow \operatorname{det}_{\mathrm F}(I_C-K_0).\] If trace-norm convergence fails, the determinant may diverge or vanish with a nontrivial asymptotic rate. A renormalised endpoint can then be introduced only after an asymptotic expansion has been established.

Definition 16. Assume that \(\Delta(t)\neq 0\) for sufficiently small \(t>0\) and that, for a continuous choice of the logarithm, \[\log\Delta(t) = C_{\mathrm{div}}(t)+c_0+o(1)\] as \(t\to 0^{+}\), where \(C_{\mathrm{div}}(t)\) is a specified divergent counterterm. The renormalised feedback determinant is \[\Delta_{\mathrm{ren}} = \exp(c_0) = \lim_{t\to 0^{+}} \exp\bigl(-C_{\mathrm{div}}(t)\bigr)\Delta(t),\] provided that the limit exists.

Definition 16 is conditional: the existence and uniqueness of the counterterm are not consequences of the dcpo semantics alone. In the present paper, renormalisation will be used only in examples for which the small-\(t\) asymptotics can be computed explicitly.

7.6 A semantic Fredholm invariant↩︎

Suppose that a closed program \(P\) admits a linear feedback presentation \[(C_P,R_P,T_P,S_P)\] satisfying Assumption 1. Define \[\Delta_P(q) = \operatorname{det}_{\mathrm F}\bigl(I_{C_P}-qS_PT_P\bigr).\] Then:

  1. \(\Delta_P(q)\) is entire in \(q\);

  2. its zeros are exactly the parameters for which the regularised feedback closure is singular;

  3. its logarithm generates traces of closed loop executions;

  4. it is invariant under bounded isomorphisms of feedback presentations;

  5. its value at \(q=1\) is the unregularised Fredholm determinant whenever the return operator remains trace class.

The determinant is therefore a derived invariant of the linear feedback semantics. It supplements, but does not replace, the order-theoretic denotation constructed in Sections 4 and 5. The examples in the next section illustrate both the Abel reconstruction and the Fredholm invariant in concrete recursive programs.

8 Examples↩︎

This section illustrates the constructions of the preceding sections in a sequence of examples of increasing analytic complexity. The first two examples come directly from recursive hybrid quantum programs. The remaining examples focus on the linear feedback sector and show how ordinary and regularised Fredholm determinants arise from execution resolvents.

8.1 Repeat-until-success as a scalar feedback loop↩︎

Consider again the repeat-until-success computation of Sections 2.5, 3.5, and 5.7. A failed trial has quantum weight \[(1-p)\operatorname{id}_{\mathcal{A}},\] whereas a successful trial has quantum weight \[p\mathcal{U}.\] A terminating execution with exactly \(n\) failures followed by one success has degree \(n+1\) and weight \[p(1-p)^n\mathcal{U}.\] Consequently, its degree-weighted graph denotation is \[Z_{\mathrm{RUS}}(q) = \sum_{n=0}^{\infty} q^{n+1}p(1-p)^n\mathcal{U}.\] For \[|q|<(1-p)^{-1},\] the series converges in operator norm and gives \[Z_{\mathrm{RUS}}(q) = \frac{pq}{1-(1-p)q}\mathcal{U}.\] The limit at \(q=1\) is therefore \[\lim_{q\to 1^{-}}Z_{\mathrm{RUS}}(q) = \mathcal{U},\] in agreement with the least-fixed-point semantics.

The same calculation can be written as a feedback resolvent. Let the scalar return factor be \[K=1-p.\] The success edge contributes \(pq\mathcal{U}\), and hence \[Z_{\mathrm{RUS}}(q) = pq(1-qK)^{-1}\mathcal{U}.\] The associated feedback determinant is \[\Delta_{\mathrm{RUS}}(q) = 1-(1-p)q.\] Its only zero is \[q=(1-p)^{-1}>1.\] Thus, the feedback operator is nonsingular throughout the physical interval \(0\leq q\leq 1\), and the damping parameter can be removed without renormalisation.

With \(q=e^{-t}\), one obtains \[Z_{\mathrm{RUS}}(t) = \frac{pe^{-t}}{1-(1-p)e^{-t}}\mathcal{U}\] and \[\Delta_{\mathrm{RUS}}(t) = 1-(1-p)e^{-t}.\] Both quantities have regular limits as \(t\to 0^{+}\).

8.2 A measurement-controlled loop with two terminal outcomes↩︎

Let \(\mathcal{A}\) be a von Neumann algebra, and let \[A_0,A_1,R\in W^{*}(\mathcal{A},\mathcal{A})\] satisfy \[A_0(1_{\mathcal{A}}) + A_1(1_{\mathcal{A}}) + R(1_{\mathcal{A}}) \leq 1_{\mathcal{A}}.\] The maps \(A_0\) and \(A_1\) describe two terminating measurement outcomes, while \(R\) describes a retry outcome. The corresponding recursion functional on \(\mathsf{Q}(\mathcal{A},\mathcal{A},\{0,1\})\) is \[F(\xi) = \delta(0,A_0) + \delta(1,A_1) + R\triangleright\xi.\] Its \(n\)-th Kleene approximant is \[F^n(\bot) = \sum_{j=0}^{n-1} \left( \delta\bigl(0,R^j\circ A_0\bigr) + \delta\bigl(1,R^j\circ A_1\bigr) \right).\] Indeed, the term indexed by \(j\) represents \(j\) successive retries followed by one of the two terminal outcomes.

The exact-depth graph contribution is \[D_{j+1} = \delta\bigl(0,R^j\circ A_0\bigr) + \delta\bigl(1,R^j\circ A_1\bigr), \qquad j\geq 0.\] The Abel-regularised graph denotation is therefore \[Z(q) = \sum_{j=0}^{\infty}q^{j+1} \left( \delta\bigl(0,R^j\circ A_0\bigr) + \delta\bigl(1,R^j\circ A_1\bigr) \right).\] This series is well defined in the quantum orchestra dcpo for every \(0<q\leq 1\). The order-theoretic Abel reconstruction theorem gives \[\sup_{0<q<1}Z(q) = \operatorname{fix}(F).\]

Suppose, in addition, that the channels are represented as bounded operators on a Banach space of observables and that \[r(R)<1,\] where \(r(R)\) is the spectral radius of \(R\). Then the series converges in operator norm at \(q=1\), and the two terminal components of the denotation are \[\sum_{j=0}^{\infty}R^j\circ A_0 = (I-R)^{-1}A_0\] and \[\sum_{j=0}^{\infty}R^j\circ A_1 = (I-R)^{-1}A_1.\] For \(0<q<1\), the corresponding regularised expressions are \[q(I-qR)^{-1}\circ A_0\] and \[q(I-qR)^{-1}\circ A_1.\] Thus, the same execution resolvent simultaneously controls all terminal outcomes of the measurement-dependent loop.

8.3 A finite-dimensional feedback determinant↩︎

Let \[C=R=\mathbb{C}^d,\] and let \(T,S\in\mathcal{L}(\mathbb{C}^d)\) be such that \[ST = \operatorname{diag}(\lambda_1,\ldots,\lambda_d).\] The regularised execution resolvent is \[(I_C-qST)^{-1} = \operatorname{diag} \left( \frac{1}{1-q\lambda_1}, \ldots, \frac{1}{1-q\lambda_d} \right),\] whenever \[q\lambda_j\neq 1\] for every \(j\). The feedback determinant is \[\Delta_{T,S}(q) = \prod_{j=1}^{d}(1-q\lambda_j).\] Hence the singular parameters are precisely \[q=\lambda_j^{-1}\] for the nonzero eigenvalues of \(ST\).

For example, in dimension two, \[ST = \begin{pmatrix} \alpha & 0\\ 0 & \beta \end{pmatrix}\] gives \[\Delta_{T,S}(q) = (1-q\alpha)(1-q\beta).\] The logarithmic derivative is \[\frac{d}{dq}\log\Delta_{T,S}(q) = - \frac{\alpha}{1-q\alpha} - \frac{\beta}{1-q\beta},\] which is the trace of the regularised loop resolvent with the sign prescribed by Proposition 22.

This example also makes the cross-ratio interpretation explicit. The graph subspaces \(\Gamma(qT)\) and \(\Gamma(S)\) are complementary exactly when \[(1-q\alpha)(1-q\beta)\neq 0.\] Thus, the determinant vanishes exactly when the two graph decompositions cease to be transverse.

8.4 A trace-class diagonal return operator↩︎

Let \[C=R=\ell^2(\mathbb{N})\] with canonical orthonormal basis \((e_n)_{n\geq 1}\), and fix a parameter \[0<a<1.\] Define Hilbert–Schmidt operators \(T\) and \(S\) by \[Te_n=a^{n/2}e_n\] and \[Se_n=a^{n/2}e_n.\] Then \[STe_n=a^ne_n,\] and \(ST\) is trace class because \[\operatorname{Tr}(ST) = \sum_{n=1}^{\infty}a^n = \frac{a}{1-a}.\] The feedback determinant is the convergent \(q\)-product \[\Delta_a(q) = \operatorname{det}_{\mathrm F}(I_C-qST) = \prod_{n=1}^{\infty}(1-qa^n).\] It is defined for every \(q\in\mathbb{C}\) and is nonzero at \(q=1\) because \[\sum_{n=1}^{\infty}a^n<\infty\] and \(a^n\neq 1\).

For \(|q|<a^{-1}\), its logarithm can be computed from the trace expansion: \[\begin{align} \log\Delta_a(q) &= - \sum_{m=1}^{\infty} \frac{q^m}{m}\operatorname{Tr}\bigl((ST)^m\bigr) \\ &= - \sum_{m=1}^{\infty} \frac{q^m}{m} \sum_{n=1}^{\infty}a^{nm} \\ &= - \sum_{m=1}^{\infty} \frac{q^m}{m} \frac{a^m}{1-a^m}. \end{align}\] The endpoint value is \[\Delta_a(1) = \prod_{n=1}^{\infty}(1-a^n).\] This example shows that an infinite-dimensional feedback determinant may be a genuine convergent \(q\)-series determinant without requiring any subtraction at \(q=1\).

8.5 A heat-regularised determinant with a singular endpoint↩︎

We finally consider a model in which the regularised return operator is trace class for every \(t>0\), but no trace-class operator remains at \(t=0\). Let \[C=\ell^2(\mathbb{N})\] and let \(N\) be the number operator \[Ne_n=ne_n, \qquad n\geq 1.\] For \(t>0\), define \[K(t)=e^{-tN}.\] Then \[K(t)e_n=e^{-tn}e_n\] and \[\operatorname{Tr}(K(t)) = \sum_{n=1}^{\infty}e^{-tn} = \frac{e^{-t}}{1-e^{-t}}.\] Thus, \(K(t)\) is trace class for every \(t>0\), and its Fredholm determinant is \[\Delta_{\mathrm{heat}}(t) = \operatorname{det}_{\mathrm F}(I_C-K(t)) = \prod_{n=1}^{\infty}(1-e^{-tn}).\] Equivalently, with \(q=e^{-t}\), \[\Delta_{\mathrm{heat}}(q) = \prod_{n=1}^{\infty}(1-q^n).\] This is the Euler product associated with the degree spectrum of \(N\).

At \(t=0\), the operator \(K(t)\) converges strongly to the identity, which is not trace class. The determinant has no nonzero unregularised endpoint; in fact, \[\Delta_{\mathrm{heat}}(t) \longrightarrow 0\] as \(t\to 0^{+}\). The classical small-\(t\) asymptotic of the Euler product is [29] \[\Delta_{\mathrm{heat}}(t) = \sqrt{\frac{2\pi}{t}} \exp\left( -\frac{\pi^2}{6t} +\frac{t}{24} \right) \bigl(1+o(1)\bigr).\] Consequently, the renormalised determinant \[\Delta_{\mathrm{heat}}^{\mathrm{ren}} = \lim_{t\to 0^{+}} \sqrt{\frac{t}{2\pi}} \exp\left( \frac{\pi^2}{6t} -\frac{t}{24} \right) \Delta_{\mathrm{heat}}(t)\] exists and satisfies \[\Delta_{\mathrm{heat}}^{\mathrm{ren}}=1.\]

This example clarifies the role of the parametrisation \(q=e^{-t}\). The variable \(t\) acts as a heat cutoff on the degree spectrum. For positive \(t\), the cutoff produces a trace-class return operator and a genuine Fredholm determinant. Removing the cutoff requires a renormalisation because the trace-class condition is lost at \(t=0\). Such a renormalisation is not needed in the trace-class situation of Section 8.4.

8.6 Comparison of the examples↩︎

The examples display three distinct behaviours.

  1. In the repeat-until-success and two-outcome loops, the dcpo semantics is reconstructed directly from positive execution contributions. The parameter \(q=e^{-t}\) regularises the depth of recursion, but the limit at \(q=1\) is already finite.

  2. In the finite-dimensional and trace-class diagonal feedback sectors, the Fredholm determinant extends continuously to \(q=1\). Its zeros detect singular feedback, and no renormalisation is necessary.

  3. In the heat-regularised example, every positive value of \(t\) yields a trace-class determinant, but the endpoint operator is not trace class. A nontrivial small-\(t\) subtraction is therefore required to extract a finite value.

These cases separate the order-theoretic existence of a recursive denotation from the analytic existence of a Fredholm determinant. The former is supplied by directed completeness and Scott continuity. The latter requires additional Schatten-class estimates and may fail at the undamped endpoint even when the regularised family is well defined for every \(t>0\).

9 Discussion and further work↩︎

The constructions developed in this paper separate three levels that are often combined in the treatment of recursive hybrid quantum programs. The first is the order-theoretic denotation of recursion by least fixed points in the quantum orchestra monad. The second is a combinatorial refinement by graded execution graphs. The third is an optional linear-analytic layer in which a feedback presentation gives rise to a resolvent, an algebraic cross-ratio, and, under Schatten-class assumptions, a Fredholm determinant. Keeping these levels distinct clarifies both the scope of the results and the additional hypotheses required at each stage.

9.1 Summary of the semantic construction↩︎

For a finitary hybrid control system, every terminating execution history is represented by a finite path whose weight is the ordered composition of the normal completely positive subunital maps attached to its edges. Path concatenation defines a graded category, and the corresponding formal series form a complete graded algebra. The degree records execution length and is additive under concatenation and continuation grafting.

Semantic evaluation sends a terminating graph to the associated Dirac quantum orchestra and extends to admissible positive graph polynomials. The compatibility of graph concatenation with channel composition and of graph grafting with Kleisli composition shows that the graph construction is compositional. For locally finite execution series, evaluation is defined as the directed supremum of the evaluations of the finite degree truncations.

The finite-unfolding correspondence of Theorem 9 identifies these truncations with the Kleene approximants of the recursive semantic functional. Therefore, the graph-series semantics is a conservative refinement of the original quantum orchestra semantics: \[\llbracket P\rrbracket_{\mathrm{gr}} = \llbracket P\rrbracket.\] The refinement retains information that is absent from the final least fixed point, including the individual terminating histories, their execution lengths, and their decomposition into successive control-flow steps.

The degree weighting \[R_q[\Gamma] = q^{|\Gamma|}[\Gamma], \qquad 0<q<1,\] produces an increasing family of regularised denotations. The Abel reconstruction theorem gives \[\sup_{0<q<1}\llbracket P\rrbracket_{q} = \llbracket P\rrbracket.\] Equivalently, with \(q=e^{-t}\), \[\lim_{t\to 0^{+}}^{\mathrm{Scott}}\llbracket P\rrbracket_{t} = \llbracket P\rrbracket.\] This result requires directed completeness, positivity, and Scott continuity, but no norm convergence.

9.2 Scope of the graph model↩︎

The execution graphs used here are finite paths generated by a finitary control system. This level of generality is sufficient for the recursive measurement-controlled programs considered in the examples, but it does not cover every language feature that may occur in a full hybrid quantum programming language.

First, the construction assumes finite branching at each elementary command. Countably or continuously valued measurements require an extension from finite quantum instruments to suitable measurable or domain-theoretic instruments. In that setting, sums over outgoing edges must be replaced by operator-valued integration, and local finiteness of the graph series must be reformulated.

Second, the presentation uses a fixed von Neumann algebra for the quantum store. Dynamic allocation, deallocation, and changes of quantum type can be handled only after replacing the single algebra by a family of algebras indexed by control locations or types. The execution category then becomes a typed category whose arrows carry channels with varying domains and codomains. The formal-series construction extends naturally to this setting, provided that the grading remains locally finite.

Third, the present results establish denotational adequacy of the graph expansion with respect to the given recursive semantic functional. They do not constitute a full-abstraction theorem. Such a theorem would require an operational equivalence for the programming language and a proof that equality of graph-series denotations coincides with contextual equivalence. Since the graph series retains more information than the quantum orchestra denotation, full abstraction may require an explicit quotient identifying operationally indistinguishable histories.

9.3 Meaning and limitations of the Abel parameter↩︎

The parameter \(q\) is introduced by the execution grading. It assigns the factor \(q^{n}\) to a history of degree \(n\). It should not, without additional modelling assumptions, be interpreted as physical time, a transition probability, or a decoherence parameter. The parametrisation \[q=e^{-t}\] is useful because it turns degree damping into a multiplicative semigroup, but the variable \(t\) is initially only a regulator conjugate to the execution degree.

Two related Abel expressions occur in the construction. If \(D_n\) denotes the semantic contribution of histories of exact degree \(n\), then \[\sum_{n=0}^{\infty}q^nD_n\] is the directly weighted execution series. If \(A_n\) denotes the cumulative Kleene approximant, then \[(1-q)\sum_{n=0}^{\infty}q^nA_n\] represents the same regularised denotation. The factor \(1-q\) is required because every exact-depth contribution occurs in all later cumulative approximants. It is therefore a canonical Abel normalisation rather than an independently chosen counterterm.

By contrast, the renormalised Fredholm determinants considered in Section 7 may require the subtraction of additional divergent terms as \(t\to 0^{+}\). Such counterterms are not determined by the dcpo semantics. Their existence and invariance must be proved in each analytic class under consideration. In particular, a regularised determinant should not be regarded as a semantic invariant unless the choice of regularisation and subtraction is shown to be canonical under the relevant program equivalences.

9.4 Feedback, cross-ratios, and Fredholm determinants↩︎

The feedback construction of Section 6 applies after a linear continuation interface \(C\), a linear result interface \(R\), and maps \[T:C\longrightarrow R, \qquad S:R\longrightarrow C\] have been extracted from the program. The return operator is \(ST\), and the regularised feedback equation is solved by the execution resolvent \[(I_C-qST)^{-1}.\] Its Neumann expansion enumerates repeated traversals of the feedback interface. The identity \[\operatorname{CR}(C_0,R_0;\Gamma(qT),\Gamma(S)) = I_C-qST\] shows that invertibility of the feedback operator is equivalent to transversality of two graph subspaces. This is an algebraic observation and does not require a smooth structure on a Grassmannian.

The Fredholm determinant \[\Delta_{T,S}(q) = \operatorname{det}_{\mathrm F}(I_C-qST)\] requires substantially stronger assumptions. The interfaces must be realised as Hilbert spaces and the return operator must be trace class; a sufficient condition is that both \(T\) and \(S\) are Hilbert–Schmidt. Under these assumptions, the zeros of the determinant detect singular feedback, while the trace expansion of its logarithm records closed cyclic traversals of the loop.

This determinant is a derived invariant of a chosen linear feedback presentation. The paper proves invariance under bounded changes of interface coordinates. It does not prove that every quantum orchestra admits a canonical Hilbert-space feedback presentation, nor that two arbitrary presentations of the same denotation necessarily yield the same determinant. Establishing such a result would require a functorial linearisation procedure compatible with the monadic semantics.

The determinant considered here is not asserted to be a tau function of an integrable hierarchy. No Plücker relations, Hirota equations, loop-group factorisation, or Sato Grassmannian flow is constructed. Such structures may arise in special feedback families carrying an additional integrable-system symmetry, but they are not consequences of the graph-series semantics alone.

9.5 Further directions↩︎

Several extensions of the present framework appear natural.

9.5.0.1 Typed and higher-dimensional execution diagrams.

The path model can be replaced by formal series indexed by a graded small category with varying quantum interfaces. More complicated concurrency or resource-sensitive constructs may require trees, directed acyclic graphs, or higher-dimensional diagrams rather than paths. The essential algebraic condition is that every coefficient of a fixed total degree be determined by only finitely many decompositions.

9.5.0.2 Continuous classical outcomes.

A measurable version of the construction should combine quantum instruments with valuations or kernels on continuous classical domains. The corresponding execution expansion would involve iterated operator-valued integrals. An Abel reconstruction theorem would then require a monotone-convergence principle compatible with both the measurable and dcpo structures.

9.5.0.3 Operational adequacy and full abstraction.

The graph semantics provides a natural bridge between small-step execution and denotational recursion. A next step is to define an operational reduction system whose finite runs are precisely the execution graphs and to prove that the probability and quantum effect of termination agree with graph evaluation. Contextual equivalence could then be compared with equality in the graph-series model and in its quantum orchestra quotient.

9.5.0.4 Canonical feedback extraction.

The linear feedback sector would become intrinsically semantic if one could associate functorially with a recursive orchestra a pair of continuation and result interfaces together with maps \(T\) and \(S\). Such a construction may be related to linearisations of continuation semantics, traced monoidal categories, or geometry-of-interaction models. It should preserve Kleisli composition and send recursive closure to an execution resolvent.

9.5.0.5 Determinants and trace formulas.

For graded trace-class return series, the coefficients of \[\log\operatorname{det}_{\mathrm F}(I-K(q))\] are sums of traces of closed execution cycles. This suggests analogues of zeta functions and trace formulas for recursive programs. A satisfactory theory would need to identify the appropriate equivalence relation on cyclic executions and to determine when the resulting determinant is compositional under program substitution.

9.5.0.6 Geometric refinements.

When the feedback graph subspaces belong to a restricted Grassmannian, the algebraic cross-ratio may admit a smooth or diffeological refinement. This could provide geometric information about families of recursive programs and their singular loci. Such a development requires additional polarization and operator-ideal hypotheses and is therefore separate from the semantic results proved here.

9.6 Conclusion↩︎

The main outcome of this paper is a graded execution semantics for recursive hybrid quantum programs that remains compatible with the quantum orchestra model. Finite execution histories form a formal graph series, semantic evaluation is compositional, and finite degree truncations coincide with Kleene approximants. Exponential damping of the graph degree produces an Abel family whose Scott limit is the ordinary least-fixed-point denotation.

In a supplementary linear sector, recursive feedback is represented by the resolvent of \(I_C-qST\). The same operator is an algebraic cross-ratio of graph subspaces, and its Fredholm determinant provides a scalar invariant whenever the return operator is trace class. These analytic constructions enrich the execution semantics but depend on hypotheses that are not needed for the existence of the recursive denotation itself.

The resulting framework therefore distinguishes clearly between the general order-theoretic semantics of recursion, its combinatorial refinement by execution graphs, and the additional operator-theoretic invariants available in restricted feedback sectors.

9.6.0.1 Data availability statement

No data are available for this work.

9.6.0.2 Conflict of interest statement

The authors declare no conflict of interest.

9.6.0.3 Funding

No funding supported this work.

9.6.0.4 Acknowledgements

J.-P.M. thanks the France 2030 framework programme Centre Henri Lebesgue ANR-11-LABX-0020-01 for creating an attractive mathematical environment.

9.6.0.5 Author’s Note on AI Assistance

Portions of the text were developed with the assistance of a generative language model (OpenAI ChatGPT, based on the GPT-4 architecture). The AI was used to assist with drafting, editing, and standardizing the bibliography format. All mathematical content, structure, and theoretical constructions were provided, verified, and curated by the authors. The authors assume full responsibility for the correctness, originality, and scholarly integrity of the final manuscript.

References↩︎

[1]
P. Selinger and B. Valiron, “A lambda calculus for quantum computation with classical control,” Mathematical Structures in Computer Science, vol. 16, no. 3, pp. 527–552, 2006, doi: 10.1017/S0960129506005238.
[2]
P. Selinger, “Dagger compact closed categories and completely positive maps,” Electronic Notes in Theoretical Computer Science, vol. 170, pp. 139–163, 2007, doi: 10.1016/j.entcs.2006.12.018.
[3]
A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, and B. Valiron, “Quipper: A scalable quantum programming language,” ACM SIGPLAN Notices, vol. 48, no. 6, pp. 333–342, 2013, doi: 10.1145/2499370.2462177.
[4]
S. Staton, “Algebraic effects, linearity, and quantum programming languages,” in Proceedings of the 42nd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, 2015, pp. 395–406, doi: 10.1145/2676726.2676999.
[5]
K. Cho, “Semantics for a quantum programming language by operator algebras,” New Generation Computing, vol. 34, no. 1–2, pp. 25–68, 2016, doi: 10.1007/s00354-016-0204-3.
[6]
M. Huot and S. Staton, “Quantum channels as a categorical completion,” in 34th annual ACM/IEEE symposium on logic in computer science, 2019, pp. 1–13, doi: 10.1109/LICS.2019.8785700.
[7]
C. Heunen and R. Kaarsgaard, “Quantum information effects,” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, pp. 1–27, 2022, doi: 10.1145/3498663.
[8]
X. Jia, A. Kornell, B. Lindenhovius, M. W. Mislove, and V. Zamdzhiev, “Semantics for variational quantum programming,” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, pp. 1–31, 2022, doi: 10.1145/3498687.
[9]
S. Sakai, \(C^*\)-Algebras and \(W^*\)-Algebras. Springer, 1971.
[10]
E. B. Davies and J. T. Lewis, “An operational approach to quantum probability,” Communications in Mathematical Physics, vol. 17, no. 3, pp. 239–260, 1970, doi: 10.1007/BF01647093.
[11]
T. Fritz, “The quantum instrument monad,” arXiv preprint arXiv:2606.27805, 2026, doi: 10.48550/arXiv.2606.27805.
[12]
R. I. Booth, D. Leichtle, A. Rice, and K. Worrall, “Composing quantum instruments,” arXiv preprint arXiv:2606.28291, 2026, doi: 10.48550/arXiv.2606.28291.
[13]
A. Rice, D. Leichtle, K. Worrall, and R. I. Booth, “Quantum orchestras: A concrete semantics for recursive hybrid programs,” arXiv preprint arXiv:2607.09605, 2026, doi: 10.48550/arXiv.2607.09605.
[14]
E. Moggi, “Notions of computation and monads,” Information and Computation, vol. 93, no. 1, pp. 55–92, 1991, doi: 10.1016/0890-5401(91)90052-4.
[15]
R. Atkey, “Parameterised notions of computation,” Journal of Functional Programming, vol. 19, no. 3–4, pp. 335–376, 2009, doi: 10.1017/S095679680900728X.
[16]
P. B. Levy, J. Power, and H. Thielecke, “Modelling environments in call-by-value programming languages,” Information and Computation, vol. 185, no. 2, pp. 182–210, 2003, doi: 10.1016/S0890-5401(03)00088-9.
[17]
S. Katsumata, “Parametric effect monads and semantics of effect systems,” in Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, 2014, pp. 633–645, doi: 10.1145/2535838.2535846.
[18]
S. Katsumata, D. McDermott, T. Uustalu, and N. Wu, “Flexible presentations of graded monads,” Proceedings of the ACM on Programming Languages, vol. 6, no. ICFP, pp. 902–930, 2022, doi: 10.1145/3547654.
[19]
A. Tarski, “A lattice-theoretical fixpoint theorem and its applications,” Pacific Journal of Mathematics, vol. 5, no. 2, pp. 285–309, 1955, doi: 10.2140/pjm.1955.5.285.
[20]
S. Abramsky and A. Jung, “Domain theory,” in Handbook of logic in computer science, volume 3: Semantic structures, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, Eds. Oxford: Clarendon Press, 1994, pp. 1–168.
[21]
V. Stoltenberg-Hansen, I. Lindström, and E. R. Griffor, Mathematical theory of domains, vol. 22. Cambridge University Press, 1994.
[22]
S. L. Bloom and Z. Ésik, Iteration theories: The equational logic of iterative processes. Berlin: Springer, 1993.
[23]
M. Giry, A categorical approach to probability theory,” in Categorical aspects of topology and analysis, vol. 915, B. Banaschewski, Ed. Springer, 1982, pp. 68–85.
[24]
C. Jones and G. D. Plotkin, “A probabilistic powerdomain of evaluations,” in Proceedings of the fourth annual symposium on logic in computer science, 1989, pp. 186–195.
[25]
K. Keimel and G. D. Plotkin, “Mixed powerdomains for probability and nondeterminism,” Logical Methods in Computer Science, vol. 13, no. 1, pp. 1–84, 2017, doi: 10.23638/LMCS-13(1:2)2017.
[26]
J.-P. Magnot, “Diffeological generalized formal series: An overview,” arXiv preprint arXiv:2508.15786, 2025, doi: 10.48550/arXiv.2508.15786.
[27]
T. Ehrhard and L. Regnier, “Uniformity and the taylor expansion of ordinary lambda-terms,” Theoretical Computer Science, vol. 403, no. 2–3, pp. 347–372, 2008, doi: 10.1016/j.tcs.2008.06.001.
[28]
T. Ehrhard and A. Walch, “Coherent taylor expansion as a bimonad,” Mathematical Structures in Computer Science, vol. 35, 2025, doi: 10.1017/S0960129525000040.
[29]
G. H. Hardy, Divergent series. Oxford: Clarendon Press, 1949.
[30]
J. Korevaar, Tauberian theory: A century of developments, vol. 329. Berlin: Springer, 2004.
[31]
A. Joyal, R. Street, and D. Verity, “Traced monoidal categories,” Mathematical Proceedings of the Cambridge Philosophical Society, vol. 119, no. 3, pp. 447–468, 1996, doi: 10.1017/S0305004100074338.
[32]
M. Hasegawa, “Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi,” in Typed lambda calculi and applications, 1997, vol. 1210, pp. 196–213, doi: 10.1007/3-540-62688-3_37.
[33]
S. Goncharov and L. Schröder, “Guarded traced categories,” Logical Methods in Computer Science, vol. 14, no. 3, 2018, doi: 10.23638/LMCS-14(3:10)2018.
[34]
E. Haghverdi and P. J. Scott, “A categorical model for the geometry of interaction,” Theoretical Computer Science, vol. 350, no. 2–3, pp. 252–274, 2006, doi: 10.1016/j.tcs.2005.10.028.
[35]
I. Hasuo and N. Hoshino, “Semantics of higher-order quantum computation via geometry of interaction,” Annals of Pure and Applied Logic, vol. 168, no. 2, pp. 404–469, 2017, doi: 10.1016/j.apal.2016.10.010.
[36]
J.-P. Magnot, “On smooth infinite dimensional grassmannians, splittings and non-commutative generalized cross-ratio mappings,” arXiv preprint arXiv:2404.16888, 2024, doi: 10.48550/arXiv.2404.16888.
[37]
I. C. Gohberg and M. G. Krein, Introduction to the theory of linear nonselfadjoint operators, vol. 18. Providence, RI: American Mathematical Society, 1969.
[38]
B. Simon, Trace ideals and their applications, 2nd ed., vol. 120. Providence, RI: American Mathematical Society, 2005.
[39]
A. Paetznick and K. M. Svore, “Repeat-until-success: Non-deterministic decomposition of single-qubit unitaries,” Quantum Information and Computation, vol. 14, no. 15–16, pp. 1277–1301, 2014, doi: 10.26421/QIC14.15-16-2.