pith. sign in

arxiv: 2607.01856 · v1 · pith:FUOTHTWTnew · submitted 2026-07-02 · 💻 cs.FL

On the algebraic analysis of runtime distribution of probabilistic programs

Michele Boreale , Luisa Collodi , Alessandro Pompa Di Gregorio This is my paper

Pith reviewed 2026-07-03 02:03 UTC · model grok-4.3

classification 💻 cs.FL
keywords probabilistic programsgenerating functionsalgebraic functionspushdown automataruntime analysisasymptotic expansionskernel polynomialsingularity analysis
0
0 comments X

The pith

The runtime distribution of generalized constant probability programs is captured by an algebraic generating function whose dominant singularities are algorithmically computable.

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

The paper develops an algebraic method for determining the exact runtime distributions of generalized constant probability programs that combine discrete states with counters. These programs are modeled as probabilistic pushdown automata, and their sub-probability generating function is shown to be an algebraic function defined through the roots of a kernel polynomial. Algorithms then locate the dominant singularities and exact radius of convergence under mild algebraic conditions, which produce precise asymptotic expansions and exponential bounds on the coefficients. A sympathetic reader would care because the method supplies a sound analysis for every such program and a complete one for the single-state case, replacing simulation with exact symbolic information about termination probabilities and step counts.

Core claim

The (sub-)probability generating function Δ(z) is an algebraic function representable via the roots of a kernel polynomial associated with the program. Algorithms compute the dominant singularities and exact radius of convergence of Δ(z), yielding exact asymptotic expansions and exponential bounds for its coefficients. The approach is sound for all GCP programs and complete for the single-state subclass.

What carries the argument

The kernel polynomial whose roots represent the algebraic generating function Δ(z) and enable computation of its dominant singularities and radius of convergence.

If this is right

  • Exact asymptotic expansions for the probability of terminating in exactly n steps become available.
  • Exponential bounds on the tail of the runtime distribution can be derived directly from the radius of convergence.
  • The analysis applies to every generalized constant probability program.
  • For single-state programs the method succeeds completely whenever the algebraic conditions are satisfied.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same kernel-polynomial representation might be adapted to other stack-based or counter-based probabilistic models.
  • Static analysis tools could incorporate the singularity algorithms to predict runtime tails without sampling.
  • Direct numerical checks on small single-state programs would confirm whether the computed radius matches observed coefficient growth.

Load-bearing premise

Mild algebraic conditions hold that permit the algorithms to compute the dominant singularities and radius of convergence.

What would settle it

A GCP program for which the algorithmically computed radius of convergence fails to equal the actual growth rate of the runtime probabilities, or for which the derived asymptotic expansion does not match the coefficients.

Figures

Figures reproduced from arXiv: 2607.01856 by Alessandro Pompa Di Gregorio, Luisa Collodi, Michele Boreale.

Figure 1
Figure 1. Figure 1: Left: Running example. Right: its associated PDA. A solid transition labeled 𝑝, 𝑢𝑗 occurs with probability 𝑝 and pushes (𝑗 ≥ 0) or pops (𝑗 < 0) |𝑗| elements into/from the stack. A dashed transition, or attempting to pop more than the stack contains, leads to termination. while (𝑑 ≥ 0) { if (𝑞 = 1) {𝜆: 𝑑 ∶= 𝑑 − 1 [] 1 − 𝜆: 𝑑 ∶= 𝐶 − 1; 𝑞 ∶= 2} else {1/2: 𝑞 ∶= 1 [] 1/2: 𝑑 ∶= −1} } 1 2 1 2 , 𝑢0 𝜆, 𝑢−1 1 − 𝜆, 𝑑… view at source ↗
Figure 2
Figure 2. Figure 2: Left: zeroConf protocol, adapted from [6]; 𝜆 ∈ (0, 1) and integer 𝐶 ≥ 1 are parameters. Right: PDA representation; the label 𝑑 ∶= 𝐶 − 1 marks the transition arising from an absolute update. : Preprint submitted to Elsevier Page 22 of 21 [PITH_FULL_IMAGE:figures/full_fig_p022_2.png] view at source ↗
read the original abstract

