pith. sign in

arxiv: 2606.22238 · v1 · pith:QGQV5IKPnew · submitted 2026-06-20 · 💻 cs.PL

Powerdomains and nondeterminism in synthetic domain theory

Yue Niu , Taro Sekiyama This is my paper

Pith reviewed 2026-06-26 10:36 UTC · model grok-4.3

classification 💻 cs.PL
keywords synthetic domain theorypowerdomainsnondeterminismcomputational adequacydenotational semanticsdependent type theorymetalanguage
0
0 comments X

The pith

Synthetic domain theory contains computationally adequate powerdomains for nondeterminism.

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

The paper constructs the lower, upper, and convex powerdomains inside synthetic domain theory. Synthetic domain theory is an axiomatic setting in which every definable map between domains is continuous. The constructions are shown to yield denotational models of nondeterminism that are computationally adequate. These models support a nondeterministic metalanguage that embeds directly into dependent type theory, which then serves as a logic for reasoning about the metalanguage. Computational adequacy further implies that denotational arguments can be used to analyze the operational behavior of concrete programs.

Core claim

In synthetic domain theory the lower, upper, and convex powerdomains can be defined using the background axioms, and the resulting structures furnish computationally adequate denotational models of nondeterminism. The metalanguage based on these models embeds into dependent type theory, supplying an expressive logic for reasoning, while the adequacy theorems guarantee that denotational reasoning applies to the operational semantics of actual programs.

What carries the argument

The synthetic lower, upper, and convex powerdomains, constructed so that they inherit the automatic continuity of all definable maps from the ambient synthetic domain theory.

If this is right

  • A nondeterministic metalanguage embeds directly into dependent type theory.
  • Dependent type theory becomes an expressive logic in which to reason about the metalanguage.
  • Denotational arguments through the metalanguage apply to the operational behavior of programs.
  • All maps definable from the powerdomains remain continuous by construction.

Where Pith is reading between the lines

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

  • The same axiomatic approach might be used to internalize other computational effects while retaining continuity and adequacy.
  • The embedding into dependent type theory could support machine-checked proofs of properties of nondeterministic programs.
  • Operational equivalence proofs for nondeterministic languages might be carried out entirely inside the synthetic setting.

Load-bearing premise

The axioms of synthetic domain theory are strong enough to define the three powerdomains while keeping every definable map continuous and while supporting the computational-adequacy proofs.

What would settle it

An explicit definition, inside the theory, of a map between any of the constructed powerdomains that fails to be continuous, or a concrete nondeterministic program whose operational behavior is not matched by its denotational semantics in the model.

Figures

Figures reproduced from arXiv: 2606.22238 by Taro Sekiyama, Yue Niu.

Figure 1
Figure 1. Figure 1: Left: the free pre-lower semilattice HX as a quotient type; right: the free pre-upper semilattice GX. The only difference between the two types is the swapped boundary of the constructor l corresponding to the axioms S ⊑p S ∨ T and S ∨ T ⊑ S respectively. The second property we need may be shown by S-induction. Proposition 40. The synthetic predomain reflection S : E → C restricts to the left adjoint to th… view at source ↗
read the original abstract

Synthetic domain theory is an axiomatization of domain theory within a constructive universe of sets such that all definable maps between domains are continuous. In this paper we construct the counterparts to the well-known lower, upper, and convex powerdomains in the setting of synthetic domain theory and prove that they produce computationally adequate denotational models of nondeterminism. By developing the theory of powerdomains in synthetic domain theory, we obtain a nondeterministic metalanguage that directly embeds into dependent type theory, where the latter serves as an expressive logic for reasoning about the metalanguage. Moreover, the computational adequacy results imply that denotational reasoning through the metalanguage may be used to study operational behaviors of actual programs.

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

0 major / 2 minor

Summary. The paper constructs the lower, upper, and convex powerdomains inside the axiomatic framework of synthetic domain theory (where all definable maps are continuous by construction) and proves that the resulting structures yield computationally adequate denotational models of nondeterminism. The adequacy proofs relate the denotational semantics directly to an operational semantics via the embedding of the nondeterministic metalanguage into dependent type theory, which then serves as a logic for reasoning about the metalanguage.

Significance. If the constructions and adequacy proofs hold, the work supplies a nondeterministic metalanguage that inherits automatic continuity from synthetic domain theory while supporting direct embedding into DTT. This is a clear strength: the adequacy results allow denotational reasoning to be transferred to operational behavior without additional continuity arguments, and the constructive setting avoids classical domain-theoretic overhead. The approach is parameter-free with respect to the background axioms of synthetic domain theory.

