Jedność parametryczna a parametryczność binarna

Ostatnio zainteresowałem się parametrownością po obejrzeniu artykułu LICS Bernardy'ego i Moulina z 2012 r. ( Https://dl.acm.org/citation.cfm?id=2359499 ). W tym artykule internalizują one jednoargumentową parametryczność w systemie czystego typu z typami zależnymi i podpowiadają, w jaki sposób można rozszerzyć konstrukcję na dowolne arie.

Wcześniej widziałem tylko parametr binarny. Moje pytanie brzmi: jaki jest przykład interesującego twierdzenia, które można udowodnić za pomocą binarnej parametryczności, ale nie jednoznacznej parametryczności? Byłoby również interesujące zobaczyć przykład twierdzenia możliwego do udowodnienia z trzeciorzędową parametrycznością, ale nie binarną (chociaż widziałem dowody, że n-parametryczność jest równoważna dla n> = 2: patrz http: //www.sato.kuis .kyoto-u.ac.jp / ~ takeuti / art / par-tlca.ps.gz )

Zazwyczaj używasz binarnej parametryczności, aby udowodnić równoważność programu. Jest to nienaturalne, gdy robi się to z jednolitym modelem, ponieważ mówi tylko o jednym programie na raz.

Zwykle używasz modelu jednoargumentowego, jeśli jedyne, co cię interesuje, to jedność. Na przykład zobacz nasz najnowszy szkic, Powierzchownie podstrukturalne typy , w którym udowadniamy wynik poprawności typu za pomocą modelu jednoargumentowego. Ponieważ solidność mówi o zachowaniu jednego programu (jeśli to albo się rozbiega, albo zmniejsza do wartości v : A ), wystarczy model jednoargumentowy. Jeśli chcielibyśmy dodatkowo udowodnić równoważność programów, potrzebowalibyśmy modelu binarnego.$e : A$$v : A$

EDYCJA: Właśnie zdałem sobie sprawę, że jeśli spojrzysz na nasz artykuł, to wygląda jak zwykły stary model relacji logicznych / wykonalności. Powinienem powiedzieć trochę więcej o tym, co czyni go (i innymi modelami) parametrycznym. Zasadniczo model jest parametryczny, gdy można udowodnić dla niego lemat przedłużenia tożsamości: to znaczy dla dowolnego wyrażenia typu, jeśli wszystkie zmienne typu swobodnego są powiązane ze stosunkami tożsamości, to wyrażenie typu jest stosunkiem tożsamości. Nie udowadniamy tego jawnie jako lematu (nie wiem dlaczego, ale rzadko robisz to, robiąc modele operacyjne), ale ta właściwość jest niezbędna dla poprawności naszego języka.

Definicja „relacji” i „relacji tożsamości” w parametryzacji jest w rzeczywistości trochę do uchwycenia, a ta swoboda jest tak naprawdę niezbędna, jeśli chcesz wspierać fantazyjne typy, takie jak typy wyższe lub typy zależne, lub chcesz pracować z bardziej wyszukanymi strukturami semantycznymi. Najbardziej dostępny opis tego, jaki znam, znajduje się w dokumencie roboczym Boba Atkeya Relacyjna parametryczność dla wyższych rodzajów .

Jeśli masz dobry apetyt na teorię kategorii, to Rosolini sformułował ją w sposób abstrakcyjny w swoim artykule Refleksyjne wykresy i polimorfizm parametryczny . Od tego czasu opracowali go dalej Dunphy i Reddy w swoim artykule Granice parametryczne , a także Birkedal, Møgelberg i Petersen w domenowych teoretycznych modelach polimorfizmu parametrycznego .

To powinien być komentarz do odpowiedzi Neela, ale jest trochę długi. Podpowiedzi Rasmusa Petersena znalazłem w pracy Møgelberga (podkreśl moje):

Ivar Rummelhoff [36] badał kodowanie liczb naturalnych w modelach na różnych PCA i wykazał, że w niektórych z tych modeli kodowanie zawiera więcej niż liczby naturalne. Dlatego te modele nie mogą być parametryczne. Mimo że o tym nie wspomina, pokazuje to, że parametryczność jednoargumentowa różni się od parametryczności binarnej (relacyjnej), ponieważ można łatwo wykazać, że kodowanie liczb naturalnych w dowolnym modelu jest jednoarametryczne.

Cytowany artykuł to Polynat w modelach PER .

$n$$n$$R$$(n+1)$$R'(\vec{x},y) \iff R(\vec{x}) \land y = x_i$$i \in [1..n]$$n$$n+1$$n+1$$n$. Ponieważ więcej relacji oznacza silniejszą parametryczność, a mniej rodzin funkcji można by uznać za „parametryczne”, rozumiemy, że „prawdziwa parametryczność” jest tym, co uzyskujemy w limicie, a każda parametryczność skończona jest jej przybliżeniem.

Te nieskończone stosunki sformalizowano jako „logiczne relacje Kripkego o różnej aromacie”, zwane również stosunkami Jung-Tiuryn. Jung i Tiuryn ​​wykazali, że taka nieskończona parametryczność jest wystarczająca do scharakteryzowania definiowalności lambda, a O'Hearn i Riecke wykazali , że wystarczy scharakteryzować w pełni abstrakcyjne modele dla języków programowania, w tym sekwencyjnego PCF. To fundamentalne i piękne wyniki!

Zatem jedność parametryczna jest najprostszym i najmniej wyrazistym przybliżeniem prawdziwej parametryczności, a parametryczność binarna staje się nieco lepsza. Twoje pytanie brzmi „o ile lepiej”? Mam wrażenie, że jest o wiele lepiej. Powodem jest to, że na poziomie jedności „relacja tożsamości” jest relacją prawdziwą, co niewiele znaczy. Na poziomie binarnym „relacja tożsamości” to równość. Nagle skaczesz w siłę parametryczności, przechodząc z poziomu jedności do poziomu binarnego. Następnie jest coraz bardziej udoskonalany.

Kurt Sieber dogłębnie przestudiował te kwestie: sekwencyjność i języki podobne do Algolu .

Prawdopodobnie najłatwiejszym do przeczytania tekstem dla zastosowań binarnej parametryczności są Twierdzenia Wadlera za darmo! .

Właściwie jestem nieco zaskoczony tym pytaniem, ponieważ parametryczność binarna jest najczęściej wymieniana w dokumentach parametrycznych. Nawet oryginalny artykuł Reynoldsa „Typy, abstrakcja i polimorfizm parametryczny” wspomina o tym wszędzie. Raczej jednoznaczna parametryczność nie jest powszechnie znana.