Teoria typu intuicjonistycznego - Intuitionistic type theory

Intuicjonistyczna teoria typów (znana również jako teoria typów konstruktywnych lub teoria typów Martina-Löfa ) jest teorią typów i alternatywną podstawą matematyki . Intuicjonistyczna teoria typów została stworzona przez Pera Martina-Löfa , szwedzkiego matematyka i filozofa , który po raz pierwszy opublikował ją w 1972 roku. Istnieje wiele wersji teorii typów: Martin-Löf zaproponował zarówno intensjonalne, jak i ekstensjonalne warianty teorii oraz wczesne wersje implikacyjne , okazał się niespójny przez paradoks Girarda , ustąpił miejsca orzecznikowiwersje. Jednak wszystkie wersje zachowują podstawowy projekt logiki konstruktywnej przy użyciu typów zależnych.

Projekt

Martin-Löf zaprojektował teorię typów na zasadach konstruktywizmu matematycznego . Konstruktywizm wymaga, aby każdy dowód istnienia zawierał „świadka”. Tak więc każdy dowód na to, że „istnieje liczba pierwsza większa niż 1000” musi identyfikować konkretną liczbę, która jest zarówno liczbą pierwszą, jak i większą niż 1000. Teoria typów intuicjonistycznych osiągnęła ten cel projektowy poprzez internalizację interpretacji BHK . Interesującą konsekwencją jest to, że dowody stają się obiektami matematycznymi, które można badać, porównywać i manipulować.

Konstruktory typów intuicjonistycznej teorii typów zostały zbudowane tak, aby podążały za korespondencją jeden-do-jednego z logicznymi spójnikami. Na przykład spójnik logiczny o nazwie implikacja ( ) odpowiada typowi funkcji ( ). Ta korespondencja nazywana jest izomorfizmem Curry-Howarda . Poprzednie teorie typów również podążały za tym izomorfizmem, ale Martin-Löf jako pierwszy rozszerzył go o logikę predykatów , wprowadzając typy zależne . ${\displaystyle A\implikuje B}$${\ Displaystyle A \ do B}$

Teoria typów

Intuicjonistyczna teoria typów ma 3 skończone typy, które następnie składa się z 5 różnych konstruktorów typów. W przeciwieństwie do teorii mnogości, teorie typów nie są oparte na logice takiej jak teoria Frege'a . Tak więc każda cecha teorii typów spełnia podwójną funkcję jako cecha zarówno matematyki, jak i logiki.

