Jak zdobyć Rachunek Konstrukcji z innych punktów w Kostce Lambda?

CoC jest zwieńczeniem wszystkich trzech wymiarów Lambda Cube. To wcale nie jest dla mnie oczywiste. Wydaje mi się, że rozumiem poszczególne wymiary, a połączenie dowolnych dwóch wydaje się skutkować względnie prostym zjednoczeniem (może czegoś mi brakuje?). Ale kiedy patrzę na CoC, zamiast wyglądać jak połączenie wszystkich trzech, wygląda to zupełnie inaczej. Z jakiego wymiaru pochodzą typy, podpory i małe / duże typy? Gdzie zniknęły produkty zależne? I dlaczego skupia się na propozycjach i dowodach zamiast typów i programów? Czy istnieje coś równoważnego, co koncentruje się na typach i programach?

Edycja: W przypadku, gdy nie jest to jasne, proszę o wyjaśnienie, w jaki sposób CoC jest równoważne z prostym połączeniem wymiarów Kostki Lambda. I czy istnieje gdzieś faktyczny związek wszystkich trzech (gdzieś pod względem programów i typów, a nie dowodów i propozycji)? Jest to odpowiedź na komentarze do pytania, a nie na bieżące odpowiedzi.

lambda-calculus type-systems typed-lambda-calculus calculus-of-constructions indil
źródło

Przynajmniej powinno to być soft-question. Nie widzę tu właściwie pytania technicznego. Być może możesz być bardziej szczegółowy w kwestii tego, o co pytasz?

Andrej Bauer

@AndrejBauer Czy nie jest pytanie: jaki jest związek między prezentacją CoC Barendregt-cube / PTS a oryginalną prezentacją Coquand & Huet?

Martin Berger

@AndrejBauer: Wydaje się, że pytanie dotyczy także różnicy w prezentacji CoC (w obu postaciach) i nacisku na niektóre funkcje w praktyce. Prawdą jest, że wersja CoC zorientowana na PTS podkreśla niektóre cechy jako ważne, podczas gdy praktyka Coq podkreśla inne. Zgadzam się, że powinien mieć tag miękkiego pytania.

Jacques Carette

Cieszę się, że ktoś będzie w stanie odpowiedzieć na to pytanie.

Andrej Bauer

Odpowiedzi:

Po pierwsze, aby powtórzyć jeden z punktów Cody, Rachunek konstrukcji indukcyjnych (na których opiera się jądro Coqa) bardzo różni się od Rachunku konstrukcji. Najlepiej jest zacząć od teorii typów Martina-Löfa od wszechświatów, a następnie dodać prop sort na dole hierarchii typów. Jest to zupełnie inna bestia niż oryginalny CoC, który najlepiej jest uważać za zależną wersję F-omegi. (Na przykład CiC ma modele teoretyczne, a CoC nie.)

To powiedziawszy, sześcian lambda (którego członkiem jest CoC) jest zazwyczaj przedstawiany jako system czystego rodzaju ze względu na oszczędność pod względem liczby zasad pisania. Traktując rodzaje, typy i terminy jako elementy tej samej kategorii składniowej, możesz zapisać o wiele mniej reguł, a twoje dowody również stają się nieco mniej zbędne.

Jednak dla zrozumienia pomocne może być wyraźne oddzielenie różnych kategorii. Możemy wprowadzić trzy kategorie składniowe, rodzaje (z podziałem na metazmowę k), typy (z podziałem na metawazę A) i terminy (z podziałem na metaznaturę e). Następnie wszystkie osiem systemów można rozumieć jako wariacje tego, co jest dozwolone na każdym z trzech poziomów.

λ → (Rachunek prosty lambda)

 k ::= ∗
 A ::= p | A → B
 e ::= x | λx:A.e | e e

Jest to podstawowy typowy rachunek lambda. Istnieje jeden rodzaj ∗, który jest rodzajem typów. Same typy to typy atomowe pi typy funkcji A → B. Terminy to zmienne, abstrakcje lub aplikacje.

