pith. machine review for the scientific record. sign in

arxiv: 2601.23082 · v3 · submitted 2026-01-30 · 💻 cs.LO

Recognition: 2 theorem links

· Lean Theorem

A Complete Finitary Refinement Type System for Scott-Open Properties

Colin Riba , Adam Donadille
Authors on Pith no claims yet

Pith reviewed 2026-05-16 09:22 UTC · model grok-4.3

classification 💻 cs.LO
keywords refinement typesScott domainsspectral spacesfixpoint logicdomain theoryprogram verificationrecursive types
0
0 comments X

The pith

A finitary refinement type system is sound and complete for Scott-open properties of recursive types.

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

The paper builds a type system for proving input-output properties of programs that process infinite data such as streams and non-wellfounded trees. It establishes that this system is complete for Scott-open properties expressed in a logic that uses least and greatest fixpoints. The construction rests on the interpretation of recursive types as spectral spaces, so that positive formulas define Scott-open sets through least fixpoints while negative formulas define compact-saturated sets through greatest fixpoints. A realizability-style implication with polarity variance on function types then lets non-trivial input-output relations appear as positive formulas. The result is a finitary proof system that exactly captures the desired class of properties.

Core claim

We provide a finitary refinement type system which is sound and complete for Scott-open properties defined in a fixpoint-like logic. The system exploits the fact that Scott domains interpreting recursive types are spectral spaces; the symmetry between Scott-open and compact-saturated sets is mirrored by logical polarities, with positive formulas allowing least fixpoints and negative formulas allowing greatest fixpoints. A polarity-respecting realizability implication on function types then formulates input-output properties as positive formulas.

What carries the argument

Polarity-aware realizability implication on function types that preserves Scott-open character of positive formulas by reflecting the open-compact symmetry of spectral spaces.

If this is right

  • Non-trivial input-output properties of functions become expressible as positive formulas on function types.
  • Least fixpoints correspond exactly to positive formulas that define Scott-open sets.
  • Greatest fixpoints correspond to negative formulas that define compact-saturated sets.
  • The system stays finitary while achieving completeness for the targeted class of properties.

Where Pith is reading between the lines

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

  • The polarity mechanism may allow similar completeness results for other classes of properties once an appropriate topological duality is identified.
  • Integration with existing automated provers could turn the finitary character into practical verification tools for infinite-data programs.
  • The spectral-space foundation suggests the technique could transfer to other domain-theoretic settings that admit analogous open-compact dualities.

Load-bearing premise

Scott domains that interpret recursive types are spectral spaces whose topology lets the open-compact symmetry appear as logical polarities.

What would settle it

A concrete Scott-open property of a recursive type, such as a safety property on streams, for which no derivation exists in the refinement type system.

read the original abstract

We are interested in proving input-output properties of functions that handle infinite data such as streams or non-wellfounded trees. We provide a finitary refinement type system which is (sound and) complete for Scott-open properties defined in a fixpoint-like logic. Working on top of Abramsky's Domain Theory in Logical Form, we build from the well-known fact that the Scott domains interpreting recursive types are spectral spaces. The usual symmetry between Scott-open and compact-saturated sets is reflected in logical polarities: positive formulae allow for least fixpoints and define Scott-open sets, while negative formulae allow for greatest fixpoints and define compact-saturated sets. A realizability implication with the expected (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.

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 claims to provide a finitary refinement type system that is sound and complete for Scott-open properties defined in a fixpoint-like logic. It extends Abramsky's Domain Theory in Logical Form by using the spectral space property of Scott domains for recursive types, establishing a polarity symmetry where positive formulae correspond to least fixpoints and Scott-open sets, and negative formulae to greatest fixpoints and compact-saturated sets, with a realizability interpretation for function types to express non-trivial input-output properties.

Significance. If the results hold, this contributes to the field by offering a complete finitary type system for properties of functions on infinite data structures like streams and trees. It builds directly on established domain theory results to achieve both soundness and completeness in a finitary setting, which could have implications for program verification in domains involving recursive types.