Jeśli nie znasz teorii typów i znasz teorię zbiorów, krótkie podsumowanie jest następujące: Typy zawierają terminy, tak jak zbiory zawierają elementy. Terminy należą do jednego i tylko jednego typu. Terminy takie jak i obliczają („redukują”) do terminów kanonicznych, takich jak 4. Więcej informacji można znaleźć w artykule Teoria typów .${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$

0 typ, 1 typ i 2 typ

Istnieją 3 typy skończone: Typ 0 zawiera 0 terminów. Typ 1 zawiera 1 termin kanoniczny. I 2 typu zawiera 2 warunki kanoniczne.

Ponieważ typ 0 zawiera 0 terminów, jest również nazywany typem pustym . Służy do reprezentowania wszystkiego, co nie może istnieć. Jest również napisane i przedstawia wszystko, czego nie można udowodnić. (Oznacza to, że dowód na to nie może istnieć). W rezultacie negacja jest definiowana jako funkcja do niej: . ${\displaystyle \bot}$${\ Displaystyle \ neg A: = A \ do \ bot}$

Podobnie typ 1 zawiera 1 termin kanoniczny i reprezentuje istnienie. Jest również nazywany typem jednostki . Często reprezentuje twierdzenia, które można udowodnić i dlatego czasami jest napisane . ${\ Displaystyle \ top}$

Wreszcie, 2 rodzaj zawiera 2 warunki kanoniczne. Reprezentuje definitywny wybór między dwiema wartościami. Jest używany dla wartości logicznych, ale nie propozycji. Propozycje są uważane za typ 1 i mogą zostać udowodnione, że nigdy nie mają dowodu ( typ 0 ) lub mogą nie zostać udowodnione w żaden sposób. ( Prawo wykluczonego środka nie dotyczy twierdzeń w teorii typów intuicjonistycznych).

Σ typ konstruktor

Typy Σ zawierają uporządkowane pary. Podobnie jak w przypadku typowych uporządkowanych typów par (lub dwukrotnych ), typ Σ może opisywać iloczyn kartezjański , , dwóch innych typów, i . Logicznie rzecz biorąc, taka uporządkowana para zawierałaby dowód i dowód , więc można zobaczyć taki typ zapisany jako . ${\displaystyle A\razy B}$${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle A \ klin B}$

Typy są bardziej zaawansowane niż typowe uporządkowane typy par ze względu na typowanie zależne . W parze uporządkowanej rodzaj drugiego terminu może zależeć od wartości pierwszego terminu. Na przykład pierwszy wyraz pary może być liczbą naturalną, a typ drugiego wyrazu może być wektorem o długości równej pierwszemu wyrazowi. Taki typ byłby napisany:

${\ Displaystyle \ suma _ {n {\ mathbin {:}} {\ mathbb {N}}} \ nazwa operatora {Vec} ({\ mathbb {R}}, n)}$

Używając terminologii teorii mnogości, jest to podobne do indeksowanych rozłącznych związków zbiorów. W przypadku zwykłych par porządkowych rodzaj drugiego terminu nie zależy od wartości pierwszego terminu. W ten sposób typ opisujący iloczyn kartezjański jest napisany: ${\displaystyle {\mathbb {N}}\razy {\mathbb {R}}}$

${\ Displaystyle \ suma _ {n {\ mathbin {:}} {\ mathbb {N}}} {\ mathbb {R}}}$

Należy tutaj zauważyć, że wartość pierwszego wyrazu, , nie zależy od typu drugiego wyrazu, . ${\ Displaystyle n}$${\displaystyle {\mathbb {R}}}$

Oczywiście, typy mogą być używane do budowania dłuższych krotek o typach zależnych używanych w matematyce oraz rekordów lub struktur używanych w większości języków programowania. Przykładem zależnej trójki są dwie liczby całkowite i dowód, że pierwsza liczba całkowita jest mniejsza niż druga liczba całkowita, opisana przez typ:

${\ Displaystyle \ suma _ {m {\ mathbin {:}} {\ mathbb {Z}}} {\ suma _ {n {\ mathbin {:}} {\ mathbb {Z}}} ((m < n) ={\text{Prawda}})}}$

Typowanie zależne pozwala typom pełnić rolę kwantyfikatora egzystencjalnego . Zdanie „istnieje typ typu , taki jaki jest udowodniony” staje się typem uporządkowanych par, gdzie pierwsza pozycja jest wartością typu, a druga jest dowodem . Zauważ, że rodzaj drugiej pozycji (dowodów ) zależy od wartości w pierwszej części zamówionej pary ( ). Jego typ to: ${\ Displaystyle n}$${\ Displaystyle {\ mathbb {N} }}$${\ Displaystyle P (n)}$${\ Displaystyle n}$${\ Displaystyle {\ mathbb {N} }}$${\ Displaystyle P (n)}$${\ Displaystyle P (n)}$${\ Displaystyle n}$

${\ Displaystyle \ suma _ {n {\ mathbin {:}} {\ mathbb {N}}} P (n)}$

Π typ konstruktor

Typy zawierają funkcje. Podobnie jak w przypadku typowych typów funkcji, składają się one z typu wejścia i typu wyjścia. Są one jednak bardziej zaawansowane niż typowe typy funkcji, ponieważ typ zwracany może zależeć od wartości wejściowej. Funkcje w teorii typów różnią się od teorii mnogości. W teorii mnogości sprawdzasz wartość argumentu w zestawie uporządkowanych par. W teorii typów argument jest zastępowany terminem, a następnie stosowane jest do niego obliczenie („redukcja”).

Jako przykład zapisano typ funkcji, która przy danej liczbie naturalnej zwraca wektor zawierający liczby rzeczywiste: ${\ Displaystyle n}$${\ Displaystyle n}$

${\ Displaystyle \ prod _ {n {\ mathbin {:}} {\ mathbb {N} }} \ operatorname {Vec} ({\ mathbb {R}}, n)}$

Gdy typ wyjścia nie zależy od wartości wejściowej, typ funkcji jest często zapisywany po prostu z . Tak więc jest rodzaj funkcji od liczb naturalnych do liczb rzeczywistych. Takie Π-typy odpowiadają logicznej implikacji. Propozycja logiczna odpowiada typowi zawierającemu funkcje, które pobierają dowody A i zwracają dowody B. Ten typ można by zapisać bardziej konsekwentnie jako: ${\ Displaystyle \ do}$${\displaystyle {\mathbb {N}}\do {\mathbb {R}}}$${\displaystyle A\implikuje B}$${\ Displaystyle A \ do B}$

${\ Displaystyle \ prod _ {a {\ mathbin {:}} A} B}$

Typy Π są również używane w logice do uniwersalnej kwantyfikacji . Stwierdzenie „dla każdego typu , jest udowodnione” staje się funkcja od typu do dowodów . Zatem podana wartość funkcji generuje dowód, który jest spełniony dla tej wartości. Typ byłby ${\ Displaystyle n}$${\ Displaystyle {\ mathbb {N} }}$${\ Displaystyle P (n)}$${\ Displaystyle n}$${\ Displaystyle {\ mathbb {N} }}$${\ Displaystyle P (n)}$${\ Displaystyle n}$${\displaystyle P()}$

${\ Displaystyle \ prod _ {n {\ mathbin {:}} {\ mathbb {N}}} P (n)}$

= wpisz konstruktor

Typy = są tworzone z dwóch terminów. Mając dwa terminy, takie jak i , możesz utworzyć nowy typ . Terminy tego nowego typu stanowią dowody, że para sprowadza się do tego samego terminu kanonicznego. Tak więc, ponieważ zarówno i obliczyć do terminu kanonicznego , będzie termin typu . W intuicjonistycznej teorii typów istnieje jeden sposób tworzenia terminów typów = i to poprzez refleksyjność : ${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\ Displaystyle 2 + 2 = 2 \ cdot 2}$${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\ Displaystyle 4}$${\ Displaystyle 2 + 2 = 2 \ cdot 2}$

${\displaystyle \operatorname {refl} {\mathbin {:}}\prod _{a{\mathbin {:}}A}(a=a).}$

Możliwe jest tworzenie typów = takich, w których terminy nie są zredukowane do tego samego terminu kanonicznego, ale nie będzie można tworzyć terminów tego nowego typu. W rzeczywistości, gdybyś był w stanie stworzyć wyraz , mógłbyś utworzyć wyraz . Umieszczenie tego w funkcji wygeneruje funkcję typu . Ponieważ tak intuicjonistyczna teoria typów definiuje negację, należałoby lub w końcu . ${\ Displaystyle 1 = 2}$${\ Displaystyle 1 = 2}$${\displaystyle \bot}$${\displaystyle 1=2\do \bot}$${\ Displaystyle \ ldots \ do \ bot}$${\ Displaystyle \ neg (1 = 2)}$${\displaystyle 1\neq 2}$

Równość dowodów jest obszarem aktywnych badań w teorii dowodu i doprowadziła do rozwoju teorii typów homotopii i innych teorii typów.

Typy indukcyjne

Typy indukcyjne umożliwiają tworzenie złożonych typów samoodnoszących się. Na przykład połączona lista liczb naturalnych jest albo listą pustą, albo parą liczb naturalnych i inną połączoną listą. Typy indukcyjne mogą być używane do definiowania nieograniczonych struktur matematycznych, takich jak drzewa, wykresy itp. W rzeczywistości typ liczb naturalnych może być zdefiniowany jako typ indukcyjny, będący albo bytem, albo następcą innej liczby naturalnej. ${\ Displaystyle 0}$

Typy indukcyjne definiują nowe stałe, takie jak zero i funkcja następnika . Ponieważ nie ma definicji i nie może być oceniany przez podstawienie, terminy takie jak i stają się terminami kanonicznymi liczb naturalnych. ${\ Displaystyle 0 {\ mathbin {:}} {\ mathbb {N}}}$${\ Displaystyle S {\ mathbin {:}} {\ mathbb {N}} \ do {\ mathbb {N}}}$${\displaystyle S}$${\ Displaystyle S0}$${\displaystyle SSS0}$

Dowody na typach indukcyjnych są możliwe dzięki indukcji . Każdy nowy typ indukcyjny ma swoją własną regułę indukcyjną. Aby udowodnić predykat dla każdej liczby naturalnej, użyj następującej reguły: ${\displaystyle P()}$

${\displaystyle {\operatorname {{\mathbb {N}}-elim}}\,{\mathbin {:}}P(0)\,\do \lewo(\prod_{n{\mathbin {:}} {\mathbb {N} }}P(n)\do P(S(n))\right)\do \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n) }$

