Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Complete Finitary Refinement Type System for Scott-Open Properties

Colin Riba, Adam Donadille

TL;DR

The paper develops a finitary refinement type system that is sound and complete for Scott-open properties of functions over infinite data (streams and trees) by grounding refinements in a fixpoint-like logic over Scott domains. It relies on Domain Theory in Logical Form and the spectral-space structure of Scott domains to separate Open (positive) and Compact-Saturated (negative) properties via polarity. A realizability implication with polarity control enables expressive input-output specifications, and the main Positive Completeness Theorem shows that all sound positive specifications are derivable. The framework yields a semantically grounded, potentially semi-decidable approach to verifying infinite-data properties, with future directions toward liveness, CBPV, and effects.

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 properties, while negative formulae allow for greatest fixpoints and define compact-saturated properties. A realizability implication with the usual (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.

A Complete Finitary Refinement Type System for Scott-Open Properties

TL;DR

The paper develops a finitary refinement type system that is sound and complete for Scott-open properties of functions over infinite data (streams and trees) by grounding refinements in a fixpoint-like logic over Scott domains. It relies on Domain Theory in Logical Form and the spectral-space structure of Scott domains to separate Open (positive) and Compact-Saturated (negative) properties via polarity. A realizability implication with polarity control enables expressive input-output specifications, and the main Positive Completeness Theorem shows that all sound positive specifications are derivable. The framework yields a semantically grounded, potentially semi-decidable approach to verifying infinite-data properties, with future directions toward liveness, CBPV, and effects.

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 properties, while negative formulae allow for greatest fixpoints and define compact-saturated properties. A realizability implication with the usual (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.
Paper Structure (13 sections, 18 theorems, 18 equations, 10 figures, 1 table)

This paper contains 13 sections, 18 theorems, 18 equations, 10 figures, 1 table.

Table of Contents

  1. Introduction
  2. The Pure System
  3. The Logic
  4. Formulae
  5. Deduction
  6. The Refinement Type System
  7. Semantics
  8. Semantics of the Pure System
  9. Scott Domains as Spectral Spaces
  10. Semantics of Formulae
  11. Semantics of the Refinement Type System
  12. Conclusion
  13. Proofs of §\ref{['sec:log']} (\ref{['sec:log']})

Key Result

Lemma 7

For each $\varphi \in \mathcal{L}^\omega(\tau)$, there is some $\psi \in \mathcal{L}^{\lor\land}(\tau)$ such that $\varphi \mathrel{\dashv\vdash} \psi$.

Figures (10)

  • Figure 1: Typing rules for pure types, where $i \in \{1,2\}$.
  • Figure 2: Formation rules for $\mathcal{L}^s$ (the predicates $\mathrel{\mathsf{Pos}}$ and $\mathrel{\mathsf{Neg}}$ are defined in Figure \ref{['fig:posneg']}).
  • Figure 3: The predicates $\mathrel{\mathsf{Pos}}$ and $\mathrel{\mathsf{Neg}}$, where $\mathord{\triangle} \in \{\pi_1,\pi_2, \mathop{\mathsf{in}}_1, \mathop{\mathsf{in}}_2, \mathop{\mathsf{fold}}\}$, and where $\star$ is $\land$ or $\lor$.
  • Figure 4: Deduction rules.
  • Figure 5: The consistency predicate $\mathcal{C}$.
  • ...and 5 more figures

Theorems & Definitions (35)

  • Example 1
  • Example 2
  • Definition 3: Formulae
  • Example 4
  • Example 5
  • Remark 6: Non-Examples
  • Definition 7: Deduction
  • Lemma 7
  • Remark 8
  • Lemma 8
  • ...and 25 more