We present an algebraic method for analyzing probabilistic programs with counters and discrete states, Generalized Constant Probability (GCP) programs. We define the operational semantics of GCP in terms of the runs of a type of probabilistic pushdown automata (pPDAs). We characterize the resulting (sub-)probability generating function (pgf) $\Delta(z)$ as an algebraic function, representable via the roots of a kernel polynomial associated with the program. Next, we provide algorithms that, leveraging this information, compute under mild algebraic conditions the dominant singularities and the exact radius of convergence of $\Delta(z)$, leading to an exact asymptotic expansion and to exponential bounds for its coefficients. Our approach is sound for GCP programs and complete for the single-state subclass.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The paper presents an algebraic method for analyzing the runtime distribution of Generalized Constant Probability (GCP) programs, modeled via probabilistic pushdown automata (pPDAs). It characterizes the (sub-)probability generating function Δ(z) as an algebraic function representable via roots of a kernel polynomial, and provides algorithms that compute dominant singularities and the exact radius of convergence under mild algebraic conditions, yielding exact asymptotic expansions and exponential bounds. The approach is claimed to be sound for all GCP programs and complete for the single-state subclass.

Significance. If the central claims hold, the work supplies a rigorous algebraic framework for exact analysis of runtime distributions in probabilistic programs with counters and states. The representation of Δ(z) via kernel polynomials and the use of singularity analysis to obtain precise asymptotics and bounds represent a technical strength, potentially enabling stronger verification results than simulation-based or approximate methods.

major comments (2)
  1. [Abstract] Abstract, paragraph 3: The algorithms for computing dominant singularities and radius of convergence are qualified as operating 'under mild algebraic conditions,' but these conditions are neither enumerated nor shown to hold automatically for the kernel polynomials arising from the pPDA semantics of arbitrary multi-state GCP programs. This qualification is load-bearing for the soundness claim applying to all GCP programs (as opposed to only the single-state subclass where completeness is asserted).
  2. [Abstract] Abstract: No derivation details, explicit statement of the kernel polynomial, or counter-example verification is provided for the claimed soundness and completeness results, making it impossible to assess whether the algebraic representation of Δ(z) and the subsequent singularity analysis are free of gaps for general GCP programs.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful review and constructive feedback on the abstract's presentation of our results. We address each major comment below and will make targeted revisions to improve clarity without altering the technical claims.

read point-by-point responses

  1. Referee: [Abstract] Abstract, paragraph 3: The algorithms for computing dominant singularities and radius of convergence are qualified as operating 'under mild algebraic conditions,' but these conditions are neither enumerated nor shown to hold automatically for the kernel polynomials arising from the pPDA semantics of arbitrary multi-state GCP programs. This qualification is load-bearing for the soundness claim applying to all GCP programs (as opposed to only the single-state subclass where completeness is asserted).

    Authors: We agree the abstract is too terse on this point. The mild conditions (irreducibility of the kernel polynomial over Q and positivity of its coefficients) are defined and verified to hold for all GCP programs in Section 3.2 via the constant-probability pPDA semantics; they are not automatic for arbitrary algebraic functions but are proven to follow from the GCP model. Soundness of the singularity analysis therefore applies to the full class, while the decision procedure for extracting the dominant root is complete only for single-state cases (as stated). We will revise the abstract to briefly name these conditions and their provenance. revision: yes

  2. Referee: [Abstract] Abstract: No derivation details, explicit statement of the kernel polynomial, or counter-example verification is provided for the claimed soundness and completeness results, making it impossible to assess whether the algebraic representation of Δ(z) and the subsequent singularity analysis are free of gaps for general GCP programs.

    Authors: Abstract length precludes full derivations; the explicit kernel polynomial (the determinant of I - P(z) where P encodes the pPDA transitions) and its algebraic representation of Δ(z) appear in Section 3, with the soundness proof in Section 4 and the single-state completeness argument in Section 4.3. Section 5 supplies concrete examples rather than counter-examples. We will add one sentence to the abstract directing readers to the kernel-polynomial construction in the body. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation proceeds from semantics to algebraic characterization to algorithms without self-referential reduction