Typy indukcyjne w intuicjonistycznej teorii typów są definiowane w kategoriach typów W, typu drzew dobrze ugruntowanych . Późniejsze prace nad teorią typów wygenerowały typy koindukcyjne, indukcyjno-rekursywne i indukcyjno-indukcyjne do pracy nad typami o bardziej niejasnych rodzajach autoodniesienia. Wyższe typy indukcyjne umożliwiają zdefiniowanie równości między terminami.

Typy wszechświata

Typy wszechświata pozwalają na pisanie dowodów na wszystkie typy utworzone za pomocą innych konstruktorów typów. Każdy termin w typie uniwersum może być odwzorowany na typ utworzony za pomocą dowolnej kombinacji konstruktora typu indukcyjnego. Jednak, aby uniknąć paradoksów, nie ma w tych mapach terminu . ${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle 0,1,2,\Sigma,\pi,=,}$${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{0}}$

Aby napisać dowody dotyczące wszystkich „małych typów” i , musisz użyć , które zawiera termin dla , ale nie dla siebie . Podobnie dla . Istnieje predykatywna hierarchia wszechświatów, więc aby określić ilościowo dowód na dowolne stałe, stałe wszechświaty, możesz użyć . ${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{2}}$${\displaystyle k}$${\ Displaystyle {\ Mathcal {U}} _ {k + 1}}$

