Czy MALL + nieograniczone typy rekurencyjne Turing jest kompletne?

Jeśli spojrzysz na rekurencyjne kombinatory w nierozpisanym rachunku lambda, takie jak kombinator Y lub kombinator omega:

\begin{array}{lcl} ω & = & (λ x . x x) (λ x . x x) \\ Y & = & λ f . (λ x . f (x x)) (λ x . f (x x)) \end{array}

$\begin{array}{lcl} \omega & = & (\lambda x.\,x\;x)\;(\lambda x.\,x\;x)\\ Y & = & \lambda f.\,(\lambda x.\,f\;(x\;x))\; (\lambda x.\,f\;(x\;x)) \\ \end{array}$ Oczywiste jest, że wszystkie te kombinatory kończą kopiowanie gdzieś w swojej definicji.

Co więcej, wszystkie te kombinatory można pisać w prostym typie rachunku lambda, jeśli rozszerzysz go o typy rekurencyjne $\mu\alpha.\,A(\alpha)$ , gdzie $\alpha$ może występować negatywnie w typie rekurencyjnym.

Co się jednak stanie, jeśli dodasz pełne (negatywne) typy rekurencyjne do wolnego od wykładniczego fragmentu logiki liniowej (tj. MALL)?

$!A$

! ZA ≜ μ α . ja I ZA I (α \otimes α)

$!A \triangleq \mu\alpha.\;I \;\&\; A \;\&\; (\alpha \otimes \alpha)$

Czy jest tak, że MALL plus nieograniczone typy rekurencyjne wciąż się normalizują‽

lo.logic pl.programming-languages linear-logic

— Neel Krishnaswami
źródło

Myślałem o tym dopiero innego dnia i spędziłem kilka godzin na zabawie z kilkoma pomysłami, ale nie mogłem znaleźć sposobu na wyrażenie wartości rekurencyjnej ani przekonać się, że to niemożliwe. Moją intuicją jest to, że tak nie jest! Nie zastanawiałem się jednak nad innym kierunkiem - jeśli przyjmiesz zasadę wprowadzenia! i typy rekurencyjne, czy to pozwala zdefiniować kombinator punktowy?

— CA McCann,

Zawsze myślałem, że termin w którym każda zmienna występuje najwyżej raz, można pisać w prostym typie fragmentu. To by pokazało, że nie można zdefiniować kombinatora punktów stałych, w którym zmienne są używane liniowo.

λ

$\lambda$

— Andrej Bauer,

Myślę, że po prostu odpowiedział na pytanie o MLL, ale dodatki zrobić pozwalają zmienne mają być powielane (liniowość następnie zakłada pojedynczych zdarzeń w sekwencji redukcyjnych, z grubsza).

A & B

$A & B$

— Neel Krishnaswami

Jeśli komutacje addytywne są pomijane w MALL, łatwo jest pokazać, że rozmiar dowodu zmniejsza się z każdym krokiem eliminacji cięcia. Jeśli dozwolone są komutacje addytywne, dowód nie jest tak łatwy, ale został podany w oryginalnym dokumencie „Linear Logic”. Nazywa się to Twierdzeniem Małej Normalizacji (następstwo 4.22, s. 71), które mówi, że dopóki reguła skurczowo-promocyjna nie jest zaangażowana (jak w przypadku MALL), obowiązuje normalizacja. Argument nie opiera się na samych formułach, mogą być nieskończone (np. Zdefiniowane rekurencyjnie).

$\mu\alpha.\;I \;\&\; A \;\&\; (\alpha \otimes \alpha)$

$\mu$ $!A$

— Stéphane Gimenez
źródło

Zauważ również, że sugerowany typ jest krótko wspomniany na stronie 101 (ostatnia strona) artykułu.

— Stéphane Gimenez