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.

lo.logic type-theory

— Konstantin Solomatov
źródło

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 na typy z typu abstrakcji, zwykle napisane i przedstaw rodzaj rodzajów, a także rodzaj abstrakcji. Jeśli chodzi o reguły, kluczem jest reguła eliminacji dla , odpowiednio. : $\lambda$ $A \rightarrow B$ $\Pi x^A. B$ $A \rightarrow B$ $\Pi x^A. B$

\frac{Γ ⊢ M : A \to B Γ ⊢ N : A}{Γ ⊢ M N : B} \frac{Γ ⊢ M : Π x^{A} . B Γ ⊢ N : A}{Γ ⊢ M N : B {N / x}}

$\newcommand{\TYPES}[3]{#1 \vdash #2 : #3} \newcommand{\SUBST}[2]{\{#1/#2\}} \frac{ \TYPES{\Gamma}{\color{red}{M}}{A \rightarrow B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{\color{red}{MN}}{B} } \qquad \frac{ \TYPES{\Gamma}{{\color{red}M}}{\Pi x^A. B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{{\color{red}{MN}}}{B\SUBST{{\color{red}N}}{x}} }$

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$

N. de Bruijn: Język matematyczny AUTOMAT, jego użycie i niektóre z jego rozszerzeń.
RF Harper, F. Honsell, G. Plotkin: A Framework for Defining Logics .
F. Pfenning: Ramy logiczne.
F. Pfenning: Ramy logiczne - krótkie wprowadzenie .

— Martin Berger
źródło

Czy znasz jakieś książki wprowadzające na temat asystentów dowodowych (ramy logiczne) odpowiednie dla kogoś, kto już zna podstawy prostych rachunków lambda i logiki pierwszego rzędu?

— Trismegistos,

@Trismegistos Obawiam się, że nie. Proponuję nauczyć się konkretnego asystenta. Agda jest najłatwiejsza do zdobycia, ponieważ jest to w zasadzie Haskell, ale z typami zależnymi. Z mojego doświadczenia wynika, że ramy logiczne nie są tak ważne, jak inne wymiary asystentów ds. Dowodu. Na przykład Isabelle to ogólna przysłowia, które można tworzyć za pomocą różnych logik, więc naprawdę ujawnia ramy logiczne. Ale Isabelle / HOL jest jedyną instancją stosowaną w praktyce. Wynika to z tego, że wszystkie taktyki dowodowe, wszelkie wsparcie dla prover zostały napisane dla logiki obiektowej HOL. I od tego zależy użyteczność provera.

— Martin Berger,