Typy wszechświatów są trudną cechą teorii typów. Oryginalna teoria typów Martina-Löfa musiała zostać zmieniona, aby uwzględnić paradoks Girarda . Późniejsze badania obejmowały takie tematy, jak „super wszechświaty”, „wszechświaty Mahlo” i wszechświaty nieprzydatne.

Wyroki

Formalna definicja teorii typu intuicjonistycznego jest napisana za pomocą osądów. Na przykład w zdaniu „jeśli jest typem i jest typem to jest typem” występują osądy „jest typem”, „i” oraz „jeśli… to…”. Wyrażenie to nie jest osądem; jest to definiowany typ. ${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle \ textstyle \ suma _ {a: A} B}$${\ Displaystyle \ textstyle \ suma _ {a: A} B}$

Ten drugi poziom teorii typów może być mylący, szczególnie jeśli chodzi o równość. Istnieje osąd terminu równość, który może powiedzieć . Jest to stwierdzenie, że dwa terminy sprowadzają się do tego samego terminu kanonicznego. Istnieje również orzeczenie o równości typów, powiedzmy , co oznacza, że ​​każdy element jest elementem typu i na odwrót. Na poziomie typu istnieje typ i zawiera terminy, jeśli istnieje dowód na to i sprowadza się do tej samej wartości. (Oczywiście, terminy tego typu są generowane przy użyciu terminu osąd równości.) Wreszcie, istnieje anglojęzyczny poziom równości, ponieważ używamy słowa „cztery” i symbolu „ ” w odniesieniu do terminu kanonicznego . Synonimy takie jak te są nazywane przez Martina-Löfa „zdecydowanie równymi”. ${\displaystyle 4=2+2}$${\ Displaystyle A = B}$${\ Displaystyle A}$${\ Displaystyle B}$${\displaystyle 4=2+2}$${\ Displaystyle 4}$${\displaystyle 2+2}$${\ Displaystyle 4}$${\displaystyle SSSS0}$