minor comments (2)
  1. [Abstract] The abstract states that the powerdomains 'produce computationally adequate denotational models,' but the precise statement of adequacy (e.g., the relation between denotational and operational semantics) is not previewed; a one-sentence clarification would help readers locate the main theorem.
  2. [§2] Notation for the three powerdomain constructions (lower, upper, convex) is introduced without an early comparison table; adding such a table in §2 or §3 would make the differences in the synthetic setting easier to track.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the paper and for recommending acceptance. The report contains no major comments requiring a point-by-point response.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper constructs lower, upper, and convex powerdomains directly from the axioms of synthetic domain theory (SDT), which enforce continuity of all definable maps by construction. Computational adequacy is then proved by embedding the denotational semantics into dependent type theory and relating it to an operational semantics; these steps rely on the independent SDT axioms and standard domain-theoretic arguments rather than any self-referential definition, fitted parameter renamed as prediction, or load-bearing self-citation chain. No equation or theorem reduces to its own input by construction, and the central claims remain externally falsifiable against operational behavior.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on the axioms of synthetic domain theory that enforce continuity of definable maps; these are background assumptions imported from prior literature rather than derived here.

axioms (1)
  • domain assumption Axioms of synthetic domain theory ensuring all definable maps between domains are continuous
    The entire development is carried out inside synthetic domain theory, whose continuity axiom is invoked to obtain the desired properties of the powerdomains.

pith-pipeline@v0.9.1-grok · 5635 in / 1172 out tokens · 27411 ms · 2026-06-26T10:36:15.203630+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

