Exact real number computations relative to hereditarily total functionals.
From MaRDI portal
We show that the continuous existential quantifier \(\exists_{\omega}\) is not definable in Escardó's Real-\(PCF\) from all functionals equivalent to a given total one in a uniform way. We further prove that relative to any total functional of type \((I\rightarrow I)\rightarrow I\) which gives the maximum-value for any total input, we may, given a computable, total functional \(\Phi\) of type \((R\rightarrow R)\rightarrow R\) find a Real-\(PCF\)-definable total \(\Psi\) equivalent to \(\Phi\).
Recommendations
Cites work
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Computability over the partial continuous functionals
- Full abstraction, totality and PCF
- scientific article; zbMATH DE number 4212032 (Why is no real title available?)
- scientific article; zbMATH DE number 1229489 (Why is no real title available?)
- scientific article; zbMATH DE number 1531372 (Why is no real title available?)
- scientific article; zbMATH DE number 1390018 (Why is no real title available?)
- LCF considered as a programming language
- PCF extended with real numbers
- The hereditary partial effective functionals and recursion theory in higher types
Cited in
(3)
This page was built for publication: Exact real number computations relative to hereditarily total functionals.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1607298)
