Rachunek konstrukcji - Calculus of constructions

W logice matematycznej i informatyki The rachunek konstrukcji ( CoC ) jest teoria typ stworzony przez Thierry Coquand . Może służyć zarówno jako typowany język programowania, jak i jako konstruktywna podstawa matematyki . Z tego drugiego powodu CoC i jego warianty były podstawą dla Coq i innych asystentów dowodu .

Niektóre z jego wariantów obejmują rachunek konstrukcji indukcyjnych (dodający typy indukcyjne ), rachunek konstrukcji (ko)indukcyjnych (dodający koindukcję ) oraz rachunek predykatywny konstrukcji indukcyjnych (który usuwa pewną niepredykatywność ).

Rachunek konstrukcji, z dodatkowym aksjomatem odpowiadającym aksjomatowi wyboru , może być zakodowany w teorii mnogości Zermelo-Fraenkla z wyborem (ZFC) i odwrotnie. Dlatego oba są równospójne .

Cechy ogólne

CoC to typowy rachunek lambda wyższego rzędu , początkowo opracowany przez Thierry'ego Coquand'a . Jest dobrze znany z bycia na szczycie Barendregt „s lambda sześcianu . W CoC można definiować funkcje od terminów do terminów, a także terminy na typy, typy na typy i typy na terminy.

CoC jest silnie normalizujący , chociaż niemożliwe jest udowodnienie tej właściwości w CoC, ponieważ implikuje spójność, której nie można udowodnić z samego systemu , zgodnie z twierdzeniem Gödla .

Stosowanie

CoC został opracowany wraz z asystentem dowodu Coq . Po dodaniu funkcji (lub usunięciu ewentualnych zobowiązań) do teorii, stały się one dostępne w Coq.

Warianty CoC są używane w innych asystentach dowodowych, takich jak Matita .

Podstawy rachunku konstrukcji

Rachunek konstrukcji można uznać za rozszerzenie izomorfizmu Curry-Howarda . Izomorfizm Curry'ego-Howarda kojarzy termin w po prostu typowanym rachunku lambda z każdym dowodem dedukcji naturalnej w intuicjonistycznej logice zdań . Rachunek konstrukcji rozszerza ten izomorfizm na dowody w pełnym intuicjonistycznym rachunku predykatów, który obejmuje dowody zdań kwantyfikowalnych (które będziemy również nazywać „zdaniami”).

Warunki

Termin w rachunku konstrukcji jest wykonana przy użyciu zasad następujących:

• ${\ Displaystyle \ mathbf {T}}$to termin (zwany także typem );
• ${\ Displaystyle \ mathbf {P} }$to termin (zwany także prop , rodzaj wszystkich zdań);
• Zmienne ( ) to terminy;${\displaystyle x,y,\ldots}$
• Jeśli i są terminami, to tak jest ;${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle (AB)}$
• Jeśli i są terminami i jest zmienną, to terminami są również: ${\ Displaystyle A}$${\ Displaystyle B}$${\displaystyle x}$
  • ${\ Displaystyle (\ lambda x: AB)}$,
  • ${\displaystyle (\forall x:AB)}$.

Innymi słowy, składnia terminu w BNF to:

${\ Displaystyle e:: = \ mathbf {T} \ mid \ mathbf {P} \ mid x \ mid e \ e \ mid \ lambda x {\ mathbin {:}} ee \ mid \ forall x {\ mathbin { :}}ee}$

Rachunek konstrukcji ma pięć rodzajów obiektów:

1. dowody , które są terminami , których typami są zdania ;
2. propozycje , które są również znane jako małe typy ;
3. predykaty , które są funkcjami zwracającymi zdania;
4. duże typy , które są typami predykatów ( jest przykładem dużego typu);${\ Displaystyle \ mathbf {P} }$
5. ${\ Displaystyle \ mathbf {T}}$ sam w sobie, który jest typem dużych typów.

Wyroki

Rachunek konstrukcji umożliwia dowodzenie sądów typowania :

${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}$

Co można odczytać jako implikację

