Интуиция за строгой позитивностью?

Мне интересно, может ли кто-нибудь подсказать мне, почему строгая положительность индуктивных типов данных гарантирует строгую нормализацию.

Чтобы было ясно, я вижу, как наличие отрицательных явлений приводит к расхождению, то есть путем определения:

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

мы можем написать расходящуюся функцию.

Но мне интересно, как мы можем доказать, что строго положительные индуктивные типы не допускают расхождения? т.е. есть ли какая-то индукционная мера, которая позволяет нам построить доказательство сильной нормализации (используя логические отношения или подобное)? И где такое доказательство разрушается для негативных явлений? Есть ли хорошие ссылки, которые показывают сильную нормализацию для языка с индуктивными типами?

reference-request pl.programming-languages type-theory type-systems dependent-type jmite
источник

Я думаю, что идея строго положительных типов может быть преобразована в W типов, концептуально. Кроме того, не строгий положительный тип несовместим с Coq vilhelms.github.io/posts/… . Замечено, что позитивный тип согласуется с Агдой, но я хотел бы также увидеть концептуальное объяснение ...

molikto

@molikto Спасибо, это полезно. Но я думал, что W-типы не дают желаемых принципов индукции в интенсиональной теории? Как мы можем доказать сильную нормализацию для строго положительных индуктивов в интенсиональной теории?

Ответы:

Похоже, вам нужен обзор аргументов нормализации для систем типов с положительными типами данных. Я бы порекомендовал кандидатскую диссертацию Накса Мендлера: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html .

$\lambda$

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

Мы бы получили:

λ (t) = 0

$\lambda(t) = 0$

t

$t$

λ (Z e r o) = 0

$\lambda(\mathrm{Zero}) = 0$

λ (S u c (o)) = λ (o) + 1

$\lambda(\mathrm{Suc}(o)) = \lambda(o)+1$

λ (L i m (f)) = sup_{n} λ (f n)

$\lambda(\mathrm{Lim}(f)) = \sup_n \lambda(f\ n)$

где колеблется над членами с нормальными формами. Предостережение заключается в том, что эта интерпретация определяется только в 3-м случае, когда имеет нормальную форму, что требует некоторой осторожности в определениях. $n$ $f\ n$

Затем можно определить рекурсивные функции по индукции по этому порядковому номеру.

Обратите внимание , что эти типы данных могут быть определены уже в классической теории множеств, как указано в отличном Индуктивный Families бумаге Dybjer ( http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf ). Однако, поскольку функциональные пространства настолько огромны, для типов, таких как, Ordтребуются действительно большие порядковые числа для интерпретации.

Коди
источник

Спасибо, это очень полезно! Вы знаете, могут ли такие ординалы быть определены в самой теории типов? то есть, если бы я пытался использовать Agda для индукции-рекурсии, чтобы смоделировать теорию типов с помощью индуктивов (но без индукции-рекурсии), могу ли я использовать что-то подобное Ordдля моделирования ординалов, необходимых для демонстрации обоснованности?

@jmite, вы можете, но ординалы в конструктивных теориях немного странные, и вы могли бы также работать с обоснованными порядками или деревьями ( а-ля W-тип, как полагает Моликто). Может быть трудно иметь единый унифицированный тип, который бы отражал обоснованность каждой индуктивности в объектном языке, хотя ...

cody

@cody Разве пример Ord, который вы даете строго положительный тип?

Хеннинг Басольд

@HenningBasold да, это так (вот почему я использовал это как иллюстрацию!). Но он не ведет себя точно так же, как ординалы в (классической) теории множеств, и, конечно, не похож на множество всех ординалов. В частности, довольно сложно определить порядок по ним.

Cody

@HenningBasold также я должен отметить, что вопрос jmite касался конкретно положительных типов, хотя интересна и информация о более общих настройках!

cody

Другим хорошим источником для выхода за рамки строго положительных типов является кандидатская диссертация Ральфа Мэттса: http://d-nb.info/956895891

Он обсуждает расширения Системы F с (строго) положительными типами в главе 3 и доказывает много сильных результатов нормализации в главе 9. Есть несколько интересных идей, обсужденных в главе 3.

Мы можем добавить наименьшие фиксированные точки для любого типа со свободной переменной , при условии, что мы можем предоставить свидетельство монотонности . Эта идея уже присутствует в работе Мендлера, о которой упоминал Коди. Такие свидетели существуют канонически для любого положительного типа, потому что они синтаксически монотонны. $\rho$ $\alpha$ $\forall \alpha \forall \beta.\, (\alpha \to \beta) \to \rho \to \rho[\beta/\alpha]$
Когда мы переходим от строго положительных к положительным типам, то индуктивные типы больше не могут рассматриваться как деревья (кодирование W-типа). Вместо этого они вводят некоторую форму непредсказуемости, потому что конструкция положительного индуктивного типа уже количественно определяет сам тип. Обратите внимание, что это несколько умеренная форма непредсказуемости, поскольку семантика таких типов все еще может быть объяснена в терминах порядковой итерации монотонных функций.
Мэттес также приводит несколько примеров положительных индуктивных типов. Особенно интересны
- тип продолжения , где не встречается в . $\mu.\, 1 + ((\alpha \to \rho) \to \rho)$ $\alpha$ $\rho$
- тип который работает для любого типа , превращая его в положительный тип. Обратите внимание, что это очень сильно использует непредсказуемость системы F. $\mu \alpha \forall \beta.\, (\alpha \to \beta) \to \rho[\beta/\alpha]$ $\rho$

Matthes также использует положительные индуктивные типы для анализа двойного отрицания, например, в этой статье: https://www.irit.fr/~Ralph.Matthes/papers/MatthesStabilization.pdf . Он вводит расширение Париго и доказывает сильную нормализацию. $\lambda\mu$

Я надеюсь, что это поможет с вашим вопросом.

Хеннинг Базольд
источник