Czy w teorii typów istnieje dobre pojęcie o braku terminacji i zatrzymaniu dowodów?

Konstruktywna teoria typów z jej podstawową interpretacją w ramach korespondencji curry-howard składa się wyłącznie z całkowitych, obliczalnych funkcji. W literaturze niektórzy mówili o stosowaniu „teorii typów obliczeniowych” w celu przedstawienia nieterminacji w programach funkcjonalnych, ale w artykułach, na które się natknąłem, nie wydaje się to być główną motywacją dla teorii (na przykład Benton wspomina o niedeterminacji, kontynuacjach i wyjątkach, bez wchodzenia w szczegółowe informacje na temat nieterminacji), więc nie znalazłem jeszcze dokumentu, który dałby solidną interpretację nieterminacji przy użyciu obliczeniowej teorii typów.

W szczególności szukam sposobu, w którym biorąc pod uwagę typ reprezentujący prawdopodobnie niekończące się obliczenia typu , , powinno istnieć pewne pojęcie dowodów, że kończy typ tak, że podane i , że konstruuje termin . $A$ $T(A)$ $x : T(A)$ $H(x)$ $x:T(A)$ $p:H(x)$ $\tilde x : A$

Motywuję to tym, że w końcu chciałbym móc bardziej formalnie powiązać pojęcia w teorii złożoności obliczeniowej z konstruktywną teorią typów. W szczególności interesuje mnie, jaką moc jako formalne teorie zyskują typy konstruktywne dzięki dostępowi do wyroczni zatrzymującej, i aby to zrobić, oczywiście muszę mieć formalne pojęcie możliwego braku wypowiedzenia i dowody zaprzestania postępuj zgodnie z nim w ramach teorii typu.

lo.logic type-theory oracles halting-problem Nathan BeDell
źródło

Czy spojrzałeś na Constable-Mendler, Rekurencyjne definicje w teorii typów ? Dają sposób definiowania dla każdego stałoprzecinkowych rekurencyjnej definicji częściowego funkcji

jest domeną orzeczenie

tak, że dla

reprezentuje typ dowodów, które

zatrzymuje się na

. Wierzę, że jest to zaimplementowane w Nuprl.

f

$f$

A

$A$

B

$B$

d o m (f)

$\mathrm{dom}(f)$

x \in A

$x\in A$

d o m (f) (x)

$\mathrm{dom}(f)(x)$

f

$f$

x

$x$

Ulrik Buchholtz

Szukasz monady opóźniającej ?

Andrej Bauer,

@UlrikBuchholtz Myślę, że to dość blisko tego, czego szukam, chociaż mam pewne trudności z analizowaniem notacji Nuprl, która jest używana w pracy - z którą nie jestem podobny. Jeśli dobrze rozumiem, zasadniczo definiują one częściową funkcję rekurencyjną od

(lub przynajmniej identyfikują je za pomocą) jako całkowitą funkcję rekurencyjną z $ \ {x: A | dom (f) (g) \} do B. (Patrz uwaga na dole strony 27)

A

$A$

B

$B$

Nathan BeDell 12.04.16

Odpowiedzi:

Ponieważ jednym z głównych zastosowań teorii typów w formalizacjach było studiowanie języków programowania i ogólnie obliczeń, wiele myśli poświęcono sposobom przedstawiania programów, które prawdopodobnie nie kończą się.

Nie zrobię tutaj pełnej ankiety, ale postaram się wskazać główne kierunki różnych kierunków.

Podejście „relacyjne”: możesz zdefiniować swoje hipotetyczne programy tak, jak mówią relacje, które zawiera iff jest zdefiniowane dla i . Zazwyczaj jest to, co dzieje się z Kleene T-orzecznika . Działa to równie dobrze w formalizacjach teorii typów, jak w logice klasycznej (choć oczywiście nie można udowodnić ). $F\ x\ y$ $f$ $x$ $f(x)=y$ $\forall x (\exists y, F\ x\ y)\vee (\neg\exists y, F\ x\ y)$

Bardziej wyrafinowanym sposobem na to jest metoda „Bove-Capretta” (patrz Modelowanie rekurencji w teorii typów , która dla każdej funkcji rekurencyjnej definiuje „dostępny predykat”, który koduje fakt, że dane obliczenie jest skończone. Definicja funkcji przyjmuje dodatkowy argument, który jest dowodem na to, że dane dane wejściowe są dostępne. Aby zdefiniować funkcję bez tego dodatkowego predykatu, musisz udowodnić, że każda możliwa kombinacja danych wejściowych jest dostępna.
$A$
```
codata Delay A =
| Now : A -> Delay A
| Later (Delay A)
```
To koduje prawdopodobnie nieskończony strumień Latertokenów („tyknięć” obliczeń), który może kończyć się wynikiem Now a. Brak wypowiedzenia jest równoznaczny z niepodobnością do programu

loop = Późniejsza pętla i zakończenie mogą być zdefiniowane przez predykat indukcyjny w stosunku do Delay A:
```
data Terminates : Data A -> Prop =
| Term_now : forall x, Terminates (Now x)
| Term_later : forall d, Terminates d -> Terminates (Later d)
```
Myślę, że agda-istas mają wiele do powiedzenia na temat tego, co nazywają monadą stronniczości (patrz np. Danielsson ).
Podejście „częściowej teorii typów” : jest to nieco bardziej eksperymentalne (teoria jest wciąż opracowywana), ale istnieją pewne teorie typów, które są rozwijane, aby poradzić sobie z faktem, że istnieją zasadniczo dwa rodzaje funkcji, które chcemy napisz w teorii typów: warunki próbne i programy. Okazuje się, że trudno jest uzyskać rozsądną teorię tych rzeczy (i zachować spójność teorii), ale poważną próbę podjęli tutaj Casinghino i in. Oraz podobny wysiłek Kimmela i in .

Jestem pewien, że istnieją inne podejścia, o których nie wiem i byłbym szczęśliwy, gdyby ktoś chciał wypełnić tę listę.

$\Pi^0_1$

Istnieją inne, dość owocne interakcje między teorią typów a teorią złożoności, zwykle pod parasolem ukrytej złożoności obliczeniowej .

cody
źródło

Ciekawe, dzięki za informację! Uważam, że podejście z częściową teorią typów jest prawdopodobnie najbliższe duchowi tego, czego szukam - a przynajmniej artykuł Kimmela wydaje się na pewnym poziomie konkretnie tego, czego szukam (zobacz zasady pisania dla „tcast” ).

Nathan BeDell,