Jaka jest zależność i różnica między rachunkiem konstrukcji indukcyjnych a teorią typu intuicyjnego?

Jak stwierdzono w tytule, zastanawiam się nad jakąkolwiek relacją i różnicą między CIC a ITT. Czy ktoś mógłby mi wyjaśnić lub wskazać mi literaturę porównującą te dwa systemy? Dzięki.

Odpowiedziałem już nieco, ale jeśli tak, postaram się przedstawić bardziej szczegółowy przegląd horyzontów teoretycznych typu.

Jestem trochę rozmyślany nad historycznymi szczegółami, więc bardziej świadomi czytelnicy będą musieli mi wybaczyć (i poprawić mnie!). Podstawowa historia polega na tym, że Curry odkrył podstawową zgodność między kombinatorami prostego typu (lub ) a logiką zdań, która została poszerzona przez Howarda o logikę pierwszego rzędu, oraz IIRC niezależnie odkryte przez de Bruijna w dochodzeniach wokół ogromnie wpływowy system Automath .$\lambda$

System Automath był udoskonaleniem prostej teorii typu Kościoła, która sama w sobie była dramatycznym uproszczeniem teorii typów Russela i Whitehead z wszechświatami i aksjomatem redukowalności . Był to stosunkowo dobrze znany logiczny teren w latach 60.

Określa odpowiednią regułę eliminacji. Następnie podał bardzo potężny system fundamentalny oparty na takich osądach, pozwalając mu na stworzenie systemu fundamentalnego podobnego do Automath przy użyciu bardzo niewielu konstrukcji składniowych. Girard stwierdził, że ten system jest sprzeczny, co skłoniło Martina-Löfa do przyjęcia predykatywnych wszechświatów w stylu Russel , poważnie ograniczając ekspresję teorii (poprzez skuteczne usunięcie aksjomatu redukowalności) i czyniąc ją nieco bardziej złożoną (ale miała tę zaletę, że dzięki czemu jest spójny).

Eleganckie konstrukcje pozwalające na zdefiniowanie symboli logicznych już nie działały, co skłoniło ML do wprowadzenia ich w innej formie jako indukcyjnie zdefiniowanych rodzin . Jest to bardzo skuteczny pomysł, ponieważ pozwala zdefiniować wszystko, od osądowej równości i operatorów logicznych po liczby naturalne i funkcjonalne typy danych, jakie pojawiają się w informatyce. Zauważ, że każda dodana przez nas rodzina przypomina dodawanie pewnej liczby aksjomatów, które należy uzasadnić jako spójne w każdym przypadku. Ten system (typy zależne + wszechświaty + rodziny indukcyjne) jest zwykle nazywany ITT .

Wystąpiła jednak pewna frustracja, ponieważ potężny, ale prosty system fundamentalny był niespójny, a wynikowy system był bardziej złożony i nieco słaby (w tym sensie, że trudno było w nim rozwinąć wiele nowoczesnych ram matematycznych). Wchodzi Thierry Coquand, który wraz ze swoim przełożonym Gerardem Huetem przedstawił Rachunek konstrukcji (CoC) , który w większości rozwiązał te problemy: ujednolicone podejście do dowodów i typów danych, potężny (impredykatywny) system fundamentalny oraz możliwość definiowania „konstrukcji” „odmiany logicznej lub matematycznej. To ostatecznie przekształciło się w faktyczną implementację systemu zaprojektowanego jako nowoczesna alternatywa dla Automath, którego kulminacją jest znany i kochany system Coq .

Zdecydowanie sugeruję ten fundamentalny artykuł na temat CoC, ponieważ Thierry zna absurdalną ilość na temat historycznego rozwoju teorii typów i prawdopodobnie wyjaśnia to znacznie lepiej niż ja. Możesz także zajrzeć do jego artykułu na temat teorii typów, chociaż nie wyjaśnij szczegółowo korespondencję CH.