Poniższy opis orzeczeń opiera się na dyskusji w Nordström, Petersson i Smith.

Teoria formalna działa z typami i przedmiotami .

Typ deklaruje:

• ${\displaystyle A\ {\mathsf {typ}}}$

Obiekt istnieje i należy do typu, jeśli:

• ${\ Displaystyle a {\ mathbin {:}} A}$

Obiekty mogą być równe

• ${\displaystyle a=b}$

i typy mogą być równe

• ${\ Displaystyle A = B}$

Deklarowany jest typ zależny od obiektu z innego typu

• ${\ Displaystyle (x {\ mathbin {:}} A) B}$

i usunięte przez podstawienie

• ${\displaystyle B[x/a]}$, zastępując zmienną obiektem w .${\displaystyle x}$${\displaystyle a}$${\ Displaystyle B}$

Obiekt zależny od obiektu innego typu można wykonać na dwa sposoby. Jeśli obiekt jest „abstrakcyjny”, to jest napisany

• ${\displaystyle [x]b}$

i usunięte przez podstawienie

• ${\displaystyle b[x/a]}$, zastępując zmienną obiektem w .${\displaystyle x}$${\displaystyle a}$${\displaystyle b}$

Obiekt zależny od obiektu można również zadeklarować jako stałą jako część typu rekurencyjnego. Przykładem typu rekurencyjnego jest:

• ${\ Displaystyle 0 {\ mathbin {:}} \ mathbb {N}}$
• ${\ Displaystyle S {\ mathbin {:}} \ mathbb {N} \ do \ mathbb {N}}$

Oto stały obiekt zależny od obiektu. Nie kojarzy się z abstrakcją. Stałe takie jak można usunąć, definiując równość. Tutaj relacja z dodawaniem jest definiowana za pomocą równości i dopasowywania wzorców do obsługi rekurencyjnego aspektu : ${\displaystyle S}$${\displaystyle S}$${\displaystyle S}$

${\ Displaystyle {\ zacząć {wyrównany} \ operatorname {dodaj} i {\ mathbin {:}} \ (\ mathbb {N} \ razy \ mathbb {N} ) \ do \ mathbb {N} \ \ \ operatorname {dodaj } (0,b)&=b\\\nazwa operatora {dodaj} (S(a),b)&=S(\nazwa operatora {dodaj} (a,b)))\end{wyrównany}}}$

${\displaystyle S}$ jest manipulowana jako stała nieprzezroczysta - nie ma wewnętrznej struktury do podstawienia.

Tak więc obiekty i typy oraz te relacje służą do wyrażania formuł w teorii. Następujące style osądów służą do tworzenia nowych obiektów, typów i relacji z już istniejących:

${\ Displaystyle \ Gamma \ vdash \ sigma \ {\ mathsf {typ}}}$	σ jest dobrze uformowanym typem w kontekście Γ.
${\ Displaystyle \ Gamma \ vdash t {\ mathbin {:}} \ sigma}$	t jest dobrze sformułowanym terminem typu σ w kontekście Γ.
${\ Displaystyle \ Gamma \ vdash \ sigma \ równoważnik \ tau}$	σ i τ są równymi typami w kontekście Γ.
${\ Displaystyle \ Gamma \ vdash t \ równoważnik u {\ mathbin {:}} \ sigma}$	t i u są sądownie równymi terminami typu σ w kontekście Γ.
${\ Displaystyle \ vdash \ Gamma \ {\ mathsf {kontekst}}}$	Γ to dobrze sformułowany kontekst typowania założeń.

