Constructive Domains with Classical Witnesses

TL;DR

This paper develops a constructive framework for continuous domains that allows program extraction without witnesses of correctness, using classical logic to formulate correctness assertions and constructing function spaces and real numbers.

Contribution

It introduces a novel constructive theory of continuous domains with classical correctness assertions, including a new construction of function spaces and a representation theorem for real numbers.

Findings

Constructed a constructive theory of continuous domains from predomain bases.

Presented a new construction of function spaces within this framework.

Proved a representation theorem characterizing real numbers as total elements of the completion.

Abstract

We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain base and construct a completion. We then investigate continuity with respect to the Scott topology, and present a construction of the function space. We then discuss our main motivating example in detail, and instantiate our theory to real numbers that we conceptualise as the total elements of the completion of the predomain of rational intervals, and prove a representation theorem that precisely delineates the class of representable continuous functions.