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?

— 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

Kanonicznym odniesieniem do tego jest Peter Dybjer, Inductive Families , który zapewnia dość kompleksowe leczenie rodzin indukcyjnych opartych na eliminatorach.

— cody
źródło

Możesz znaleźć niektóre z naszych ostatnich artykułów na ten temat, ponieważ wyprowadzamy eliminatory dla typów danych zakodowanych w lambda. Na przykład, zobacz ten jeden dla rodzajowego wyprowadzenia eliminatory, a to jeden z podstawowych techniki stosowane tylko do Nat typu.

— Aaron Stump
źródło