Zgodnie z konwencją istnieje typ reprezentujący wszystkie inne typy. Nazywa się (lub ). Ponieważ jest typem, jego członkowie są obiektami. Istnieje typ zależny, który odwzorowuje każdy obiekt na odpowiadający mu typ. W większości tekstów nigdy nie jest napisane. Na podstawie kontekstu wypowiedzi czytelnik prawie zawsze może stwierdzić, czy odnosi się do typu, czy też odnosi się do obiektu, który odpowiada typowi. ${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {zestaw}}$${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {El}}$${\displaystyle \operatorname {El}}$${\ Displaystyle A}$${\displaystyle {\mathcal {U}}}$

To jest kompletna podstawa teorii. Wszystko inne pochodzi.

Aby zaimplementować logikę, każda propozycja ma swój własny typ. Obiekty w tych typach reprezentują różne możliwe sposoby udowodnienia propozycji. Oczywiście, jeśli nie ma dowodu na zdanie, to typ nie ma w nim obiektów. Operatory takie jak „i” i „lub”, które działają na propozycjach, wprowadzają nowe typy i nowe obiekty. Podobnie jest z typem, który zależy od typu i typu . Obiekty w tym typie zależnym są zdefiniowane tak, aby istniały dla każdej pary obiektów w i . Oczywiście, jeśli lub nie ma dowodu i jest typem pustym, to nowy reprezentujący typ również jest pusty. ${\displaystyle A\razy B}$${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle A}$${\ Displaystyle B}$${\displaystyle A\razy B}$

Można to zrobić dla innych typów (liczby logiczne, liczby naturalne itp.) i ich operatorów.

Modele kategoryczne teorii typów

Używając języka teorii kategorii , RAG Seely wprowadził pojęcie lokalnie kartezjańskiej kategorii zamkniętej (LCCC) jako podstawowy model teorii typów. Zostało to udoskonalone przez Hofmanna i Dybjera do kategorii z rodzinami lub kategorii z atrybutami na podstawie wcześniejszych prac Cartmella.

Kategoria z rodzinami to kategoria C kontekstów (w której obiekty są kontekstami, a morfizmy kontekstu są podstawieniami) wraz z funktorem T  : C ^op → Fam ( Zbiór ).

Fam ( Zbiór ) to kategoria rodzin Zbiorów, w której obiekty są parami „zestawu indeksów” A i funkcji B : X → A , a morfizmy są parami funkcji f  : A → A' i g  : X → X' , takie, że B' _° g = f _° B — innymi słowy, f odwzorowuje B _a na B _{g ( a )} . ${\ Displaystyle (A, B)}$

Funktor T przypisuje kontekstowi G zbiór typów, a dla każdego , zbiór terminów. Aksjomaty funktora wymagają, aby współgrały one harmonijnie z podstawieniem. Zmiana jest zazwyczaj tworzona w postaci Af lub AF , gdzie jest typu, w i jest warunek w , i M oznacza podstawienie od D do G . Tutaj i . ${\ Displaystyle Ty (G)}$${\ Displaystyle A: Ty (G)}$${\ Displaystyle Tm (G, A)}$${\ Displaystyle Ty (G)}$${\ Displaystyle Tm (G, A)}$${\ Displaystyle Af: Ty (D)}$${\displaystyle af:Tm(D,Af)}$

Kategoria C musi zawierać obiekt końcowy (pusty kontekst) oraz obiekt końcowy formy produktu zwanej zrozumieniem lub rozszerzeniem kontekstu, w którym prawy element jest typem w kontekście lewego elementu. Jeżeli G jest kontekstem, i , to powinien istnieć obiekt finalny pomiędzy kontekstami D z odwzorowaniami p  : D → G , q  : Tm ( D,Ap ). ${\ Displaystyle A: Ty (G)}$${\ Displaystyle (G, A)}$

Ramy logiczne, takie jak u Martina-Löfa, przybierają postać warunków zamknięcia na kontekstowych zestawach typów i terminów: że powinien istnieć typ o nazwie Zestaw, a dla każdego zestawu typ, że typy powinny być zamknięte w formach suma zależna i produkt, i tak dalej.