λω_ (STLC + operatory wyższego rodzaju)

 k ::= ∗ | k → k
 A ::= a | p | A → B | λa:k.A | A B
 e ::= x | λx:A.e | e e

STLC pozwala na abstrakcję tylko na poziomie terminów. Jeśli dodamy go na poziomie typów, dodamy nowy rodzaj, k → kktóry jest typem funkcji na poziomie typu, a także abstrakcję λa:k.Ai aplikację A Bna poziomie typu. Więc teraz nie mamy polimorfizmu, ale mamy operatory typu.

Jeśli pamięć służy, ten system nie ma więcej mocy obliczeniowej niż STLC; po prostu daje możliwość skracania typów.

λ2 (System F)

 k ::= ∗
 A ::= a | p | A → B  | ∀a:k. A 
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Zamiast dodawać operatory typu, moglibyśmy dodać polimorfizm. Na poziomie typu dodajemy, ∀a:k. Aktóry jest wzorem typu polimorficznego, a na poziomie terminu dodajemy abstrakcję do typów Λa:k. ei aplikacji typów e [A].

Ten system jest znacznie potężniejszy niż STLC - jest tak silny, jak arytmetyka drugiego rzędu.

λω (System F-omega)

 k ::= ∗ | k → k 
 A ::= a | p | A → B  | ∀a:k. A | λa:k.A | A B
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Jeśli mamy zarówno operatory typu, jak i polimorfizm, otrzymujemy F-omegę. Ten system jest mniej więcej teorią typu jądra większości współczesnych języków funkcjonalnych (takich jak ML i Haskell). Jest również znacznie potężniejszy niż System F - jest równoważny siłą arytmetyki wyższego rzędu.

λP (LF)

 k ::= ∗ | Πx:A. k 
 A ::= a | p | Πx:A. B | Λx:A.B | A [e]
 e ::= x | λx:A.e | e e

Zamiast polimorfizmu moglibyśmy pójść w kierunku zależności od prostego rachunku różniczkowego lambda. Jeśli zezwoliłeś typowi funkcji na użycie jej argumentu w typie zwracanym (tzn. Πx:A. B(x)Zamiast pisać A → B), to otrzymasz λP. Aby było to naprawdę przydatne, musimy rozszerzyć zestaw rodzajów o rodzaj operatorów typów, które przyjmują warunki jako argumenty Πx:A. k, dlatego też musimy dodać odpowiednią abstrakcję Λx:A.Bi aplikację również A [e]na poziomie typu.

Ten system jest czasem nazywany LF lub Edinburgh Logical Framework.

Ma taką samą moc obliczeniową jak prosty rachunek lambda.

λP2 (bez nazwy specjalnej)

 k ::= ∗ | Πx:A. k 
 A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A [e]
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Możemy również dodać polimorfizm do λP, aby uzyskać λP2. Ten system nie jest często używany, więc nie ma określonej nazwy. (Jeden artykuł, który przeczytałem, który go wykorzystał, to indukcja Hermana Geuversa, nie jest możliwy do uzyskania w teorii zależnych typów drugiego rzędu .)

Ten system ma taką samą wytrzymałość jak System F.

λPω_ (bez nazwy specjalnej)

 k ::= ∗ | Πx:A. k | Πa:k. k'
 A ::= a | p | Πx:A. B | Λx:A.B | A [e] | λa:k.A | A B 
 e ::= x | λx:A.e | e e

Możemy również dodać operatory typu do λP, aby uzyskać λPω_. Wymaga to dodania rodzaju Πa:k. k'dla operatorów typów oraz odpowiedniej abstrakcji Λx:A.Bi aplikacji na poziomie typu A [e].

Ponieważ ponownie nie ma skoku w sile obliczeniowej nad STLC, system ten powinien również stanowić dobrą podstawę dla logicznej struktury, ale nikt tego nie zrobił.

λPω (rachunek konstrukcji)

 k ::= ∗ | Πx:A. k | Πa:k. k'
 A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A [e] | λa:k.A | A B 
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]

Wreszcie dochodzimy do λPω, rachunku konstrukcji, poprzez pobranie λPω_ i dodanie wcześniejszego typu polimorficznego ∀a:k.Aoraz abstrakcji na poziomie terminów Λa:k. ei aplikacji e [A]do tego.

