Jak pokazać, że typ w systemie z typami zależnymi nie jest zamieszkały (tj. Formuła nie do udowodnienia)?

W przypadku systemów bez typów zależnych, takich jak system typu Hindley-Milner, typy odpowiadają formułom logiki intuicyjnej. Nie wiemy, że modele algebrami Heytinga, a w szczególności do zbicia wzór, można ograniczyć do jednego Heytinga Algebra gdzie każdy wzór jest reprezentowany przez otwarte podzestawu .$\mathbb{R}$

Na przykład, jeśli chcemy pokazać, że nie jest zamieszkały, konstruujemy odwzorowanie ϕ ze wzorów na otwarte podzbiory R , definiując: ϕ ( α $\forall\alpha.\alpha\lor(\alpha\rightarrow\bot)$$\phi$$\mathbb{R}$ Następnie ϕ ( α → ⊥

$$\begin{align} \phi(\alpha) &= (-\infty, 0) \end{align}$$ To pokazuje, że oryginalnej formuły nie da się udowodnić, ponieważ mamy model, w którym nie jest to prawda, lub równoważnie (według izomorfizmu Curry'ego-Howarda) tego typu nie można zamieszkać. $$\begin{align} \phi(\alpha\rightarrow\bot) &= \mbox{int}( [0, \infty) ) \\ & = (0,\infty) \\ \phi(\alpha\lor(\alpha\rightarrow\bot)) &= (-\infty, 0) \cup (0,\infty) \\ &= \mathbb{R} \setminus {0}. \end{align}$$

Inną możliwością byłoby użycie ramek Kriepke .

---

Czy istnieją podobne metody dla systemów z typami zależnymi? Jak jakieś uogólnienie algeb Heytinga lub ramek Kripke?

Uwaga: nie proszę o procedurę decyzyjną, wiem, że nie może być żadnej. Proszę tylko o mechanizm, który pozwala być świadkiem niewiarygodności formuły - przekonać kogoś, że jest to nie do udowodnienia.

To, że formuła jest nie do udowodnienia, można zasadniczo zrobić na dwa sposoby. Przy odrobinie szczęścia możemy być w stanie wykazać w ramach teorii typów, że formuła implikuje taką, o której wiadomo, że jest nie do udowodnienia. Innym sposobem jest znalezienie modelu, w którym formuła jest nieprawidłowa, co może być dość trudne. Na przykład zajęło bardzo dużo czasu znalezienie modelu grupoidowej teorii typów zależnych, który jako pierwszy unieważnił unikalność dowodów tożsamości .

Pytanie „jaki jest model teorii typów zależnych?” ma dość skomplikowaną odpowiedź. Jeśli zignorujesz pewne właściwości podstawienia, model jest lokalnie kartezjańską kategorią zamkniętą i może to być najprostsza odpowiedź. Jeśli chcesz mieć „prawdziwy” model, istnieje kilka opcji, zobacz stronę nLab na kategorycznych modelach teorii typów zależnych . W każdym razie odpowiedź jest zawsze nieco skomplikowana, ponieważ teoria typów zależnych jest dość złożonym systemem formalnym.

Gdybym zaproponował tylko jeden artykuł na ten temat, prawdopodobnie poleciłbym oryginalny artykuł Roberta Seely'ego „Lokalnie kartezjańskie zamknięte kategorie i teoria typów” . Gdybym miał zasugerować inną, prawdopodobnie byłaby to ta, która wyjaśnia, co należy poprawić w pracy Seely, np. Martina Hoffmana „O interpretacji teorii typów w lokalnie kartezjańskich kategoriach zamkniętych” .

Ostatnim ważnym postępem w tej dziedzinie jest uświadomienie, że modele teoretyczne homotopii są również modelami teorii typów zależnych, patrz odniesienia do homotopytypetheory.org . Daje to bogactwo możliwości, ale należy teraz nauczyć się teorii homotopii, aby zdobyć modele.