<p>Regarding your second question, I seem to remember that for higher-order types the question was linked closely to whether PCF+timeout was equivalent to Type Two Effectivity (Turing machines with infinite inputs and outpus), i.e., Kleene's second partial combinatory algebra. John Longley claimed for a while that Kleene's second algebra was equivalent to PCF+timeout+catch, but in the end he never published a detailed result.</p>

<p>On the other hand, I am pretty sure that John Longley opus magnum <a href="http://homepages.inf.ed.ac.uk/jrl/Research/ubiquity-full.pdf">"On the ubiquity of certain total type structures"</a> (Mathematical Structures in Computer Science 17(5) (2007), 841--953) implies that the higher-order functionals definable in PCF+timeout are precisely the hereditarily effective ones.</p>

CC BY-SA 2.5
2011-03-16T14:02:15.113Z
Still no word on full abstractness, but you did answer question 2, so this is accepted.
Neel Krishnaswami
CC BY-SA 2.5
2011-03-17T05:13:55.150Z
Martin says nobody thought too hard about full abstraction. He points out that full abstraction follows if you can define a dense sequence for every type, i.e., given a type `t`, define a sequence `int -> t` in PCF+timeout which is dense with respect to the ultrametric on `t`.
Andrej Bauer
CC BY-SA 2.5
2011-03-05T19:20:37.340Z
2011-03-05T19:20:37.340Z
Andrej Bauer
<p>In his 1999 workshop paper <a href="http://www.cs.bham.ac.uk/~mhe/papers/metricpcf.pdf" rel="nofollow">"A Metric Model of PCF"</a>, Mart&iacute;n Escard&oacute;  showed that it is possible to give a simple interpretation of PCF in the category of complete ultrametric spaces and nonexpansive maps. </p>

<p>He showed this model was adequate, and that it could model the addition of a timeout construct (i.e., an operator which would run its argument for some finite number of steps, and either yield an answer or signal an error if it failed to terminate within the time limit). He then suggested that it would be natural to investigate whether the metric model was fully abstract with respect to PCF+timeouts. </p>

<ol>
<li>Has anyone investigated this, and if so, what's the answer?</li>
<li>Does PCF+timeouts realize the same functions as Turing machines, including at higher type?</li>
</ol>

<p>(As an aside, how do you put accents into the text? I've dropped an accent from both  his first and last names. EDIT: Name fixed. I'm leaving this parenthetical in so that the comments to the post continue to make sense.) </p>

CC BY-SA 2.5
2011-03-05T15:23:15.570Z
You can use &iacute; and &oacute; to represent the characters with accents.  (Clearly this doesn't work in comments though)
Marc Hamann
CC BY-SA 2.5
2011-03-05T19:12:54.427Z
On ädvaǹçéd computerš sućh as a Mac typing Martín Hötzel Escardó is easy as Π, π and ϖ.
Andrej Bauer
CC BY-SA 2.5
2011-03-05T20:10:40.820Z
Υβυντυ ισ αλσω åđƔąņćĕð!
Radu GRIGore
CC BY-SA 2.5
2011-03-06T18:06:28.643Z
मैं बहुत है कि सुनने के लिए खुश हूँ.
Andrej Bauer
CC BY-SA 2.5
2011-03-07T13:47:55.843Z
What's going on here? Do we have a contest for finding the most complicated language of human beings? I want to join! :D
Hsien-Chih Chang 張顯之
CC BY-SA 2.5
2011-03-07T16:42:34.617Z
@Andrej, I don't think what you said actually makes sense :), but the Hindi is pretty :)
Suresh Venkat
CC BY-SA 2.5
2011-03-09T05:25:43.250Z
Google translate surely thinks it makes sense :-)
Andrej Bauer
<pl.programming-languages><denotational-semantics><metric-spaces>
Is Escardó's metric semantic for PCF+timeouts fully abstract ?
Neel Krishnaswami
# Is Escardó's metric semantic for PCF+timeouts fully abstract ?

(Asked by: username_0 on 2011-03-05)

In his 1999 workshop paper ["A Metric Model of PCF"](http://www.cs.bham.ac.uk/~mhe/papers/metricpcf.pdf), Martín Escardó showed that it is possible to give a simple interpretation of PCF in the category of complete ultrametric spaces and nonexpansive maps.

He showed this model was adequate, and that it could model the addition of a timeout construct (i.e., an operator which would run its argument for some finite number of steps, and either yield an answer or signal an error if it failed to terminate within the time limit). He then suggested that it would be natural to investigate whether the metric model was fully abstract with respect to PCF+timeouts.

1. Has anyone investigated this, and if so, what's the answer?
2. Does PCF+timeouts realize the same functions as Turing machines, including at higher type?

(As an aside, how do you put accents into the text? I've dropped an accent from both his first and last names. EDIT: Name fixed. I'm leaving this parenthetical in so that the comments to the post continue to make sense.)

**Tags:** pl.programming-languages, denotational-semantics, metric-spaces

> **Comments:**
> **username_1**: You can use &iacute; and &oacute; to represent the characters with accents.  (Clearly this doesn't work in comments though)  
> **username_2**: On ädvaǹçéd computerš sućh as a Mac typing Martín Hötzel Escardó is easy as Π, π and ϖ.  
> **username_3**: Υβυντυ ισ αλσω åđƔąņćĕð!  
> **username_2**: मैं बहुत है कि सुनने के लिए खुश हूँ.  
> **username_4**: What's going on here? Do we have a contest for finding the most complicated language of human beings? I want to join! :D  
> **username_5**: @Andrej, I don't think what you said actually makes sense :), but the Hindi is pretty :)  
> **username_2**: Google translate surely thinks it makes sense :-)  

---

## 1 answers

### Answer by username_2 on 2011-03-05. Score: 11 | Accepted answer

Regarding your second question, I seem to remember that for higher-order types the question was linked closely to whether PCF+timeout was equivalent to Type Two Effectivity (Turing machines with infinite inputs and outpus), i.e., Kleene's second partial combinatory algebra. John Longley claimed for a while that Kleene's second algebra was equivalent to PCF+timeout+catch, but in the end he never published a detailed result.

On the other hand, I am pretty sure that John Longley opus magnum ["On the ubiquity of certain total type structures"](http://homepages.inf.ed.ac.uk/jrl/Research/ubiquity-full.pdf) (Mathematical Structures in Computer Science 17(5) (2007), 841--953) implies that the higher-order functionals definable in PCF+timeout are precisely the hereditarily effective ones.

> **Comments:**
> **username_0**: Still no word on full abstractness, but you did answer question 2, so this is accepted.  
> **username_2**: Martin says nobody thought too hard about full abstraction. He points out that full abstraction follows if you can define a dense sequence for every type, i.e., given a type `t`, define a sequence `int -> t` in PCF+timeout which is dense with respect to the ultrametric on `t`.  

---

