Zredukowanie produktów w HoTT do kodowania kościoła / Scotta

Więc idę z książką HoTT z niektórymi ludźmi. Stwierdziłem, że większość typów indukcyjnych, które zobaczymy, można zredukować do typów zawierających tylko zależne typy funkcji i wszechświaty, przyjmując typ rekurencji za inspirację dla typu równoważnego. Zacząłem szkicować, jak sądzę, że to zadziała i po pewnym potknięciu doszedłem do tego, co uważałem za odpowiedź.

\cdot \times \cdot \equiv \prod_{ZA, b, do : U} (ZA \to b \to do) \to do

$\cdot \times \cdot \equiv \prod_{A, B, C : \mathcal{U}} (A \to B \to C) \to C$

(\cdot, \cdot) \equiv λ za : ZA . λ b : b . λ do : U . λ sol : ZA \to b \to do . sol (za) (b)

$(\cdot, \cdot) \equiv \lambda a : A. \lambda b : B. \lambda C : \mathcal{U}. \lambda g : A \to B \to C. g(a)(b)$

ja n {re}_{ZA \times b} \equiv λ do . λ sol . λ p . sol (p r_{1} (p)) (p r_{2)} (p))

$ind_{A \times B} \equiv \lambda C. \lambda g. \lambda p. g(pr_1(p))(pr_2(p))$

To daje poprawnych równań definiujących (definiowanie równań dla i pominięte), ale oznaczałoby to, że musiałby niewłaściwy typ. $pr_1$ $pr_2$ $ind_{A \times B}$

{ind}_{ZA \times b} : \prod_{do : ZA \times b \to U} (\prod_{za : ZA} \prod_{b : b} do ((za, b))) \to \prod_{p : ZA \times b} do ((p r_{1} (p), p r_{2)} (p)))

$\text{ind}_{A \times B} : \prod_{C : A \times B \to \mathcal{U}} (\prod_{a:A} \prod_{b:B} C((a, b))) \to \prod_{p : A \times B} C((pr_1(p), pr_2(p)))$

I wydaje się, że nie ma prostej naprawy tego. Pomyślałem również o następującej definicji.

ja n {re}_{ZA \times b} \equiv λ do . λ sol . λ p . p (do (p)) (sol)

$ind_{A \times B} \equiv \lambda C. \lambda g. \lambda p. p(C(p))(g)$

Ale to po prostu nie sprawdza typu.

Innym pomysłem było użycie $uniq_{A \times B}$ do konwersji $C((pr_1(p), pr_2(p)))$ do $C(p)$ ale nie jest jasne, jak to zrobić. Po pierwsze musiałbym pokazać, jak zmniejszyć typy funkcji zależne od typów tożsamości, co okazuje się jeszcze trudniejsze w moich bazgrołach niż w produktach. Dodatkowo $uniq_{A \times B}$ nie wydaje się być do zdefiniowania bez odpowiedniej formy indukcji, więc nawet gdybym pozwolił sobie na typy tożsamości przedstawione w książce, nie byłbym bliżej posiadania definicji $uniq_{A \times B}$

Wygląda więc na to, że możemy zdefiniować tutaj rekursor, ale nie cewkę indukcyjną. Możemy zdefiniować coś, co bardzo przypomina wygląd induktora, ale nie do końca to robi. Rekurencja pozwala nam wykonywać logikę, przyjmując ten typ za sens logicznej koniunkcji, ale nie pozwala nam udowodnić rzeczy o produktach, które wydają się brakować.

Czy możemy zrobić coś, co, jak twierdziłem, może być dokonane? To znaczy, czy możemy zdefiniować typ przy użyciu tylko zależnych typów funkcji i wszechświatów, które mają funkcję parowania i cewkę z tymi samymi równaniami definiującymi i typami jak produkty? To moje rosnące podejrzenie, że złożyłem fałszywe roszczenie. Wygląda na to, że jesteśmy w stanie być tak frustrująco blisko, ale po prostu nie do końca. Jeśli nie możemy tego zdefiniować, jaki argument wyjaśnia, dlaczego nie możemy? Czy produkty przedstawione w książce HoTT zwiększają wytrzymałość systemu?

