Czy kombinator Y jest sprzeczny z korespondencją Curry-Howarda?

Kombinator Y ma typ . Według korespondencji Curry-Howarda, ponieważ typ ( a → a ) → a jest zamieszkały, musi odpowiadać prawdziwemu twierdzeniu. Jednak a → a jest zawsze prawdziwe, więc wydaje się, że typ kombinatora Y odpowiada twierdzeniu a , co nie zawsze jest prawdziwe. Jak to może być?$(a \rightarrow a) \rightarrow a$$(a \rightarrow a) \rightarrow a$$a \rightarrow a$$a$

Oryginalna korespondencja Curry-Howarda jest izomorfizmem między intuicyjną logiką zdań a prostym typem rachunku lambda.

Istnieją oczywiście inne izomorfizmy podobne do Curry-Howarda; Phil Wadler słynie zwrócił uwagę, że dwulufowa nazwa „Curry-Howard” przewiduje inne dwulufowe nazwy, takie jak „Hindley-Milner” i „Girard-Reynolds”. Byłoby zabawnie, gdyby „Martin-Löf” był jednym z nich, ale tak nie jest. Ale dygresję.

Kombinator Y nie zaprzecza temu, z jednego kluczowego powodu: nie można go wyrazić w prostym typie rachunku lambda.

W rzeczywistości o to właśnie chodziło. Haskell Curry odkrył kombinator punktów stałych w niepisanym rachunku lambda i wykorzystał go, aby udowodnić, że niepoparty rachunek lambda nie jest systemem dedukcji dźwięku.

Co ciekawe, typ Y odpowiada logicznemu paradoksowi, który nie jest tak dobrze znany, jak powinien, zwany paradoksem Curry'ego. Rozważ to zdanie:

Jeśli to zdanie jest prawdziwe, oznacza to, że Święty Mikołaj istnieje.

Załóżmy, że zdanie było prawdziwe. Wtedy oczywiście Święty Mikołaj by istniał. Ale dokładnie to mówi zdanie, więc zdanie jest prawdziwe. Dlatego Święty Mikołaj istnieje. CO BYŁO DO OKAZANIA

Curry-Howard odnosi systemy typu do systemów logicznej dedukcji. Między innymi odwzorowuje:

• programy do proofów
• ocena programu do przekształceń na dowodach
• typy zamieszkane według prawdziwych zdań
• wpisz systemy do logicznych systemów dedukcyjnych

$a \to b$$a$$b$$Y (\lambda x. x) \to Y (\lambda x.M)$

Korespondencja Curry-Howarda jest po prostu: korespondencja. Sam w sobie nie oznacza, że ​​pewne twierdzenia są prawdziwe. Mówi, że typowość / sprawdzalność przenosi się z jednej strony na drugą.

Korespondencja Curry-Howarda jest przydatna jako narzędzie sprawdzające w wielu systemach typów: po prostu typowany rachunek lambda, system F, rachunek konstrukcji itp. Wszystkie te systemy typów mają właściwość, że odpowiednia logika jest spójna (jeśli zwykła matematyka jest spójna ). Mają także tę właściwość, że nie pozwalają na dowolną rekurencję. Korespondencja Curry-Howarda pokazuje, że te dwie właściwości są powiązane.

Curry-Howard nadal stosuje się do niekończących się kalkulatorów maszynowych i niespójnych systemów dedukcyjnych. Po prostu nie jest to szczególnie przydatne.