Teoria taka jak predykatywna teoria mnogości wyraża warunki domknięcia na typach zbiorów i ich elementach: że powinny one być domknięte w operacjach, które odzwierciedlają sumę zależną i iloczyn oraz w różnych formach definicji indukcyjnej.

Ekstensywny kontra intensjonalny

Podstawowym rozróżnieniem jest teoria typu ekstensjonalnego i intensjonalnego . W ekstensjonalnej teorii typów równość definicyjna (tj. obliczeniowa) nie różni się od równości zdań, która wymaga dowodu. W konsekwencji sprawdzanie typów staje się nierozstrzygalne w teorii typów ekstensjonalnych, ponieważ programy w teorii mogą się nie kończyć. Na przykład taka teoria pozwala nadać typ kombinatorowi Y , szczegółowy przykład tego można znaleźć w Nordstöm and Petersson Programming w Martin-Löf's Type Theory . Nie oznacza to jednak, że teoria typów ekstensjonalnych może być podstawą dla praktycznego narzędzia, na przykład NuPRL jest oparty na teorii typów ekstensywnych.

W przeciwieństwie do teorii typów intensjonalnych, sprawdzanie typu jest rozstrzygalne , ale reprezentacja standardowych pojęć matematycznych jest nieco bardziej kłopotliwa, ponieważ rozumowanie intensjonalne wymaga użycia setoidów lub podobnych konstrukcji. Istnieje wiele wspólnych obiektów matematycznych, które są trudne do pracy z lub nie mogą być reprezentowane bez tego, na przykład, liczby całkowite , liczby wymierne , a liczbami rzeczywistymi . Liczby całkowite i wymierne mogą być reprezentowane bez setoidów, ale ta reprezentacja nie jest łatwa w obsłudze. Bez tego nie można przedstawić liczb rzeczywistych Cauchy'ego.

Teoria typów homotopii pracuje nad rozwiązaniem tego problemu. Pozwala na zdefiniowanie wyższych typów indukcyjnych , które nie tylko definiują konstruktory pierwszego rzędu ( wartości lub punkty ), ale konstruktory wyższego rzędu, tj. równości między elementami ( ścieżki ), równości między równościami ( homotopie ), ad infinitum .

Implementacje teorii typów

Różne formy teorii typów zostały zaimplementowane jako systemy formalne leżące u podstaw wielu asystentów dowodu . Chociaż wiele z nich opiera się na pomysłach Pera Martina-Löfa, wiele z nich ma dodatkowe cechy, więcej aksjomatów lub inne podstawy filozoficzne. Na przykład system NuPRL oparty jest na teorii typów obliczeniowych, a Coq na rachunku konstrukcji (ko)indukcyjnych . Typy zależne są również wykorzystywane w projektowaniu języków programowania, takich jak ATS , Cayenne , Epigram , Agda i Idris .

Teorie typu Martina-Löfa

Per Martin-Löf skonstruował kilka teorii typów, które były publikowane w różnym czasie, niektóre z nich znacznie później niż w momencie, gdy przeddruki z ich opisem stały się dostępne dla specjalistów (m.in. Jean-Yves Girard i Giovanni Sambin). Poniższa lista jest próbą zestawienia wszystkich teorii, które zostały opisane w formie drukowanej oraz naszkicowania kluczowych cech, które je od siebie odróżniały. Wszystkie te teorie miały iloczyny zależne, sumy zależne, związki rozłączne, typy skończone i liczby naturalne. Wszystkie teorie miały te same reguły redukcji, które nie uwzględniały -redukcji ani dla produktów zależnych, ani dla sum zależnych, z wyjątkiem MLTT79, gdzie dodaje się -redukcję dla produktów zależnych.

MLTT71 była pierwszą z teorii typów stworzonych przez Pera Martina-Löfa. Pojawił się w preprintie w 1971 roku. Miał jeden wszechświat, ale ten wszechświat miał nazwę samą w sobie, tj. był teorią typów z, jak to się dziś nazywa, "Typem w typie". Jean-Yves Girard wykazał, że ten system był niespójny, a preprint nigdy nie został opublikowany.