37 extracted references · 25 canonical work pages

  1. [1]

    Barr, M. and C. Wells,Toposes, Triples, and Theories, Grundlehren der mathematischen Wissenschaften, Springer-Verlag (1985), ISBN 9780387961156. https://books.google.co.jp/books?id=e-iMPwAACAAJ

    1985

  2. [2]

    Birkedal, L., R. E. Mogelberg, J. Schwinghammer and K. Stovring,First steps in synthetic guarded domain theory: Step-indexing in the topos of trees, in:2011 IEEE 26th Annual Symposium on Logic in Computer Science, pages 55–64 (2011). https://doi.org/10.1109/LICS.2011.16

    work page doi:10.1109/lics.2011.16 2011

  3. [3]

    Fiore, M. P.,An enrichment theorem for an axiomatisation of categories of domains and continuous functions, Mathematical Structures in Com- puter Science7, pages 591–618 (1997), ISSN 1469-8072, 0960-1295. https://doi.org/10.1017/S0960129597002429 36

    work page doi:10.1017/s0960129597002429 1997

  4. [4]

    Fiore, M. P., A. M. Pitts and S. C. Steenkamp,Quotients, inductive types, and quotient inductive types, lmcsVolume 18, Issue 2(2022). https://doi.org/10.46298/lmcs-18(2:15)2022

    work page doi:10.46298/lmcs-18(2:15)2022 2022

  5. [5]

    Fiore, M. P. and G. D. Plotkin,An extension of models of axiomatic domain theory to models of synthetic domain theory, in: D. van Dalen and M. Bezem, editors,Computer Science Logic, 10th International Workshop, CSL ’96, Annual Conference of the EACSL, Utrecht, The Netherlands, September 21-27, 1996, Selected Papers, volume 1258 of Lecture Notes in Compute...

    work page doi:10.1007/3-540-63172-0_36 1996

  6. [6]

    Fiore, M. P. and G. Rosolini,The category of cpos from a synthetic view- point, in: S. D. Brookes and M. W. Mislove, editors,Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, MFPS 1997, Carnegie Mellon University, Pittsburgh, PA, USA, March 23-26, 1997, volume 6 ofElectronic Notes in Theoretical Computer Science, pages 133–...

    work page doi:10.1016/s1571-0661(05)80165-3 1997

  7. [7]

    Fiore, M. P. and G. Rosolini,Two models of synthetic domain theory 116, pages 151–162, ISSN 0022-4049. https://doi.org/10.1016/S0022-4049(96)00164-8

    work page doi:10.1016/s0022-4049(96)00164-8

  8. [8]

    Geuvers, L

    Frumin, D., H. Geuvers, L. Gondelman and N. v. d. Weide,Finite sets in homotopy type theory, in:Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, page 201–214, Association for Computing Machinery, New York, NY, USA (2018), ISBN 9781450355865. https://doi.org/10.1145/3167085

    work page doi:10.1145/3167085 2018

  9. [9]

    Gunter, C. A., P. D. Mosses and D. S. Scott,Semantic Domains and Denotational Semantics

  10. [10]

    Hennessy, M. C. B. and G. D. Plotkin,Full abstraction for a simple parallel programming language, in: J. Beˇ cv´ aˇ r, editor,Mathematical Foundations of Computer Science 1979, pages 108–120, Springer, Berlin, Heidelberg (1979), ISBN 978-3-540-35088-0. https://doi.org/10.1007/3-540-09526-8_8

    work page doi:10.1007/3-540-09526-8_8 1979

  11. [11]

    Hyland, J. M. E.,First steps in synthetic domain theory, in: A. Carboni, M. C. Pedicchio and G. Rosolini, editors,Category Theory, pages 131– 156, Springer Berlin Heidelberg, ISBN 978-3-540-46435-8

  12. [12]

    Hutchison, T

    Katsumata, S.-y.,A Semantic Formulation of tt-Lifting and Logical Pred- icates for Computational Metalanguage, in: D. Hutchison, T. Kanade, 37 J. Kittler, J. M. Kleinberg, F. Mattern, J. C. Mitchell, M. Naor, O. Nier- strasz, C. Pandu Rangan, B. Steffen, M. Sudan, D. Terzopoulos, D. Ty- gar, M. Y. Vardi, G. Weikum and L. Ong, editors,Computer Science Logi...

    work page doi:10.1007/11538363_8 2005

  13. [13]

    Carboni, M

    Kock, A.,Algebras for the partial map classifier monad, in: A. Carboni, M. C. Pedicchio and G. Rosolini, editors,Category Theory, pages 262– 278, Springer Berlin Heidelberg, Berlin, Heidelberg (1991), ISBN 978-3- 540-46435-8

    1991

  14. [14]

    B.,Call-By-Push-Value, Ph.D

    Levy, P. B.,Call-By-Push-Value, Ph.D. thesis (2001). https://www.cs.bham.ac.uk/˜pbl/papers/thesisqmwphd.pdf

    2001

  15. [15]

    Moss, and Sam Staton

    Matache, C., S. Moss and S. Staton,Concrete categories and higher-order recursion: With applications including probability, differentiability, and full abstraction, in:Proceedings of the 37th Annual ACM/IEEE Sympo- sium on Logic in Computer Science, LICS ’22, Association for Computing Machinery, New York, NY, USA (2022), ISBN 9781450393515. https://doi.or...

    work page doi:10.1145/3531130.3533370 2022

  16. [16]

    Milne, G. and R. Milner,Concurrent processes and their syntax, J. ACM 26, page 302–321 (1979), ISSN 0004-5411. https://doi.org/10.1145/322123.322134

    work page doi:10.1145/322123.322134 1979

  17. [17]

    Møgelberg, R. and A. Vezzosi,Two guarded recursive powerdomains for applicative simulation, Electronic Proceedings in Theoretical Computer Science351, pages 200–217 (2021). https://doi.org/10.4204/EPTCS.351.13

    work page doi:10.4204/eptcs.351.13 2021

  18. [18]

    A modality for recursion

    Nakano, H.,A modality for recursion, in:Proceedings of the Fifteenth Annual IEEE Symposium on Logic in Computer Science, pages 255–266, IEEE Computer Society, ISSN 1043-6871. https://doi.org/10.1109/LICS.2000.855774

    work page doi:10.1109/lics.2000.855774 2000

  19. [19]

    Sterling and R

    Niu, Y., J. Sterling and R. Harper,Cost-sensitive computational ade- quacy of higher-order recursion in synthetic domain theory(2024). 40th Conference on Mathematical Foundations of Programming Semantics (MFPS XXXX),2404.00212. https://arxiv.org/abs/2404.00212

    arXiv 2024

  20. [20]

    thesis, Uni- versity of Edinburgh

    Phoa, W.,Domain Theory in Realizability Toposes, Ph.D. thesis, Uni- versity of Edinburgh. 38

  21. [21]

    Maiorov and Gordon M

    Phoa, W.,From Term Models to Domains, Information and Computa- tion109, pages 211–255 (1994), ISSN 0890-5401. https://doi.org/https://doi.org/10.1006/inco.1994.1017

    work page doi:10.1006/inco.1994.1017 1994

  22. [22]

    Phoa, W. and P. Taylor,The Synthetic Plotkin Powerdomain(1990)

    1990

  23. [23]

    D.,A Powerdomain Construction, SIAM Journal on Comput- ing5, pages 452–487 (1976)

    Plotkin, G. D.,A Powerdomain Construction, SIAM Journal on Comput- ing5, pages 452–487 (1976). eprint: https://doi.org/10.1137/0205035. https://doi.org/10.1137/0205035

    work page doi:10.1137/0205035 1976

  24. [24]

    D.,A structural approach to operational semantics, Technical Report DAIMI FN-19, University of Aarhus (1981)

    Plotkin, G. D.,A structural approach to operational semantics, Technical Report DAIMI FN-19, University of Aarhus (1981). http://citeseer.ist.psu.edu/plotkin81structural.html

    1981

  25. [25]

    Pugh, L. and J. Sterling,When is the partial map classifier a sierpi´ nski cone?, in:2025 40th Annual ACM/IEEE Symposium on Logic in Com- puter Science (LICS), pages 718–731 (2025). https://doi.org/10.1109/LICS65433.2025.00060

    work page doi:10.1109/lics65433.2025.00060 2025

  26. [26]

    Reus, B.,Program Verification in Synthetic Domain Theory, Ph.D. thesis

  27. [27]

    Shulman and B

    Rijke, E., M. Shulman and B. Spitters,Modalities in homotopy type theory(2020). ArXiv:1706.07526 [cs, math]. https://doi.org/10.23638/LMCS-16(1:2)2020

    work page doi:10.23638/lmcs-16(1:2)2020 2020

  28. [28]

    Rosolini, G.,Continuity and effectiveness in topoi(1986)

    1986

  29. [29]

    Papers presented at the 2002 IEEE Symposium on Logic in Computer Science (LICS)

    Simpson, A.,Computational adequacy for recursive types in models of intuitionistic set theory130, pages 207–275, ISSN 0168-0072. Papers presented at the 2002 IEEE Symposium on Logic in Computer Science (LICS). https://doi.org/10.1016/j.apal.2003.12.005

    work page doi:10.1016/j.apal.2003.12.005 2002

  30. [30]

    K.,Computational Adequacy in an Elementary Topos, in: G

    Simpson, A. K.,Computational Adequacy in an Elementary Topos, in: G. Gottlob, E. Grandjean and K. Seyr, editors,Computer Science Logic, Lecture Notes in Computer Science, pages 323–342, Springer, Berlin, Heidelberg (1999), ISBN 978-3-540-48855-2. https://doi.org/10.1007/10703163_22

    work page doi:10.1007/10703163_22 1999

  31. [31]

    B.,Powerdomains, in: A

    Smyth, M. B.,Powerdomains, in: A. Mazurkiewicz, editor,Mathematical Foundations of Computer Science 1976, pages 537–543, Springer, Berlin, Heidelberg (1976), ISBN 978-3-540-38169-3. https://doi.org/10.1007/3-540-07854-1_226

    work page doi:10.1007/3-540-07854-1_226 1976

  32. [32]

    B.,Power domains and predicate transformers: A topological view, in: J

    Smyth, M. B.,Power domains and predicate transformers: A topological view, in: J. Diaz, editor,Automata, Languages and Programming, pages 662–675, Springer, Berlin, Heidelberg (1983), ISBN 978-3-540-40038-7. https://doi.org/10.1007/BFb0036946 39

    work page doi:10.1007/bfb0036946 1983

  33. [33]

    https://arxiv.org/abs/2312.17023

    Sterling, J.,Tensorial structure of the lifting doctrine in constructive domain theory(2024).2312.17023. https://arxiv.org/abs/2312.17023

    arXiv 2024

  34. [34]

    Gratzer and L

    Sterling, J., D. Gratzer and L. Birkedal,Denotational semantics of general store and polymorphism(2023). ArXiv:2210.02169 [cs]. https://doi.org/10.48550/arXiv.2210.02169

    work page doi:10.48550/arxiv.2210.02169 2023

  35. [35]

    Sterling, J. and R. Harper,Sheaf semantics of termination-insensitive noninterference, pages 5:1–5:19 (2022).2204.09421. https://doi.org/10.4230/LIPIcs.FSCD.2022.5

    work page doi:10.4230/lipics.fscd.2022.5 2022

  36. [36]

    Sterling, J. and L. Ye,Domains and Classifying Topoi(2025). ArXiv:2505.13096 [cs]. https://doi.org/10.48550/arXiv.2505.13096

    work page doi:10.48550/arxiv.2505.13096 2025

  37. [37]

    van Oosten, J. and A. K. Simpson,Axioms and (counter)examples in synthetic domain theory, Annals of Pure and Applied Logic104, pages 233–278 (2000), ISSN 01680072. https://doi.org/10.1016/S0168-0072(00)00014-2 40

    work page doi:10.1016/s0168-0072(00)00014-2 2000