Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
First-Order Universality for Real Programs
verfasst von : Thomas Anberrée
Erschienen in: Mathematical Theory and Computational Practice
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
J. Raymundo Marcial–Romero and M. H. Escardó described a functional programming language with an abstract data type
Real
for the real numbers and a non-deterministic operator
. We show that this language is universal at first order, as conjectured by these authors: all computable, first-order total functions on the real numbers are definable. To be precise, we show that each computable function
$f\colon\mathbb{R}\to\mathbb{R}$
we consider is the extension of the denotation
of some program
, in a model based on powerdomains, described in previous work. Whereas this semantics is only an approximate one, in the sense that programs may have a denotation strictly below their true outputs, our result shows that, to compute a given function, it is in fact always possible to find a program with a faithful denotation. We briefly indicate how our proof extends to show that functions taken from a large class of computable, first-order
partial
functions in several arguments are definable.