Czy kolejność deklaracji typu indukcyjnego ma znaczenie?

9

Zastanawiałem się, czy kolejność deklaracji typu indukcyjnego może mieć znaczenie.

Na przykład w Coq możesz zdefiniować Nat:

Inductive Nat :=
  | O : Nat
  | S : Nat -> Nat.

lub

Inductive Nat :=
  | S : Nat -> Nat
  | O : Nat.

Być może zmieni to kolejność parametrów w automatycznie generowanym eliminatorze, ale to nie jest wielka sprawa.

Zastanawiam się, czy można napisać taką deklarację

Inductive typewhereordermatters :=
  | cons1 : type1
  | cons2 : type2.

gdzie type2jest zależny typ, w zależności od cons1? (w tym przypadku napisanie deklaracji w innej kolejności nie miałoby żadnego znaczenia, ponieważ type2odnosi się do cons1tego, o czym jeszcze nie ma).

lo.logic type-theory coq dependent-type Guillaume Brunerie
źródło

Odpowiedzi:

10

  1. Kolejność nie ma znaczenia. Nie mogę wymyślić przypadku, w którym by to zrobił. Jak zauważa Andrej Bauer w komentarzu, zmiana kolejności powoduje, że wynik jest kanonicznie izomorficzny do oryginału .

  2. Jedna sprawa nie może zależeć od innej sprawy. Elementy sumy reprezentują wybór, więc nie ma sensu, aby wybrany wybór zależał od wyboru, który nie został podjęty.

Dave Clarke
źródło
2
Możesz sprecyzować swój pierwszy punkt. Kolejność nie ma znaczenia. Jeśli zmienisz kolejność, wynik będzie kanonicznie izomorficzny w stosunku do oryginału.
Andrej Bauer
2
@Dave: Dzięki! Zadawałem to pytanie z powodu (wysoce eksperymentalnej teorii) wyższych typów indukcyjnych, w których wydaje się , że zjawiska te zdarzają się , i chciałem wiedzieć, czy może tak być w przypadku zwykłych typów indukcyjnych.
Guillaume Brunerie
1
@Guillaume: Nie jestem pewien, na jakie zjawisko wskazujesz za pomocą linku. Różne klauzule konstruktorów definicji typu danych nie mogą zależeć od siebie, niezależnie od tego, czy jest to typ danych wyższego rzędu, czy nie. Być może myślisz o rekordach zależnych (które są używane pod linkiem i są dostępne w Agdzie i Coq )?
Noam Zeilberger
1
@Noam W przykładzie wyższej typu indukcyjnego circle, typu z loopkonstruktora zależy od basekonstruktora.
Guillaume Brunerie
2
@Gillailla: Widzę teraz (wprowadzają eksperymentalną składnię), nie wiem, jak mi tego brakowało.
Noam Zeilberger
6

Czy zamówienie ma znaczenie tak, jak pytasz? Nie.

Ale czy kolejność jest całkowicie nieistotna dla funkcjonowania asystenta dowodu? Znowu nie. W Maticie, asystencie sprawdzającym bardzo podobnym do Coq, kolejność, w jakiej konstruktory są zapisywane w definicji indukcyjnej, ma znaczenie dla sprawdzania typu, szczególnie podczas sprawdzania typu wyrażenia dopasowania.

Matita musi najpierw sprawdzić, czy wszystkie konstruktory są dopasowane w treści meczu. Odbywa się to poprzez przełączanie konstruktorów w kolejności, w jakiej zostały zadeklarowane. Następnie przychodzi sprawdzenie typu właściwego wyrażenia dopasowania, co dzieje się w odwrotnej kolejności, najpierw sprawdzając wielkość liter dla ostatniego zadeklarowanego konstruktora. Ten typ jest następnie przeprowadzany i wykorzystywany do sprawdzania innych przypadków.

To bardzo często pojawia się podczas pisania wyrażenia o dużym dopasowaniu. Najpierw chcesz wypełnić proste sprawy, pozostawiając trudniejsze sprawy pod znakiem wieloznacznym, okresowo sprawdzaj, co napisałeś, aby upewnić się, że ma to sens. Czasami Matita nie jest w stanie wywnioskować typu niepełnego wyrażenia dopasowania, ale całkiem chętnie to zrobi, jeśli wypełnisz przypadek ostatniego konstruktora zdefiniowanego w typie indukcyjnym.

Zakładam, choć nie jestem pewien, że Coq robi coś podobnego.

Dominic Mulligan
źródło