Eliminacje parametryczne i projekcyjne dla rekordów zależnych

A \times B ≜ \forall α . (A \to B \to α) \to α

$A \times B \triangleq \forall\alpha.\; (A \to B \to \alpha) \to \alpha$

π_{1} : A \times B \to A

$\pi_1 : A \times B \to A$

π_{2} : A \times B \to B

$\pi_2 : A \times B \to B$

Nie jest to tak zaskakujące, nawet jeśli naturalny odczyt typu F jest parą z eliminacją stylu let $\mathsf{let}\;(x,y) = p \;\mathsf{in}\; e$ , ponieważ te dwa rodzaje par można przenikać w intuicyjnej logice.

Teraz, w teorii typów zależnych z impredykatywną kwantyfikacją, możesz zastosować ten sam wzór, aby zakodować zależny typ rekordu $\Sigma x:A.\; B[x]$ as

Σ x : A . B [x] ≜ \forall α . (Π x : A . B [x] \to α) \to α

$\Sigma x:A.\;B[x] \triangleq \forall\alpha.\; (\Pi x:A.\; B[x] \to \alpha) \to \alpha$ Ale w tym przypadku nie ma prostego sposobu zdefiniowania eliminatorów rzutowych

π_{1} : Σ x : A . B [x] \to A

$\pi_1 : \Sigma x:A.\;B[x] \to A$ i

π_{2} : Π p : (Σ x : A . B [x]) . B [π_{1} p]

$\pi_2 : \Pi p:(\Sigma x:A.\;B[x]).\; B[\pi_1\,p]$ .

Jeśli jednak teoria typów jest parametryczna, możesz użyć parametryczności, aby pokazać, że $\pi_2$ jest definiowalny. Wydaje się, że jest to znane - patrz, na przykład, opracowanie Agdy autorstwa Dana Doela, w którym wyprowadza to bez komentarza --- ale nie mogę znaleźć odniesienia do tego faktu.

Czy ktoś zna odniesienie do faktu, że parametryczność pozwala na zdefiniowanie eliminacji rzutowych dla typów zależnych?

EDYCJA: Najbliższą rzeczą, jaką do tej pory znalazłem, jest ten artykuł Hermana Geuversa z 2001 roku. Indukcji nie można uzyskać w teorii typów zależnych od drugiego rzędu , w której dowodzi on, że nie można tego zrobić bez parametryczności.

— Neel Krishnaswami
źródło

Nie mogę powiedzieć z tego postu, jakie jest pytanie. (Nic nie wiem o okolicy i i tak nie wiedziałbym, ale chciałbym móc sformułować pytanie)

— Vijay D

Dodałem wyraźną linię pytań nad edycją. czy to pomaga?

— Neel Krishnaswami,

Tak. Po prostu początkowo nie byłem pewien, czy to tylko prośba o referencję, czy prośba o dowód. Zapytam się

— Vijay D

Kilka miesięcy temu miałem dyskusję tutaj: queuea9.wordpress.com/2012/03/28/why-not-lambda-encode-data i uważam, że parametrarność-> zasada eliminacji to folklor / oryginalne dzieło Dana. Dyskusje te są zbliżone do innych dotyczących parametryczności J.-P. Bernardi. Możesz przyjrzeć się standardowym zmianom biblioteki Coq wokół sum zależnych: coq.inria.fr/stdlib/Coq.Init.Specif.html i może coq.inria.fr/stdlib/Coq.Logic.EqdepFacts.html#

— cody

@kvb: Nie sądzę, aby była jakaś pozytywna odpowiedź. W moim ostatnim szkicu (z Derekiem Dreyerem) na temat parametryczności w rachunku konstrukcji ( mpi-sws.org/~neelk/internalizing-parametricity.pdf ) pokazujemy, że parametricity sprawia, że dźwięk , aby dodać aksjomaty, które pozwalają uzyskać mocne elims się kodowania Kościoła. Jednak nie mamy jeszcze dobrej historii, jak internalizować parametryczność w sposób, który dobrze się oblicza (najprawdopodobniej musimy zintegrować metody JP Bernardy z naszą teorią typów). Nie wydaje się to niemożliwe, ale nie wiemy jeszcze, jak to zrobić.

— Neel Krishnaswami,

Właśnie rozmawiałem z Danem Doelem, który wyjaśnił, że jego referencją był w rzeczywistości jeden Neel Krishnaswami. Zobaczył twój komentarz do n-kawiarni, że można wykonać silną indukcję za pomocą parametryczności, więc poszedł do przodu i zrobił to jako ćwiczenie, nie zdając sobie sprawy, że robienie tego dla sigmy było najwyraźniej nowym rezultatem.

Dokładny cytat: „Odniosłem się do niego. Myślałem, że powiedział, że to możliwe, więc to zrobiłem”.

— sclv
źródło