Skip to main content
fixed Escardó's name
Source Link
Neel Krishnaswami
  • 32.9k
  • 1
  • 104
  • 165

Is Escardo'sEscardó's metric semantic for PCF+timeouts fully abstract ?

In his 1999 workshop paper "A Metric Model of PCF", Martin Escardo showedMartí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.)

Is Escardo's metric semantic for PCF+timeouts fully abstract ?

In his 1999 workshop paper "A Metric Model of PCF", Martin Escardo 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.)

Is Escardó's metric semantic for PCF+timeouts fully abstract ?

In his 1999 workshop paper "A Metric Model of PCF", 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.)

Tweeted twitter.com/#!/StackCSTheory/status/44130892901384192
Source Link
Neel Krishnaswami
  • 32.9k
  • 1
  • 104
  • 165

Is Escardo's metric semantic for PCF+timeouts fully abstract ?

In his 1999 workshop paper "A Metric Model of PCF", Martin Escardo 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.)