Definability of Computable Functionals over the Reals without Equality

M. V. Korovina & O. V. Kudinov

Partially supported by grants for young scientists SB RAS and grants RFBR N 0001-00810, 99-01-00485

Based on an effective theory of continuous domains notions of computability for operators and realvalued functionals defined on the class of continuous functions are introduced. Definability of computable operators and functionals are proposed. We extend ivestigation of computability properties proposed in [3, 4] to the case of the reals without equality. Let < R, 0, 1, +, ·, <> be the standard model of the reals, denoted also by R. For the definitions of continuous domains for the reals I (the interval domains) and notions of computability we refer to the paper [2, 5].

We denote the dcpo {[u, v]} where u : [a, b] → R is lower semucontinuous function, v : [a, b] → R is upper semicontinuous function with the natural order as I_{f}.

We use the definitions of the set of hereditarily finite sets HF(R) over a model R, and the definitions of Σ-definability proposed in [1]. THEOREM An operator F : C[a, b] → C[a, b] is computable if and only if there exists an operator

F^{∗} : I_{f} → I_{f} with the following properties:

1. F^{∗}({f}) = {F (f)}

2. F^{∗}([u, v]) = [h_{1}, h_{2}] iff there exist lower-closed Σ-formula ψ_{1} and upper-closed Σ-formula ψ_{2} such

that

h_{1}|_{[x_{1},x_{2}]} > z iff HF(R) ⊧ ψ_{1}(U_{1}, U_{2}, x_{1}, x_{2}, z)
h_{2}|_{[x_{1},x_{2}]} < z iff HF(R) ⊧ ψ_{2}(U_{1}, U_{2}, x_{1}, x_{2}, z)

where U_{1}(r_{1}, r_{2}, c) ⇌ u|_{[r_{1},r_{2}]} > c and U_{2}(r_{1}, r_{2}, c) ⇌ u|_{[r_{1},r_{2}]} < c

COROLLARY A functional F : C[a, b]×[a, b] → R is computable if and only if there exists an operator F^{∗} : I_{f} → I_{f} with the following properties:

1. F (f, x) = g(x) where F^{∗}({f}) = {g)}

2. F^{∗}([u, v]) = [h_{1}, h_{2}] iff there exist lower-closed Σ-formula ψ_{1} and upper-closed Σ-formula ψ_{2} such

that

h_{1}|_{[x_{1},x_{2}]} > z iff HF(R) ⊧ ψ_{1}(U_{1}, U_{2}, x_{1}, x_{2}, z)
h_{2}|_{[x_{1},x_{2}]} < z iff HF(R) ⊧ ψ_{2}(U_{1}, U_{2}, x_{1}, x_{2}, z)

where U_{1}(r_{1}, r_{2}, c) ⇌ u|_{[r_{1},r_{2}]} > c and U_{2}(r_{1}, r_{2}, c) ⇌ u|_{[r_{1},r_{2}]} < c

1. J. Barwise, Admissible sets and structures, Berline, Springer–Verlag, 1975.

2. A. Edalat, P. Sünderhauf, A domain-theoretic approach to computability on the real line, Theoretical Computer Science, 210, 1998, pages 73–98.

3. M. Korovina, O. Kudinov, Characteristic Properties of Majorant-Computability over the Reals, Proc. of CSL’98, LNCS, 1584, 1999, pages 188–204.

4. M. Korovina, O. Kudinov, A Logical approach to Specifications of Hybrid Systems, Proc. of PSI’99, 1725, 2000, pages 10–16.

5. D. Scott, Outline of a mathematical theory of computation, In 4th Annual Princeton Conference on Information Sciences and Systems, 1970, pages 169–176.

Addresses M. V. Korovina: Institute of Informatics Systems, Koptyg pr., 4, Novosibirsk, Russia

E-mail: rita@ssc.nsu.ru

O. V. Kudinov: Institute of Mathematics, Koptyg pr., 4, Novosibirsk, Russia

E-mail: kud@math.nsc.ru