Rodzaje tego systemu są znacznie bardziej wyraziste niż w F-omega, ale ma tę samą siłę obliczeniową.

Neel Krishnaswami
źródło

Oczywiście technicznie CoC (bez aksjomatów) ma co najmniej tyle modeli teoretycznych, co CiC, po prostu nie są zbyt dobrzy w modelowaniu pożądanej sytuacji, czyli CoC z aksjomatami liczb naturalnych (powiedzmy

0 \neq 1

$0 \neq 1$

cody

Byłbym też bardzo wdzięczny za odniesienie do konserwatywności

stosunku do STLC. To wydaje się nieoczywiste.

λ ω_

$\lambda\omega\_$

cody

@cody: Nie znam referencji - Kevin Watkins naszkicował mi dowód na tablicy! Chodzi o to, że bierzesz termin wpisany w λω_, umieszczasz wszystkie typy w beta-normalnej eta-długiej formie, a następnie osadzasz go w STLC, wprowadzając świeży typ atomowy dla każdej odrębnej normalnej postaci w oryginalnym programie. To oczywiste, że sekwencje redukcji muszą być ustawione jeden do jednego.

Neel Krishnaswami

@ user833970 fakt, że

nie jest pochodna, jest w rzeczywistości o wiele prostszy niż te inne fakty, o których wspominasz, i nie ma nic wspólnego z kodowaniem

: wynika z faktu, że istnieje dowód nieistotny model CC , w których typy mają co najwyżej jeden element . Jest to zła właściwość, jeśli chcesz logiki, w której istnieje typ z więcej niż jednym elementem (powiedzmy nat). Odniesieniem jest: Nie tak prosty dowód nieistotny model CC autorstwa Miquela i Wernera.

0 \neq 1

$0\neq 1$

n a t

$\mathrm{nat}$

cody

Mówisz, że Fw jest „znacznie silniejszy” niż System F. Czy masz do tego referencję? W szczególności, czy istnieje funkcja liczb naturalnych, którą można udowodnić jako całkowitą w Fw, ale nie w F?

Thorsten Altenkirch

$\lambda$

Najpierw jednak należy prawdopodobnie spróbować rozwiązać różne problemy. Interaktywna przysłowia twierdzeń Coqa opiera się na podstawowej teorii typów, czasem z miłością nazywanej rachunkiem konstrukcji indukcyjnych z wszechświatami . Zauważysz, że jest to coś więcej niż tylko „rachunek konstrukcji”, i rzeczywiście, jest tam o wiele więcej rzeczy niż tylko CoC. W szczególności myślę, że masz wątpliwości co do tego, które funkcje są właściwe w CoC. W szczególności rozróżnienie Set / Prop i wszechświaty nie pojawiają się w CoC.

Nie podam tutaj pełnego przeglądu systemów Pure Type, ale ważna zasada (dla funkcjonalnych PTS, takich jak CoC) jest następująca

\frac{Γ ⊢ A : s Γ, x : A ⊢ B : k}{Γ ⊢ Π x : A . B : k} (s, k) \in R

$\frac{\Gamma\vdash A:s\qquad \Gamma,x:A\vdash B:k}{\Gamma\vdash \Pi x:A.B\ :\ k}\ (s,k)\in R$

$s,k$ $S$ $(s,k)$ $R$ $S$

$S$ $R$ $\Pi x:A.B$

$S$

{*, ◻}

$\{*, \square\}$

R = {(*, *), (◻, ◻), (◻, *), (*, ◻)}

$R=\{(*,*),(\square,\square),(\square,*),(*,\square)\}$

Mamy więc 4 reguły, które odpowiadają 4 różnym celom:

$(*,*)$
$(\square,\square)$
$(\square,*)$
$(*,\square)$

Wyjaśnię każde z nich bardziej szczegółowo.

$A\rightarrow B$ $\Pi x:A.B$ $x$ $B$

$*$ $\mathrm{nat}$ $\mathrm{bool}$ $x=y$ $x$ $y$ $*$

$\mathrm{list}$ $\mathrm{list}:*\rightarrow *$ $\mathrm{list}_{\mathrm{nat}}, \mathrm{list}_{\mathrm{bool}}$ $*\rightarrow *$ $(\square,\square)$

Π t : * . t \to t

$\Pi t:*.\ t\rightarrow t$

λ (t : *) (x : t) . x

$\lambda (t:*)(x:t).x$

Π t : * ._

$\Pi t:*.\_$

(◻, *)

$(\square, *)$

t \to t

$t\rightarrow t$

(*, *)

$(*,*)$

A \land B := Π t : * . (A \to B \to t) \to t

$A\wedge B := \Pi t:*.\ (A \rightarrow B\rightarrow t)\rightarrow t$

A \lor B := Π t : * . (A \to t) \to (B \to t) \to t

$A\vee B := \Pi t:*.\ (A \rightarrow t)\rightarrow(B\rightarrow t)\rightarrow t$

⊥ := Π t : * . t

$\bot := \Pi t:*.\ t$

⊤ := Π t : * . t \to t

$\top := \Pi t:*.\ t\rightarrow t$

\exists x : A . P (x) := Π t : * . (Π y : A . P (y) \to t) \to t

$\exists x:A.\ P(x):= \Pi t:*.\ (\Pi y: A.\ P(y)\rightarrow t)\rightarrow t$

(*, ◻)

$(*,\square)$

$*$ $*$ $(\square, *)$

$(\square,\square)$

Π c : * \to * . c n a t \to c n a t

$\Pi c:*\rightarrow *.\ \ c\ \mathrm{nat}\rightarrow c\ \mathrm{nat}$

$0=1$

= : n a t \to n a t \to *

$=\ :\ \mathrm{nat}\rightarrow\mathrm{nat}\rightarrow *$

= : Π t : * . t \to t \to *

$=\ :\ \Pi t:*.\ t\rightarrow t\rightarrow *$

n a t \to n a t \to *

$\mathrm{nat}\rightarrow\mathrm{nat}\rightarrow *$

(*, ◻)

$(*,\square)$

$\square \rightarrow \square$ $\square$ $\square$ $\square_i$ $i=1,2,3,\ldots$ $\square_i:\square_{i+1}$

$(\square_i, \square_i)$

\frac{Γ ⊢ A : ◻_{i}}{Γ ⊢ A : ◻_{j}} i \leq j

$\frac{\Gamma\vdash A:\square_i}{\Gamma\vdash A:\square_j}\ i\leq j$

Dzięki tym dodatkowym rodzajom i regułom otrzymujesz coś, co nie jest PTS, ale czymś bliskim. Jest to (prawie) rozszerzony rachunek konstrukcji , który jest bliższy podstawie Coq. Dużym brakującym elementem są typy indukcyjne, o których tutaj nie będę rozmawiać.

Edycja: Istnieje całkiem niezłe odniesienie, które opisuje różne funkcje języków programowania w ramach PTS, opisując PTS, który jest dobrym kandydatem do pośredniej reprezentacji funkcjonalnego języka programowania:

Henk: A Typed Intermediate Language , SP Jones i E. Meijer.

cody
źródło

Tematy zaawansowane w typach i językach programowania, S2.6 i S2.7 .

Kaveh

BTW „Rodziny typów” są często nazywane również typami wyższego rodzaju.

Martin Berger

PTS był dobrym pomysłem 20 lat temu, ale od tamtej pory wszystko się zmieniło.

Thorsten Altenkirch

@ThorstenAltenkirch nie ma potrzeby wykluczenia, Thorsten! Jest jeszcze kilka fajnych rzeczy do rozważenia z udziałem PTS, np. Przychodzi mi na myśl praca Bernardy nad zinternalizowaną parametrownością.

cody

@cody Żadne wykluczenie nie jest zamierzone, ale nie powinniśmy utknąć w przeszłości teorii typów składniowych. Praca Bernardi jest doskonała i można ją lepiej wykonać za pomocą wszechświatów.

Thorsten Altenkirch