„Chronione” negatywne zdarzenia w definicji typów indukcyjnych, zawsze złe?

Wiem, jak niektóre negatywne zdarzenia mogą być zdecydowanie złe:

data False

data Bad a = C (Bad a -> a)

selfApp :: Bad a -> a
selfApp (x@(C x')) = x' x

yc :: (a -> a) -> a
yc f = selfApp $ C (\x -> f (selfApp x))

false :: False
false = yc id

Nie jestem jednak pewien, czy:

• wszystkie typy indukcyjne z negatywnymi zdarzeniami mogą okazać się błędne;

• jeśli tak, istnieje znany mechaniczny sposób;

Na przykład walczyłem, próbując sprawić, że ten typ się nie powiedzie:

type Not a = a -> False

data Bad2 a = C2 (Bad2 (Not a) -> a)

Doceniamy każdy wskaźnik do literatury na ten temat.

Powód zakazu negatywnych zdarzeń można zrozumieć analogicznie do twierdzenia Knastera-Tarskiego. To twierdzenie tak mówi

jeśli jest kompletną siecią, a jest funkcją monotoniczną na , to zbiór stałych punktów jest również kompletną siecią. W szczególności istnieje najmniej stały punkt i największy stały punkt .f : L → L L f μ f ν $L$$f : L \to L$$L$$f$$\mu{f}$$\nu f$

W tradycyjnej teorii modeli sieci można postrzegać jako zdania, a relację rzędu można rozumieć jako uwikłanie (tj. Że prawdą jest prawdę ).p ≤ q q $L$$p \leq q$$q$$p$

Kiedy przechodzimy od teorii modelu do teorii dowodu, sieci uogólniają się na kategorie. Typy mogą być postrzegane jako obiekty o kategorii i mapy oznacza dowód , że może pochodzić z . e : P → Q Q $\mathbb{C}$$e : P \to Q$$Q$$Q$

Kiedy próbujemy interpretować typy zdefiniowane przez równania rekurencyjne, ee, , oczywistą rzeczą do zrobienia jest poszukiwanie uogólnienia twierdzenia Knastera-Tarskiego. Więc zamiast funkcji monotonicznej na sieci wiemy, że chcemy funktora , który wysyła obiekty do obiektów, ale uogólnia warunek monotoniczności, tak że każda mapa otrzymuje mapę (z warunkami koherencji, że wysyła tożsamości do tożsamości i zachowuje kompozycje, tak że ).$\mathbb{N} = \mu \alpha.\;1 + \alpha$ $F : \mathbb{C} \to \mathbb{C}$$e : P \to Q$$F(e) : F(P) \to F(Q)$$F$$F(g \circ f) = F(g) \circ F(f)$

Jeśli więc chcesz indukcyjnego typu danych , musisz także podać akcję funkcjonalną na warunkach dla operatora typu , aby mieć pewność, że żądany punkt istnieje. Surowy warunek dodatni w Agdzie i Coq jest warunkiem składniowym , który implikuje to ograniczenie semantyczne . Mówiąc luźniej, mówi, że jeśli zbudujesz operator typu na podstawie sum i produktów, zawsze możesz przygotować akcję funcjonalną, a zatem każdy typ utworzony w ten sposób powinien mieć ustalony punkt.$\mu \alpha.\;F(\alpha)$$F$

W językach o typie zależnym masz również typy indeksowane i parametryzowane, więc Twoje prawdziwe zadanie jest bardziej skomplikowane. Bob Atkey (który pisał o tym tutaj i tutaj ) mówi mi, że dobrym miejscem do znalezienia tej historii jest:

• Indukcja strukturalna i koindukcja w warunkach fibracyjnych , Claudio Hermida i Bart Jacobs 1997.
• Reguły indukcji fibracyjnej dla początkowych algebr , Neil Ghani, Patricia Johann i Clement Fumex 2010.

Jak zauważa Andrej, zasadniczo to, czy zdarzenie negatywne jest w porządku, czy nie, zależy od tego, jaki jest twój model teorii typów. Zasadniczo, kiedy masz definicję rekurencyjną, szukasz punktu stałego i istnieje wiele twierdzeń o punkcie stałym w matematyce.

Jednym z nich, z którego osobiście korzystałem, jest twierdzenie Banacha o punkcie stałym, które mówi, że jeśli masz ściśle skurczową funkcję w przestrzeni metrycznej, to ma ona unikalny punkt stały. Pomysł ten został wprowadzony do semantyki przez (IIRC) Maurice'a Nivata i był intensywnie badany przez Amerykę i Rutten, a niedawno został połączony przez Birkedala i jego współpracowników z popularną techniką operacyjną zwaną „indeksowaniem kroków”.

• Rozwiązywanie równań domen refleksyjnych w kategorii kompletnych przestrzeni metrycznych , Pierre America i Jan JMM Rutten 1989.
• Teoretyczne rozwiązanie rekurencyjnych równań metryczno-przestrzennych , Lars Birkedal, Kristian Støvring i Jacob Thamsborg. 2010 r.

Daje to początek teoriom typów, w których dozwolone są negatywne zdarzenia w typach rekurencyjnych, ale tylko wtedy, gdy negatywne zdarzenia występują pod specjalnym konstruktorem typu „ochrona”. Pomysł ten wprowadził Hiroshi Nakano, a związek z twierdzeniem Banacha został zrobiony zarówno przeze mnie, jak i przez Nicka Bentona, a także przez Larsa Birkedala i jego współautorów.

• A Modality for Recursion , Hiroshi Nakano, 2000.
• Ultrametryczna semantyka programów reaktywnych , Nick Benton i Neel Krishnaswami, 2011.
• Metryczny model strzeżonej rekurencji , Lars Birkedal, Jan Schwinghammer i Kristian Støvring, 2010.

Czasami możesz rozwiązać rekurencyjne równania „na szczęście”.

Zakładam, że chcesz to zrobić w zestawach (w przeciwieństwie do jakiejś teorii domen) Jeśli rozwiniemy twoją definicję i zapiszemy równanie bezpośrednio bez adnotacji Haskella, otrzymamy Rozważmy dwa przypadki:

$$A \cong (A \to \emptyset) \to A.$$

1. Jeśli jest zamieszkały, tzn. Zawiera coś, to , dlatego równanie zmniejsza się do I rzeczywiście, singleton set rozwiązuje równanie.$A$$A \to \emptyset \cong \emptyset$

   $$A \cong \emptyset \to A \cong 1.$$ $1$

2. Jeśli jest puste, otrzymujemy .$A$$\emptyset \cong (\emptyset \to \emptyset) \to \emptyset \cong 1 \to \emptyset \cong \emptyset$

Wniosek: istnieją dwa rozwiązania, pusty typ (który nazwałeś False) i typ urządzenia ().

Oto kolejny interesujący przykład: lub w Haskell

$$A \cong (A \to 2) \to 2,$$

data Cow a = Moo ((a -> Bool) -> Bool)

Pod względem zestawów jest to . Według twierdzenia Cantora nie ma rozwiązania, ponieważ ma mniej elementów niż . Jeśli jednak przyjrzymy się temu równaniu w przestrzeniach topologicznych, istnieje rozwiązanie, a mianowicie Dzieje się tak dlatego, że to przestrzeń Cantora, to przestrzeń jej podzbiorów clopen, których jest niezliczona liczba (i trzeba to zobaczyć tworzą dyskretną przestrzeń). Podobnie możesz wykazać bijection pomiędzy i w Haskell.$A \cong 2^{2^A}$$A$$2^{2^A}$

$$\mathbb{N} \cong 2^{2^\mathbb{N}}.$$ $2^\mathbb{N}$$2^{2^\mathbb{N}}$Integer(Integer -> Bool) -> Bool

Trudno jest coś dodać do wyjaśnień Andreja lub Neela, ale dam temu szansę. Spróbuję zająć się syntaktycznym punktem widzenia, zamiast próbować odkryć leżącą u podstaw semantykę, ponieważ wyjaśnienie jest bardziej elementarne i udzielę bardziej prostej odpowiedzi na twoje pytanie.

Zamierzam pracować w prostym typie -calculus zamiast w bardziej złożonym systemie leżącym u podstaw Haskell. Uważam w szczególności, że obecność zmiennych typu może do pewnego stopnia dezorientować.$\lambda$

Najważniejsze odniesienie jest następujące:

Mendler, N. (1991). Typy indukcyjne i ograniczenia typów w rachunku lambda drugiego rzędu. Obawiam się, że nie znalazłem referencji online. Stwierdzenia i dowody można jednak znaleźć w rozprawie doktorskiej Naxa (wysoce zalecana lektura!).

Mendler wyjaśnia, że ​​pozytywność jest koniecznym i wystarczającym warunkiem zakończenia w przypadku nierekurencyjnych definicji przypadków (i strukturalnie malejących definicji rekurencyjnych). Stwierdza to za pomocą równania równania . Podaję prosty przykład, który jest uproszczeniem typu .$\mathrm{Bad}$

$$\mathrm{Bad} = \mathrm{Bad}\rightarrow A$$

Gdzie jest dowolnym typem. Mamy wtedy$A$

$$\lambda x:\mathrm{Bad}.x\ x: \mathrm{Bad}\rightarrow A$$

a więc

$$(\lambda x:\mathrm{Bad}.x\ x)\ (\lambda x:\mathrm{Bad}.x\ x): A$$

Mendler pokazuje, że można tego dokonać dla dowolnego typu gdzie jest typem z co najmniej jednym ujemnym wystąpieniem (mogą również występować pozytywne) . Podaje wyraźny termin, który nie kończy się dla danego (strony 39-40 jego pracy).

$$\mathrm{Bad} = F(\mathrm{Bad})$$ $F(X)$$X$$F(X)$

Oczywiście nie pracujesz z typami równymi zdefiniowanymi, ale z konstruktorami , tzn. Masz

data Bad = Pack (Bad -> A)

zamiast ścisłej równości. Jednak możesz to zdefiniować

unpack :: Bad -> (Bad -> A)
unpack (Pack f) = f

co jest wystarczające do utrzymania tego wyniku:

 (\x:Bad -> unpack x x) (Pack (\x:Bad -> unpack x x))

Termin ten jest nadal dobrze wpisane typu .$A$

---

W drugim przykładzie sprawy są nieco trudniejsze, ponieważ masz coś podobnego do

$$\mathrm{Bad} = \mathrm{Bad}' \rightarrow A$$

gdzie jest powiązany , ale nie równy, z (w twoim przypadku są one równe i odpowiednio). Przyznaję, że nie mogłem zbudować prostego izomorfizmu między nimi. Ten sam problem występuje, jeśli go wymieniszB d B d B d ( N O T$\mathrm{Bad}'$$\mathrm{Bad}$$\mathrm{Bad}\ a$$\mathrm{Bad}\ (\mathrm{Not}\ a)$

type Not a = a -> False

z

data Not a = Not a

Łatwo byłoby to rozwiązać, gdyby Haskell zezwolił na takie definicje typów:

type Acc = Not Acc

W takim przypadku można zbudować kombinator pętli w dokładnie taki sam sposób jak poprzednio. Podejrzewam, że możesz nosić podobną (ale bardziej złożoną) konstrukcję

data Acc = D (Not Acc)

Problem polega na tym, że zbudować izomorfizm

Bad Acc <-> Bad (Not Acc)

masz do czynienia z wariancją mieszaną.