minor comments (2)
  1. [Abstract] The phrasing 'which is (sound and) complete' in the abstract is slightly awkward; consider rephrasing to 'which is sound and complete' for better readability.
  2. [Section 2] The background section on spectral spaces would benefit from a brief self-contained reminder of the key duality properties invoked, to reduce dependence on external references for readers.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and the recommendation for minor revision. The work establishes a finitary refinement type system that is sound and complete for Scott-open properties in a fixpoint-like logic, leveraging the spectral space structure of Scott domains for recursive types and a polarity-based distinction between least and greatest fixpoints. No specific major comments were listed in the report, so we have no individual points to address. We are happy to incorporate any minor revisions requested by the editor.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The derivation relies on external background results (Abramsky's Domain Theory in Logical Form and the established spectral-space property of Scott domains for recursive types) rather than any self-definition, fitted-parameter prediction, or load-bearing self-citation. The new finitary refinement type system is constructed on top of these facts, with polarities and realizability following directly from the imported symmetry between Scott-open and compact-saturated sets. No equation or step reduces the completeness claim to the paper's own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The construction rests on standard facts from domain theory; no free parameters or new invented entities are introduced in the abstract.

axioms (1)
  • domain assumption Scott domains interpreting recursive types are spectral spaces
    Invoked as the well-known fact enabling the polarity symmetry for open and compact sets.

pith-pipeline@v0.9.0 · 5430 in / 1037 out tokens · 34381 ms · 2026-05-16T09:22:06.631863+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

  • IndisputableMonolith/Foundation/AlexanderDuality.lean alexander_duality_circle_linking echoes
    ?
    echoes

    ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

    We build from the well-known fact that the Scott domains interpreting recursive types are spectral spaces. The usual symmetry between Scott-open and compact-saturated sets is reflected in logical polarities: positive formulae allow for least fixpoints and define Scott-open sets, while negative formulae allow for greatest fixpoints and define compact-saturated sets.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages

  1. [1]

    Abramsky

    1 S. Abramsky. Domain theory in logical form. InProceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987), pages 47–53. IEEE Computer Society Press, June

    work page 1987

  2. [2]

    doi:10.1016/0168-0072(91)90065-T. 3 S. Abramsky and A. Jung. Domain Theory. In S. Abramsky, D.M. Gabbay, and Maibaum T.S.E., editors,Handbook of Logic in Computer Science, chapter

    work page doi:10.1016/0168-0072(91)90065-t

  3. [3]

    Berger, R

    6 U. Berger, R. Matthes, and A. Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In P. Dybjer, J. Espírito Santo, and L. Pinto, editors,Proceedings of TYPES 2018, volume 130 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 1:1–1:22. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019.doi:10.4230/LIPIcs.TYPES.2018....

    work page doi:10.4230/lipics.types.2018.1 2018

  4. [4]

    Springer-Verlag. 11 M. Dickmann, N. Schwartz, and M. Tressl.Spectral Spaces. New Mathematical Monographs. Cambridge University Press, Cambirdge, 2019.doi:10.1017/9781316543870. 12 M. Gehrke and S. van Gool.Topological Duality for Distributive Lattices: Theory and Applications. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, C...

    work page doi:10.1017/9781316543870 2019

  5. [5]

    doi:10.1017/CBO9781139524438. 14 I. Hodkinson and M. Reynolds. Temporal Logic. In P. Blackburn, J. Van Benthem, and F. Wolter, editors,Handbook of Modal Logic, volume 3 ofStudies in Logic and Practical Reasoning, pages 655–720. Elsevier, 2007.doi:https://doi.org/10.1016/S1570-2464(07) 80014-0. 15 M. Hofmann and W. Chen. Abstract interpretation from Büchi ...

    work page doi:10.1017/cbo9781139524438 2007

  6. [6]

    Riba and A

    URL: https:// C. Riba and A. Donadille 17 www.sciencedirect.com/science/article/pii/030439759090165E, doi:https://doi.org/ 10.1016/0304-3975(90)90165-E. 19 G. Jaber and C. Riba. Temporal Refinements for Guarded Recursive Types. In N. Yoshida, editor,Proceedins of ESOP’21, volume 12648 ofLecture Notes in Computer Science, pages 548–578. Springer, 2021.doi:...

    work page doi:10.1016/0304-3975(90)90165-e 2021

  7. [7]

    21 D. O. Kidney and N. Wu. Hyperfunctions: Communicating Continuations. InProceedings of the 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026). ACM,

    work page 2026

  8. [8]

    URL:https://doi.org/10.1145/3776649,doi:10.1145/3776649. 22 E. Koskinen and T. Terauchi. Local Temporal Reasoning. InProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS’14, New York, NY, USA,

    work page doi:10.1145/3776649

  9. [9]

    Association for Computing Machinery.doi: 10.1145/2603088.2603138. 23 J. Lawson. Stably compact spaces.Mathematical Structures in Computer Science, 21(1):125– 169, 2011.doi:10.1017/S0960129510000319. 24 P. B. Levy.Call-By-Push-Value. Semantics Structures in Computation. Springer, Dordrecht, 2003.doi:https://doi.org/10.1007/978-94-007-0954-6. 25 P. B. Levy....

    work page doi:10.1145/2603088.2603138 2011

  10. [10]

    Association for Computing Machinery.doi:10.1145/3209108.3209204. 28 M. Nygaard and G. Winskel. Full Abstraction for HOPLA. In R.M. Amadio and D. Lugiez, editors,Proceedings of CONCUR 2003, volume 2761 ofLecture Notes in Computer Science, pages 378–392. Springer, 2003.doi:10.1007/978-3-540-45187-7_25. 29 P. Odifreddi.Classical Recursion Theory, volume 143 ...

    work page doi:10.1145/3209108.3209204 2003

  11. [11]

    URL: https://link.springer.com/chapter/10.1007/978-3-031-99536-1_ 11,doi:10.1007/978-3-031-99536-1_11

    Full version available on arXiv (https://arxiv.org/abs/ 2502.11917). URL: https://link.springer.com/chapter/10.1007/978-3-031-99536-1_ 11,doi:10.1007/978-3-031-99536-1_11. 32 C. Riba and S. Stern. Liveness Properties in Geometric Logic for Domain-Theretic Streams. InProceedings of JFLA’24,

    work page doi:10.1007/978-3-031-99536-1_

  12. [12]

    URL:https://inria.hal.science/hal-04407194

    Full version available on arXiv (https://arxiv.org/abs/ 2310.12763). URL:https://inria.hal.science/hal-04407194. 33 T. Sekiyama and H. Unno. Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations.Proc. ACM Program. Lang., 7(POPL), jan

    work page arXiv

  13. [13]

    Full version available on arXiv athttps://arxiv.org/abs/2207.10386. 34 C. Skalka, S. Smith, and D. Van Horn. Types and Trace Effects of Higher Order Programs.J. Funct. Program., 18(2):179–249, March 2008.doi:10.1017/S0956796807006466. 35 C. Sprenger and M. Dam. On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in theµ-Calculus. In A...

    work page doi:10.1017/s0956796807006466 2008

  14. [14]

    URL: https://www.worldscientific.com/doi/abs/10.1142/6284, arXiv:https:// www.worldscientific.com/doi/pdf/10.1142/6284,doi:10.1142/6284. 37 H. Unno, Y. Satake, and T. Terauchi. Relatively complete refinement type system for verifica- tion of higher-order non-deterministic programs.Proc. ACM Program. Lang., 2(POPL):12:1– 12:29, 2018.doi:10.1145/3158100. 38...

    work page doi:10.1142/6284 2018

  15. [15]

    Zhang.Logic of Domains

    41 G. Zhang.Logic of Domains. Progress in Theoretical Computer Science. Birkhäuser, Boston, MA, 1991.doi:https://doi.org/10.1007/978-1-4612-0445-9. C. Riba and A. Donadille 19 ψ∧(φ∨θ)⊣⊢(ψ∧φ)∨(ψ∧θ)ψ∨(φ∧θ)⊣⊢(ψ∨φ)∧(ψ∨θ) (a)Distributive laws. [△](φ∨ψ)⊣⊢[△]φ∨[△]ψ[△](φ∧ψ)⊣⊢[△]φ∧[△]ψ (b)Modalities△∈{π1,π2,in1,in2,fold}. (ψ1∨ψ2)∥→φ⊣⊢(ψ1∥→φ)∧(ψ2∥→φ) ψ∥→(φ1∧φ2)⊣⊢(ψ...

    work page doi:10.1007/978-1-4612-0445-9 1991