Jak uzyskać eliminatory o typie zależnym?

W programowaniu zależnym są dwa główne sposoby dekompozycji danych i wykonania rekurencji:

Zależne dopasowanie wzorca : definicje funkcji podano w postaci wielu klauzul. Ujednolicenie zapewnia, że wszystkie pominięte przypadki są niemożliwe, a zewnętrzny solver zapewnia, że rekurencja jest uzasadniona.
Eliminatory : Każda indukcyjnego typu danych posiada powiązaną stałej , który działa jako zasady indukcji jak i funkcji rekurencyjnej rozkładającym wartości typu . Są to bardziej szczegółowe, ale mają tę zaletę, że są całkowite (wszystkie przypadki są objęte ) i kończą się budową. $D$ $E_D$ $D$ $E_D$

Widziałem eliminatory dla typowych typów danych, takich jak , gdzie eliminator jest w zasadzie indukcją matematyczną, lub , gdzie eliminator jest po prostu fałdem. $Nat$ $List$

Czytałem kilka artykułów na temat zależnego dopasowywania wzorców, a wiele odnosi się do teorii typów, w których typy danych mogą być definiowane, a teoria zapewnia eliminatory. Na przykład, Wyeliminowanie Dependent Pattern Recognition opisano sposób UTT opiera się eliminator i dopasowywania wzorców może być przekształcany do eliminacji w obecności aksjomatyce . Rozumiem, że po zdefiniowaniu typu danych teoria zapewnia eliminator. $K$

To, czego nie znalazłem (a przynajmniej nie rozpoznałem, jeśli go widziałem), to dobry opis tego, jak można uzyskać eliminatory, zarówno ich typy, jak i ich semantykę.

Czy ktoś może wskazać mi odniesienie, które opisuje, w jaki sposób można uzyskać eliminator z definicji typu danych?

reference-request recursion type-theory dependent-types inductive-datatypes jmite
źródło

Jestem pewien, że w rachunku konstrukcji lub literaturze Coq znajduje się opis (dla typów ściśle pozytywnych - eliminatory Coqa na bardziej złożonych typach nie są w pełni ogólne).

Gilles 'SO - przestań być zły'

@Gilles Rozumiałem, że Coq nie używał eliminatorów, ale zamiast tego używa osobnych operatorów dopasowania i (strzeżonych).

jmite

Podstawowy język nie używa eliminatorów, ale kiedy zdefiniujesz typ, Coq generuje eliminator, który jest zdefiniowany w kategoriach fixi match. Nie mam pod ręką referencji, ale wiem, że przeczytałem coś o tym, jak generowany jest ten eliminator. cs.stackexchange.com/questions/104/... może być interesujące.

Gilles „SO- przestań być zły”

Dla każdego typu indukcyjnego TCoq definiuje zasadę indukcji, T_indktóra jest zależnym eliminatorem. Jest to zdefiniowane w kategoriach rekurencji i dopasowywania wzorców, ale można w zasadzie założyć, że jest to nowa stała o tym samym typie (z tą samą semantyką).

chi

Jak uzyskać eliminatory o typie zależnym?

Odpowiedzi: