Ramy logiczne a teoria typów

Jaka jest różnica między strukturą logiczną a teorią typów? Oba mają typy, terminy i są oparte na rachunku lambda zależnym od typu.

Mamy Edinburg LF, który opiera się na rachunku lambda-pi, jednak wydaje mi się, że istnieje tam subtelna różnica.

Streszczenie. Ramy logiczne są metajęzykiem formalizacji systemów dedukcyjnych, w których dedukcje stają się obiektami składniowymi.

Oczywiście to, co liczy się jako metajęzyk, jest dość niejasne i pomocne jest zrozumienie historycznego rozwoju ram logicznych. Pierwszą strukturą logiczną był Automath de Bruijna (1) oparty na rachunku. Wiele pomysłów z rodziny języków Automath znalazło zastosowanie w nowoczesnych ramach logicznych. Wpływ Martina-Löfa na konstruktywne teorie typów, również oparte na λ -calculi, był znaczący.$\lambda$$\lambda$

LF w Edynburgu (2) jest bardzo wpływowym układem logicznym. Edinburgh LF jest tym, co dostajesz, gdy wzbogacisz prosty typ rachunek różniczkowy-zależny od typu. To wszystko. W celu uczynienia typu zależność precyzyjna, trzeba zastąpić operatora przestrzeń funkcja A → B na typy z typu abstrakcji, zwykle napisane Π x A . B i przedstaw rodzaj rodzajów, a także rodzaj abstrakcji. Jeśli chodzi o reguły, kluczem jest reguła eliminacji dla A → B , odpowiednio. Π x A . B :$\lambda$$A \rightarrow B$$\Pi x^A. B$$A \rightarrow B$$\Pi x^A. B$

Po lewej mamy regułę dla po prostu wpisanego rachunku, po prawej regułę, która uogólnia lewą zależność od typu. Widzimy, że wartość „wpada” do tego typu we wniosku po prawej stronie.$\lambda$

Myślę, że interaktywna asystentka dowodowa Isabelle wykorzystuje intuicyjną logikę drugiego rzędu opartą na rachunku, bez żadnych liczb lub rekurencyjnych typów danych jako ramy logicznej. Zaproponowano różne inne.$\lambda$

Jedną z zalet stosowania calculi jako logicznego zrębu jest to, że konstrukty wiążące, takie jak uniwersalne kwantyfikatory, mogą być realizowane za pomocą spoiwa λ zrębowego. Zauważ, że większość struktur logicznych jest wyraźnie słaba: ramy obsługują rozumowanie na poziomie obiektu, ale są niewystarczające, aby wykonać wiele metaoretycznego rozumowania poza faktem, że określona instrukcja na poziomie obiektu jest twierdzeniem. W rzeczywistości metalowa logika jest zwykle tak słaba, że ​​nawet udowodnienie twierdzenia o dedukcji dla logiki obiektowej typu Hilberta jest niemożliwe. Oczywiście nic nie stoi na przeszkodzie, aby używać bardziej rozbudowanych teorii typów jako logicznej struktury.$\lambda$$\lambda$

$\lambda$

1. N. de Bruijn: Język matematyczny AUTOMAT, jego użycie i niektóre z jego rozszerzeń.

2. RF Harper, F. Honsell, G. Plotkin: A Framework for Defining Logics .

3. F. Pfenning: Ramy logiczne.

4. F. Pfenning: Ramy logiczne - krótkie wprowadzenie .