Exact real number computations relative to hereditarily total functionals.
type: Item
instance of: scholarly article
title: Exact real number computations relative to hereditarily total functionals.
zbMATH Open document ID: 1042.68049
DOI: 10.1016/S0304-3975(01)00100-1
author: Dag Normann
published in: Theoretical Computer Science
publication date: 2002-07-31T00:00:00Z
review text: 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\).
Mathematics Subject Classification ID: 68Q05
zbMATH DE Number: 1774171
zbMATH Keywords: Real-PCF
zbMATH Keywords: Relative definability
zbMATH Keywords: Uniformly definable
zbMATH Keywords: Total
MaRDI profile type: Publication
cites work: Q4222034
cites work: Q3360172
cites work: PCF extended with real numbers
cites work: The hereditary partial effective functionals and recursion theory in higher types
cites work: Q4934283
cites work: Computability over the partial continuous functionals
cites work: Q4513589
cites work: LCF considered as a programming language
cites work: Full abstraction, totality and PCF
cites work: A type-theoretical alternative to ISWIM, CUCH, OWHY
full work available at URL: s0304-3975(01)00100-1
OpenAlex ID: W2082376293
description: scientific article; zbMATH DE number 1774171