— Jake
źródło

O ile rozumiem, zwykłe kodowanie Kościoła daje nam typ, który dopuszcza eliminację niezależną (rekursor), ale eliminację niezależną (induktor). Twoje pytanie może być związane z tym pytaniem . Nie jestem pewien, czy HoTT coś zmieni w tej sprawie.

— chi

To wydaje się pomocne. Jak rozumiem, na moje pytanie można odpowiedzieć dla rachunku predykcyjnego typów konstrukcji (Coq minus (co) indukcyjne). Szukałem artykułów, które pasują do tych modeli (modele CoC, które nie są modelami CiC), ale nie mogę ich znaleźć. Czy przypadkiem masz źródło?

— Jake,

Niestety nie mam odniesienia do udostępnienia. Byłbym także zainteresowany posiadaniem źródła, na które mógłbym zacytować ten fakt folklorystyczny.

— chi

Ciągle znajduję też odniesienia do tego folkloru, ale nie mogę znaleźć wytłumaczenia.

— Jake,

Ładne pytanie, ale czy nie pasowałoby lepiej na cstheory.stackexchange.com

— Martin Berger

Standardowe odniesienie, które często podam, to: Indukcji nie można uzyskać w teorii typów zależnych od drugiego rzędu autorstwa Hermana Geuversa, która mówi, że nie ma żadnego typu

N. : T. y p mi

$N : \mathrm{Type}$

z funkcjami

Z : N. S. : N. \to N.

$Z:N\qquad S:N\rightarrow N$

takie, że

ja n re : Π P. : N. \to T. y p mi . P. Z \to (Π m : N. . P. m \to P. (S. m)) \to Π n : N. . P. n

$\mathrm{ind}:\Pi P:N\rightarrow \mathrm{Type}.P\ Z\rightarrow (\Pi m:N.P\ m\rightarrow P\ (S\ m))\rightarrow \Pi n:N. P\ n$

jest możliwe do udowodnienia. To sugeruje, że w rzeczywistości takie kodowanie nie może działać dla par, które opisujesz.

Sprawdzony system jest podzbiorem rachunku konstrukcji, który zawiera potężne typy produktów i wszechświat. Podejrzewam, że ten wynik można rozszerzyć na system, który Cię interesuje, w zależności od tego, co masz.

Niestety nie znam pełnej odpowiedzi na twoje pytanie. Podejrzewam, że dodanie pewnych zasad parametrycznych „wewnętrznie” jest dokładnie tym, co jest wymagane, aby te kodowania działały z zasadą pełnej indukcji. Neel Krishnaswami, którego wiedza jest moim ścisłym nadzorem, napisał artykuł z Derekiem Dreyerem:

Internalizacja parametrów relacyjnych w rachunku ekstensywnym konstrukcji

Interesujący jest również następujący artykuł Bernardy, Jansson i Patterson (Bernardy głęboko zastanowił się nad tymi tematami):

Typowość i typy zależne

Oczywiście parametryczność ma ścisły związek z HoTT w ogóle, ale nie wiem, jakie są szczegóły. Myślę, że Steve Awodey rozważył te pytania, ponieważ sztuczka z kodowaniem jest przydatna w kontekstach, w których tak naprawdę nie wiemy, jak powinny wyglądać eliminatory.

— cody
źródło

Aby zrealizować swój pomysł, potrzebujesz czegoś dodatkowego, jak wskazano w odpowiedzi na @ cody. Sam Speight pracował pod nadzorem Steve'a Awodeya, aby zobaczyć, co można osiągnąć w HoTT za pomocą impredicative wszechświata, patrz Impredicative Encodings of Inductive Types w poście na blogu HoTT .

— Andrej Bauer
źródło