MLTT72 został przedstawiony w preprint z 1972 roku, który został opublikowany. Ta teoria miała jeden wszechświat V i żadnych typów tożsamości. Wszechświat był „predykatywny” w tym sensie, że nie zakładano, że zależny iloczyn rodziny obiektów z V przez obiekt, którego nie ma w V, jak na przykład samo V. Russell, tj. można by pisać bezpośrednio „T∈V” i „t∈T” (Martin-Löf używa znaku „∈” zamiast współczesnego „:”) bez dodatkowego konstruktora, takiego jak „El”.

MLTT73 była pierwszą definicją teorii typów, którą opublikował Per Martin-Löf (została zaprezentowana na Logic Colloquium 73 i opublikowana w 1975 roku). Istnieją typy tożsamości, które nazywa on „zdaniami”, ale ponieważ nie wprowadza się rzeczywistego rozróżnienia między zdaniami a pozostałymi typami, znaczenie tego jest niejasne. Jest to, co później przybiera nazwę J-eliminator, ale jeszcze bez nazwy (zob. s. 94–95). W tej teorii istnieje nieskończony ciąg wszechświatów V ₀ , ..., V _n , ... . Wszechświaty są predykatywne, a la Russell i nie kumulują się ! W rzeczywistości wniosek 3.10 na s. 115 mówi, że jeśli A∈V _m i B∈V _n są takie, że A i B są zamienialne, to m  =  n . Oznacza to na przykład, że trudno byłoby sformułować jednoznaczność w tej teorii — w każdym z V _i istnieją typy kurczliwe, ale nie jest jasne, jak zadeklarować je jako równe, ponieważ nie ma typów tożsamości łączących V _i i V _j dla i ≠ j .

MLTT79 został zaprezentowany w 1979 roku i opublikowany w 1982 roku. W tym artykule Martin-Löf przedstawił cztery podstawowe typy sądów dla teorii typów zależnych, która od tego czasu stała się fundamentalna w badaniu metateorii takich systemów. Wprowadził w nim także konteksty jako odrębne pojęcie (zob. s. 161). Istnieją typy tożsamości z eliminatorem J (który pojawił się już w MLTT73, ale nie miał tam tej nazwy), ale także z regułą, która czyni teorię „ekstensjonalną” (s. 169). Są typy W. Istnieje nieskończona sekwencja orzecznikowych wszechświatów, które się kumulują .

Bibliopolis : istnieje dyskusja na temat teorii typów w książce Bibliopolis z 1984 roku, ale jest ona nieco otwarta i wydaje się, że nie reprezentuje określonego zestawu wyborów, a więc nie ma z nią powiązanej konkretnej teorii typów.

Zobacz też

• Logika intuicjonistyczna
• Wpisany rachunek lambda

Uwagi

Bibliografia

• Martin-Löf, Per (1984). Teoria typów intuicjonistycznych (PDF) . Sambin, Giovanni. Neapol: Bibliopolis. Numer ISBN 978-8870881059. OCLC  12731401 .

Dalsza lektura

• Według notatek Martina-Löfa, nagrany przez Giovanniego Sambina (1980)
• Nordström, Bengt; Petersson, Kent; Smith, Jan M. (1990). Programowanie w teorii typów Martina-Löfa . Oxford University Press. Numer ISBN 9780198538141.
• Thompson, Simon (1991). Teoria typów i programowanie funkcjonalne . Addisona-Wesleya. Numer ISBN 0-201-41667-0.
• Granström, Johan G. (2011). Traktat o intuicjonistycznej teorii typów . Skoczek. Numer ISBN 978-94-007-1735-0.

Linki zewnętrzne

• Projekt EU Types: Tutoriale – notatki z wykładów i slajdy z Letniej Szkoły Types 2005
• n-Kategorie - Szkic definicji – list Johna Baeza i Jamesa Dolana do Ross Street , 29 listopada 1995