Exact real number computations relative to hereditarily total functionals. (Q1607298): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(2 intermediate revisions by 2 users not shown) | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4222034 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3360172 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: PCF extended with real numbers / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The hereditary partial effective functionals and recursion theory in higher types / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4934283 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Computability over the partial continuous functionals / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4513589 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: LCF considered as a programming language / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Full abstraction, totality and PCF / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A type-theoretical alternative to ISWIM, CUCH, OWHY / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 12:17, 4 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Exact real number computations relative to hereditarily total functionals. |
scientific article |
Statements
Exact real number computations relative to hereditarily total functionals. (English)
0 references
31 July 2002
0 references
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\).
0 references
Real-PCF
0 references
Relative definability
0 references
Uniformly definable
0 references
Total
0 references