Intuicja za ścisłą pozytywnością?

Zastanawiam się, czy ktoś może dać mi intuicję, dlaczego ścisła pozytywność indukcyjnych typów danych gwarantuje silną normalizację.

Dla jasności widzę, jak negatywne zdarzenia prowadzą do rozbieżności, tj. Poprzez zdefiniowanie:

data X where Intro : (X->X) -> X

możemy napisać rozbieżną funkcję.

Zastanawiam się jednak, jak możemy udowodnić, że ściśle pozytywne typy indukcyjne nie pozwalają na rozbieżność? tzn. czy istnieje jakaś miara indukcji, która pozwala nam skonstruować dowód silnej normalizacji (przy użyciu relacji logicznych lub podobnych)? A gdzie taki dowód rozkłada się na negatywne zdarzenia? Czy istnieją jakieś dobre referencje, które wykazują silną normalizację dla języka z typami indukcyjnymi?

Wygląda na to, że potrzebujesz przeglądu argumentów normalizacyjnych dla systemów typów z dodatnimi typami danych. Poleciłbym rozprawę doktorską Nax Mendler: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html .

Jak sugeruje data, jest to dość klasyczna praca. Podstawową intuicją jest to, że porządkowa $\lambda$ może być powiązana z dowolnym elementem dodatniego typu indukcyjnego, np. Dla typu danych

Inductive Ord = Zero : Ord | Suc : Ord -> Ord | Lim : (Nat -> Ord) -> Ord

Dostalibyśmy:

gdzie rozciąga się na terminy z normalnymi formami. Zastrzeżenie polega na tym, że ta interpretacja jest zdefiniowana tylko w 3. przypadku, gdy ma również postać normalną, co wymaga pewnej ostrożności w definicjach.$n$$f\ n$

Następnie można zdefiniować funkcje rekurencyjne przez indukcję nad tym porządkiem.

Należy zauważyć, że te typy danych można zdefiniować już w klasycznej teorii zbiorów, jak wskazano w znakomitym dokumencie Inductive Families autorstwa Dybjer ( http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf ). Ponieważ jednak przestrzenie funkcji są tak ogromne, typy takie Ordwymagają do interpretacji naprawdę dużych rzędnych.

Innym dobrym źródłem wychodzenia poza ściśle pozytywne typy jest praca doktorska Ralpha Matthesa: http://d-nb.info/956895891

Omawia rozszerzenia Systemu F z (ściśle) pozytywnymi typami w rozdziale 3 i dowodzi wielu silnych wyników normalizacji w rozdziale 9. Istnieje kilka interesujących pomysłów omówionych w rozdziale 3.

1. Możemy dodać najmniej ustalone punkty dla dowolnego typu z dowolną zmienną , o ile możemy dostarczyć monotoniczności świadka . Ten pomysł jest już obecny w pracy Mendlera, o której wspominał Cody. Tacy świadkowie istnieją kanonicznie dla każdego pozytywnego typu, ponieważ są składniowo monotoniczni.$\rho$$\alpha$$\forall \alpha \forall \beta.\, (\alpha \to \beta) \to \rho \to \rho[\beta/\alpha]$

2. Kiedy przechodzimy od typów ściśle pozytywnych do pozytywnych, wówczas typy indukcyjne nie mogą być dłużej postrzegane jako drzewa (kodowanie typu W). Zamiast tego wprowadzają one pewną formę impredykatywności, ponieważ konstrukcja pozytywnego typu indukcyjnego już określa ilościowo w stosunku do samego typu. Zauważ, że jest to nieco łagodna forma impredykatywności, ponieważ semantykę takich typów można nadal wyjaśnić w kategoriach porządkowej iteracji funkcji monotonicznych.

3. Matthes podaje również przykłady pozytywnych typów indukcyjnych. Szczególnie interesujące są

   • rodzaj kontynuacji , gdzie nie występuje w .$\mu.\, 1 + ((\alpha \to \rho) \to \rho)$$\alpha$$\rho$
   • typ który działa dla każdego typu , zmieniając go w typ dodatni. Zauważ, że bardzo intensywnie wykorzystuje to impredykatywność Systemu F.$\mu \alpha \forall \beta.\, (\alpha \to \beta) \to \rho[\beta/\alpha]$ρ$\rho$

Matthes używa również dodatnich typów indukcyjnych do analizy podwójnej negacji, na przykład w tym artykule: https://www.irit.fr/~Ralph.Matthes/papers/MatthesStabilization.pdf . Wprowadza rozszerzenie Parigota i wykazuje silną normalizację.$\lambda\mu$

Mam nadzieję, że to pomoże w twoim pytaniu.