Constructive Domains with Classical Witnesses
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 ba...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5833/pdf |
| _version_ | 1797268599191109632 |
|---|---|
| author | Dirk Pattinson Mina Mohammadian |
| author_facet | Dirk Pattinson Mina Mohammadian |
| author_sort | Dirk Pattinson |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:35:02Z |
| format | Article |
| id | doaj.art-ef8367dd6a3d4cb7bcb1b5049a0d47b4 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:02Z |
| publishDate | 2021-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-ef8367dd6a3d4cb7bcb1b5049a0d47b42024-03-08T10:33:16ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-03-01Volume 17, Issue 110.23638/LMCS-17(1:19)20215833Constructive Domains with Classical WitnessesDirk PattinsonMina MohammadianWe 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.https://lmcs.episciences.org/5833/pdfcomputer science - logic in computer science |
| spellingShingle | Dirk Pattinson Mina Mohammadian Constructive Domains with Classical Witnesses Logical Methods in Computer Science computer science - logic in computer science |
| title | Constructive Domains with Classical Witnesses |
| title_full | Constructive Domains with Classical Witnesses |
| title_fullStr | Constructive Domains with Classical Witnesses |
| title_full_unstemmed | Constructive Domains with Classical Witnesses |
| title_short | Constructive Domains with Classical Witnesses |
| title_sort | constructive domains with classical witnesses |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/5833/pdf |
| work_keys_str_mv | AT dirkpattinson constructivedomainswithclassicalwitnesses AT minamohammadian constructivedomainswithclassicalwitnesses |