Звёздочка Клини, субэкспоненциалы без правила сокращения и бесконечные вычисления

Аннотация

В работе представлено расширение интуиционистской некоммутативной линейной логики с помощью звёздочки Клини и семейства субэкспоненциалов, каждый из которых допускает правило перестановки и/или ослабления, но не правило сокращения. Субэкспоненциалы, допускающие правило сокращения, применяются для спецификации вычислительных систем (например, машин Тьюринга), корректно завершающих свою работу за конечное число шагов. В работе показано, что, двойственным образом, аксиоматизируемая с помощью омега-правила звёздочка Клини позволяет моделировать бесконечные (никогда не останавливающиеся) вычисления. Предлагаемая система принадлежит классу сложности \(\Pi_1^0\). На самом деле, она является \(\Pi_1^0\)-полной (Buszkowski, 2007). В работе доказана \(\Pi_1^0\)-трудность одностороннего фрагмента данной системы с двумя субэкспоненциалами и звёздочкой Клини (этот результат не следует из конструкции Бушковского). Исчисление с омега-правилом может быть переформулировано как исчисление с бесконечными (нефундированными) выводами (Das & Pous 2018). Рассмотрен также фрагмент этого исчисления с циклическими выводами. В этом фрагменте можно моделировать зацикливание машины Тьюринга, однако оказывается, что в нём моделируются и некоторые нециклические вычисления.