First-Order Universality for Real Programs

10 years 14 days ago
First-Order Universality for Real Programs
J. Raymundo Marcial–Romero and M. H. Escard´o described onal programming language with an abstract data type Real for the real numbers and a non-deterministic operator rtest: Real → Bool. 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 : R → R we consider is the extension of the denotation Mf of some program Mf : Real → Real, 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 a...
Thomas Anberrée
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where CIE
Authors Thomas Anberrée
Comments (0)