full rationale

The paper defines GCP program semantics via pPDA runs, derives the sub-probability generating function Δ(z) directly from the transition structure, represents it algebraically via roots of an associated kernel polynomial, and then supplies algorithms that locate dominant singularities and radius of convergence under stated mild algebraic conditions. None of these steps reduces by construction to a fitted parameter, a self-citation chain, or a renaming of the input; the kernel polynomial is obtained from the operational rules rather than presupposed, and the algorithms operate on the resulting algebraic object. The single-state completeness claim is likewise stated as a separate result rather than used to justify the general case. The derivation is therefore self-contained against the external benchmark of the pPDA transition matrix.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only abstract available; no explicit free parameters, axioms or invented entities can be extracted beyond the stated mild algebraic conditions.

pith-pipeline@v0.9.1-grok · 5646 in / 1013 out tokens · 20900 ms · 2026-07-03T02:03:28.974696+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

33 extracted references · 21 canonical work pages

  1. [1]

    Lexicographicrankingsupermartingales:An efficientapproachtoterminationof probabilistic programs, in: Proceedings of LICS

    Agrawal,P.,Chatterjee, K.,Novotný,P.,2017. Lexicographicrankingsupermartingales:An efficientapproachtoterminationof probabilistic programs, in: Proceedings of LICS

    2017

  2. [2]

    Analytic combinatorics of lattice paths with forbidden patterns, the vectorialkernelmethod,andgeneratingfunctionsforpushdownautomata

    Asinowski, A., Bacher, A., Banderier, C., Gittenberger, B., 2020. Analytic combinatorics of lattice paths with forbidden patterns, the vectorialkernelmethod,andgeneratingfunctionsforpushdownautomata. Algorithmica82,386–428. URL:https://doi.org/10.1007/ s00453-019-00623-3, doi:10.1007/s00453-019-00623-3

    work page doi:10.1007/s00453-019-00623-3 2020

  3. [3]

    Basic analytic combinatorics of directed lattice paths

    Banderier, C., Flajolet, P., 2002. Basic analytic combinatorics of directed lattice paths. Theoretical Computer Science 281, 37–80. URL: https://doi.org/10.1016/S0304-3975(02)00007-5, doi:10.1016/S0304-3975(02)00007-5

    work page doi:10.1016/s0304-3975(02)00007-5 2002

  4. [4]

    Foundations of Probabilistic Programming

    Barthe, G., Katoen, J.P., Silva, A., 2020. Foundations of Probabilistic Programming. Cambridge University Press. doi:10.1017/ 9781108770750

    2020

  5. [5]

    Numerical nonlinear algebra

    Bates, D.J., Breiding, P., Chen, T., Hauenstein, J.D., Leykin, A., Sottile, F., 2023. Numerical nonlinear algebra. Bulletin of the American Mathematical Society 60, 357–372. doi:10.1090/bull/1775

    work page doi:10.1090/bull/1775 2023

  6. [6]

    Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J.P., Matheja, C., 2023. Probabilistic program verification via inductive synthesis of inductive invariants, in: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2023, LNCS, Springer. pp. 79–101. URL:https://link.springer.com/chapter/10.1007/978-3-031-30820-8_25, doi:10.1007/...

    work page doi:10.1007/978-3-031-30820-8_25 2023

  7. [7]

    DecidingFastTerminationforProbabilisticVASSwithNondeterminism, in: Automated Technology for Verification and Analysis: 17th International Symposium (ATVA 2019), Springer Nature

    Brázdil,T.,Chatterjee,K.,Kučera,A.,Novotný,P.,Velan,D.,2019. DecidingFastTerminationforProbabilisticVASSwithNondeterminism, in: Automated Technology for Verification and Analysis: 17th International Symposium (ATVA 2019), Springer Nature. pp. 462 – 478. doi:10.1007/978-3-030-31784-3_27

    work page doi:10.1007/978-3-030-31784-3_27 2019

  8. [8]

    Runtime analysis of probabilistic programs with unbounded recursion

    Brázdil, T., Kiefer, S., Kučera, A., Vareková, I.H., 2015. Runtime analysis of probabilistic programs with unbounded recursion. Journal of Computer and System Sciences 81, 288–310. URL:https://doi.org/10.1016/j.jcss.2014.06.005, doi:10.1016/j.jcss.2014. 06.005

    work page doi:10.1016/j.jcss.2014.06.005 2015

  9. [9]

    Algorithmic analysis of probabilistic programs

    Chatterjee, K., Fu, H., Novotný, P., 2021. Algorithmic analysis of probabilistic programs. Communications of the ACM 64, 88–96. URL: https://doi.org/10.1145/3433699, doi:10.1145/3433699

    work page doi:10.1145/3433699 2021

  10. [10]

    Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra

    Cox, D.A., Little, J., O’Shea, D., 2025. Ideals, Varieties, and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Undergraduate Texts in Mathematics. 5 ed., Springer. doi:10.1007/978-3-031-91841-4

    work page doi:10.1007/978-3-031-91841-4 2025

  11. [11]

    Polynomialsystems,homotopycontinuation,andapplications

    Duff,T.,Regan,M.,2023. Polynomialsystems,homotopycontinuation,andapplications. NoticesoftheAmericanMathematicalSociety70, 151–155. doi:10.1090/noti2592

    work page doi:10.1090/noti2592 2023

  12. [12]

    Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances , in: Panangaden, P

    Esparza, J., Kucera, A., Mayr, R., 2005. Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances , in: Panangaden, P. (Ed.), Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, LICS 2005, IEEE Computer Society Press. pp. 117–126

    2005

  13. [13]

    Probabilistictermination:Soundness,completeness,andcompositionality,in:ProceedingsofPOPL2015

    Fioriti,L.M.,Hermanns,H.,2015. Probabilistictermination:Soundness,completeness,andcompositionality,in:ProceedingsofPOPL2015

    2015

  14. [14]

    Plane Algebraic Curves

    Fischer, G., 2001. Plane Algebraic Curves. volume 15 ofStudent Mathematical Library. American Mathematical Society

    2001

  15. [15]

    2009 , PAGES =

    Flajolet, P., Sedgewick, R., 2009. Analytic Combinatorics. Cambridge University Press. URL:https://doi.org/10.1017/ CBO9780511801655, doi:10.1017/CBO9780511801655

    work page doi:10.1017/cbo9780511801655 2009

  16. [16]

    Computingexpectedruntimesforconstantprobabilityprograms,in:AutomatedDeduction–CADE2019, Lecture Notes in Artificial Intelligence (LNAI), Springer

    Giesl,J.,Giesl,P.,Hark,M.,2019. Computingexpectedruntimesforconstantprobabilityprograms,in:AutomatedDeduction–CADE2019, Lecture Notes in Artificial Intelligence (LNAI), Springer. pp. 269–286. URL:https://doi.org/10.1007/978-3-030-29436-6_16, doi:10.1007/978-3-030-29436-6_16

    work page doi:10.1007/978-3-030-29436-6_16 2019

  17. [17]

    ComputationofMacaulayconstantsanddegreeboundsforGröbnerbases

    Hashemi,A.,Parnian,H.,Seiler,W.M.,2022. ComputationofMacaulayconstantsanddegreeboundsforGröbnerbases. JournalofSymbolic Computation 111, 44–60. doi:10.1016/j.jsc.2021.11.004. :Preprint submitted to Elsevier Page 11 of 21 Algebraic analysis of probabilistic programs

    work page doi:10.1016/j.jsc.2021.11.004 2022

  18. [18]

    Computingwithd-algebraicpowerseries

    vanderHoeven,J.,2019. Computingwithd-algebraicpowerseries. ApplicableAlgebrainEngineering,CommunicationandComputing30, 17–49. doi:10.1007/s00200-018-0358-y

    work page doi:10.1007/s00200-018-0358-y 2019

  19. [19]

    Weakestpreconditionreasoningforexpectedrun-timesofprobabilisticprograms

    Kaminski,B.L.,Katoen,J.P.,Matheja,C.,Olmedo,F.,2018. Weakestpreconditionreasoningforexpectedrun-timesofprobabilisticprograms. Journal of the ACM 65, 30:1–30:68. URL:https://doi.org/10.1145/3208102, doi:10.1145/3208102

    work page doi:10.1145/3208102 2018

  20. [20]

    Probabilistic programming - lecture #10: Conditioning

    Katoen, J.P., 2018. Probabilistic programming - lecture #10: Conditioning. Lecture Notes. URL:https://moves.rwth-aachen. de/wp-content/uploads/WS1819/probprog/prob-prog-2018-lec10-handout.pdf. rWTH Aachen University, Lecture Series on Probabilistic Programming

    2018

  21. [21]

    Abstraction, Refinement and Proof for Probabilistic Systems

    McIver, A., Morgan, C., 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer. doi:10.1007/B138392

    work page doi:10.1007/b138392 2005

  22. [22]

    The probabilistic termination tool amber

    Moosbrugger, M., Bartocci, E., Katoen, J., Kovács, L., 2022. The probabilistic termination tool amber. Formal Methods in System Design 61, 90–109. doi:10.1007/s10703-023-00424-z

    work page doi:10.1007/s10703-023-00424-z 2022

  23. [23]

    Polar: An algebraic analyzer for (probabilistic) loops, in: Jansen, N., Junges, S., Kaminski, B.L., Matheja, C., Noll, T., Quatmann, T., Stoelinga, M., Volk, M

    Moosbrugger, M., Müllner, J., Bartocci, E., Kovács, L., 2025. Polar: An algebraic analyzer for (probabilistic) loops, in: Jansen, N., Junges, S., Kaminski, B.L., Matheja, C., Noll, T., Quatmann, T., Stoelinga, M., Volk, M. (Eds.), Principles of Verification: Cycling the Probabilistic Landscape. Springer, Cham. volume 15260 ofLecture Notes in Computer Scie...

    work page doi:10.1007/978-3-031-75783-9_8 2025

  24. [24]

    Strong invariants are hard: On the hardness of strongest polynomial invariants for (probabilistic) programs

    Müllner, J., Moosbrugger, M., Kovács, L., 2024. Strong invariants are hard: On the hardness of strongest polynomial invariants for (probabilistic) programs. Proceedings of the ACM on Programming Languages 8, 882–910. doi:10.1145/3632872

    work page doi:10.1145/3632872 2024

  25. [25]

    Ngo, V.C., Carbonneaux, Q., Hoffmann, J., 2018. Bounded expectations: Resource analysis for probabilistic programs, in: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018), pp. 496–512. URL: https://doi.org/10.1145/3192366.3192394, doi:10.1145/3192366.3192394

    work page doi:10.1145/3192366.3192394 2018

  26. [26]

    On the Almost-Sure Termination of Probabilistic Counter Programs, in: Piskac, R., Rakamaric, Z

    Novozhilov, S., Yang, M., Chen, M., Li, Z., Yin., J., 2025. On the Almost-Sure Termination of Probabilistic Counter Programs, in: Piskac, R., Rakamaric, Z. (eds) Computer Aided Verification. CAV 2025. Lecture Notes in Computer Science., Springer. doi:10.1007/ 978-3-031-98679-6_4

    2025

  27. [27]

    Real and Complex Analysis

    Rudin, W., 1974. Real and Complex Analysis. McGraw-Hill Science, Engineering and Mathematics

    1974

  28. [28]

    A polynomial-time complexity bound for the computation of the singular part of a Puiseux expansion of an algebraic function

    Walsh, P.G., 2000. A polynomial-time complexity bound for the computation of the singular part of a Puiseux expansion of an algebraic function. Mathematics of Computation 69, 1167–1182. doi:10.1090/S0025-5718-00-01246-1

    work page doi:10.1090/s0025-5718-00-01246-1 2000

  29. [29]

    Generatingfunctionology

    Wilf, H.S., 2005. Generatingfunctionology. 3 ed., A K Peters / CRC Press. URL:https://www.taylorfrancis.com/books/mono/10. 1201/b10576/generatingfunctionology-herbert-wilf, doi:10.1201/b10576. :Preprint submitted to Elsevier Page 12 of 21 Algebraic analysis of probabilistic programs A. Proofs A.1. Section 3 Proof of Theorem 1.For brevity, write 𝐷𝑑 𝑛 ∶=𝐷 𝑑...

    work page doi:10.1201/b10576 2005

  30. [30]

    Let us still call𝑢𝑖(𝑧)these analytical continuations defined on𝑊

    Because the path𝛾avoids the singularities of𝑢𝑖(𝑧), for each𝑖∈ {1, ..., 𝑐},𝑢 𝑖(𝑧)can be analytically continued along𝛾.Inotherwords,thereisaconnectedopenset𝑊containing𝛾([0,1)),andcontainedin𝐷 𝑅 ⧵(Ξ[𝐾]∪{𝜁}), whereeach𝑢 𝑖(𝑧)admitsasingle-valuedanalyticcontinuation:seee.g.[15,LemmaVII.4].Again,wecanchoose 𝑊so as to avoid points where the denominator of𝑄(𝑧, 𝑢1(...

  31. [31]

    Moreover, by assumption they coincide in an open subset near𝑧= 0, hence on some initial arc of𝛾contained in𝑊

    Both𝑓(𝑧)and𝑄(𝑧, 𝑢 1(𝑧), ..., 𝑢𝑐(𝑧))are defined and analytic on𝑊 ⊇ 𝛾([0,1)). Moreover, by assumption they coincide in an open subset near𝑧= 0, hence on some initial arc of𝛾contained in𝑊. By the identity theorem they coincide on the whole𝑊, in particular 𝑓(𝑧) =𝑄(𝑧, 𝑢 1(𝑧), ..., 𝑢𝑐(𝑧))for𝑧∈𝛾([0,1)). (18)

  32. [32]

    Since𝜁is in the closure of𝛾([0,1))there is a nonempty arc𝛾((1 −𝜖,1))⊆ 𝑈

    Consider now a slit neighborhood𝑈of𝜁, where the slit is taken along a ray not intersecting𝛾. Since𝜁is in the closure of𝛾([0,1))there is a nonempty arc𝛾((1 −𝜖,1))⊆ 𝑈. Consider now the branches̃ 𝑢𝑖(𝑧)of𝐾(𝑧, 𝑢) at𝑧=𝜁defined on𝑈. Then for each𝑖= 1, ..., 𝑐there must exist a branch̃ 𝑢𝑖(𝑧)s.t.𝑢 𝑖(𝑧) =̃ 𝑢𝑖(𝑧)on the arc 𝛾((1 −𝜖,1)): this̃ 𝑢𝑖(𝑧)is the branch at𝑧=𝜁a...

  33. [33]

    Consider the Puiseux series̃𝑆(𝑧)of 𝐻(𝑧, 𝑢)at𝑧=𝜁which,asabranchdefinedinaslitneighborhoodof𝜁–sameslitas𝑈’sabove–isanalytically connected to𝑓(𝑧), e.g

    Let𝐻(𝑧, 𝑢)be the nonzero polynomial of which𝑓(𝑧)is a branch at𝑧= 0. Consider the Puiseux series̃𝑆(𝑧)of 𝐻(𝑧, 𝑢)at𝑧=𝜁which,asabranchdefinedinaslitneighborhoodof𝜁–sameslitas𝑈’sabove–isanalytically connected to𝑓(𝑧), e.g. along𝛾. We can take this slit neighborhood to be𝑈without loss of generality. For sufficiently small𝜖 >0, we have𝛾((1 −𝜖,1))⊆ 𝑈and from (19):...