Czy semantyczna metryka Escardó dla limitów czasu PCF + jest w pełni abstrakcyjna?

W swoim artykule warsztatowym z 1999 r. „Metryczny model PCF” Martín Escardó wykazał, że można podać prostą interpretację PCF w kategorii kompletnych przestrzeni ultradźwiękowych i nie ekspansywnych map.

Pokazał, że ten model jest odpowiedni i że może modelować dodanie konstrukcji limitu czasu (tj. Operatora, który uruchomiłby swój argument dla pewnej skończonej liczby kroków i albo udzielił odpowiedzi, albo zasygnalizował błąd, jeśli nie zakończy się w ciągu termin). Następnie zasugerował, że byłoby naturalne zbadanie, czy model metryczny był w pełni abstrakcyjny w odniesieniu do limitów czasu PCF +.

1. Czy ktoś to zbadał, a jeśli tak, to jaka jest odpowiedź?
2. Czy limity czasu PCF + realizują te same funkcje co maszyny Turinga, w tym w typach wyższych?

(Na marginesie, jak wstawiasz akcenty w tekście? Usunąłem akcent zarówno z jego imienia, jak i nazwiska. EDYCJA: Nazwisko naprawione. Zostawiam to w nawiasie, aby komentarze do postu były nadal sens.)

Jeśli chodzi o twoje drugie pytanie, wydaje mi się, że pamiętam, że w przypadku typów wyższego rzędu pytanie było ściśle powiązane z tym, czy limit czasu PCF + był równoważny Efektywności Typu 2 (maszyny Turinga z nieskończonymi danymi wejściowymi i zewnętrznymi), tj. Druga częściowa algebra kombinatoryjna. John Longley przez pewien czas twierdził, że druga algebra Kleene'a była równoważna PCF + timeout + catch, ale ostatecznie nie opublikował szczegółowego wyniku.

Z drugiej strony jestem całkiem pewien, że John Longley opus magnum „O wszechobecności pewnych struktur typu całkowitego” (Struktury matematyczne w informatyce 17 (5) (2007), 841--953) sugeruje, że funkcjonale wyższego rzędu Limit czasu PCF + definiowany jest dokładnie jako dziedzicznie skuteczny.