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

Аннотация

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