Jeżeli zmienne mają typy , to termin ma typ .${\displaystyle x_{1},x_{2},\ldots}$${\displaystyle A_{1},A_{2},\ldots}$${\displaystyle t}$${\ Displaystyle B}$

Prawidłowe sądy dla rachunku konstrukcji można wyprowadzić ze zbioru reguł wnioskowania. W dalszej części używamy do oznaczania sekwencji przypisań typu ; rozumieć terminy; i oznacza albo lub . Będziemy pisać, aby oznaczać wynik podstawienia terminu za zmienną wolną w wyrazie . ${\ Displaystyle \ Gamma}$${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots}$${\displaystyle A,B,C,D}$${\ Displaystyle K, L}$${\ Displaystyle \ mathbf {P} }$${\ Displaystyle \ mathbf {T}}$${\displaystyle B[x:=N]}$${\ Displaystyle N}$${\displaystyle x}$${\ Displaystyle B}$

Reguła wnioskowania jest zapisana w postaci

${\ Displaystyle {\ Frac {\ Gamma \ vdash A: B} {\ Gamma '\ vdash C: D}}}$

co znaczy

Jeśli jest słusznym osądem, to tak jest${\ Displaystyle \ Gamma \ vdash A: B}$${\ Displaystyle \ Gamma '\ vdash C: D}$

Reguły wnioskowania dla rachunku konstrukcji

1 .${\ Displaystyle {{} \ nad \ Gamma \ vdash \ mathbf {P} : \ mathbf {T}}}$

2 .${\displaystyle {{} \nad {\gamma,x:A,\gamma '\vdash x:A}}}$

3 .${\displaystyle {\gamma \vdash A:K\qquad \qquad \gamma,x:A\vdash B:L \nad {\gamma \vdash (\forall x:AB):L}}}$

4 .${\ Displaystyle {\ Gamma \ vdash A: K \ qquad \ qquad \ Gamma, x: A \ vdash N: B \ ponad {\ Gamma \ vdash (\ Lambda x: AN): (\ Forall x: AB)}} }$

5 .${\ Displaystyle {\ Gamma \ vdash M: (\ forall x: AB) \ qquad \ qquad \ Gamma \ vdash N: A \ ponad {\ Gamma \ vdash MN: B [x: = N]}}}$

6 . ${\ Displaystyle {\ Gamma \ vdash M: A \ qquad \ qquad A = _ {\ beta} B \ qquad \ qquad \ Gamma \ vdash B: K \ ponad {\ Gamma \ vdash M: B}}}$

Definiowanie operatorów logicznych

Rachunek konstrukcji ma bardzo niewiele podstawowych operatorów: jedynym operatorem logicznym do tworzenia zdań jest . Jednak ten jeden operator wystarcza do zdefiniowania wszystkich pozostałych operatorów logicznych: ${\displaystyle \forall}$

$( A\Rightarrow B\Rightarrow C)\Rightarrow C&\\A\vee B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C&\\\ neg A&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)&\\\exists x:AB&\equiv &\forall C:\mathbf {P} .(\forall x:A.( B\Rightarrow C))\Rightarrow C&\end{array}}}$

Definiowanie typów danych

Podstawowe typy danych stosowane w informatyce można zdefiniować w ramach rachunku konstrukcji:

wartości logiczne

${\ Displaystyle \ forall A: \ mathbf {P} . A \ Strzałka w prawo A \ Strzałka w prawo A}$

Naturalni

${\ Displaystyle \ forall A: \ mathbf {P}. (A \ Strzałka w prawo A) \ Strzałka w prawo (A \ Strzałka w prawo A)}$

Produkt ${\displaystyle A\razy B}$

${\ Displaystyle A \ klin B}$

Związek rozłączny ${\displaystyle A+B}$

${\displaystyle A\vee B}$

Zauważ, że Boole's i Naturals są definiowane w taki sam sposób jak w kodowaniu Church'a . Jednak dodatkowe problemy wynikają z ekstensjonalności zdań i nieistotności dowodu.

Zobacz też

• System typu czystego
• Kostka lambda
• System F
• Typ zależny
• Teoria typów intuicjonistycznych
• Teoria typów homotopii

Bibliografia