Я знаю, что сложность большинства разновидностей типизированных лямбда-исчислений без примитива Y-комбинатора ограничена, т. Е. Могут быть выражены только функции ограниченной сложности, причем граница увеличивается с ростом выразительности системы типов. Напомню, что, например, исчисление конструкций может выражать, по крайней мере, двукратно экспоненциальную сложность.
Мой вопрос касается того, могут ли типизированные лямбда-исчисления выражать все алгоритмы с определенной степенью сложности или только некоторые? Например, существуют ли алгоритмы экспоненциального времени, не выражаемые никаким формализмом в лямбда-кубе? Какова «форма» пространства сложности, которое полностью покрыто различными вершинами Куба?
Ответы:
Я дам частичный ответ, я надеюсь, что другие заполнят пробелы.
В типизированных -calculi можно дать тип обычным представлениям данных ( для целочисленных (унарных) чисел, для двоичных строк, для логических значений) и задаться вопросом, что является сложностью функций / задач, представимых / разрешимых типизированными терминами. Я знаю точный ответ только в некоторых случаях, и в случае с простым набором он зависит от соглашения, используемого при определении «представимого / разрешимого». Во всяком случае, я не знаю ни одного случая, в котором бы была двойная экспоненциальная верхняя граница.N a t S t r B o o lλ Nat Str Bool
Сначала краткий обзор Лямбда-куба. Его 8 исчислений получены путем включения или выключения следующих 3 видов зависимостей поверх простого типа калькуляции (STLC):λ
(Зависимость терминов от терминов всегда есть).
Добавление полиморфизма Урожайность System F. Здесь вы можете ввести целые Церкви с , и аналогично для двоичных строк и логических значений. Жирар доказал, что члены системы F типа N a t → N a t представляют в точности числовые функции, совокупность которых доказуема в арифметике Пеано второго порядка. Это в значительной степени повседневная математика (хотя и без какой-либо формы выбора), поэтому класс огромен, функция Аккермана является своего рода крошечным микробом, не говоря уже о функции 2 2Nat:=∀X.(X→X)→X→X Nat→Nat . Я не знаю ни одной «естественной» числовой функции, которая не может быть представлена в Системе F. Примеры обычно строятся с помощью диагонализации или кодирования согласованности PA второго порядка или других трюков с собственнойссылкой(например, определениеβ-равенства в Системе Ф сам). Конечно, в системе F вы можете преобразовать между унарными целыми числамиNatи их двоичным представлениемStr, а затем проверить, например, является ли первый бит 1, таким образом, класс разрешимых задач (по типуStr→Bоол) одинаково огромен.22n β Nat Str Str→Bool
Остальные 3 исчисления лямбда-куба, которые включают полиморфизм, следовательно, по меньшей мере так же выразительны, как и система F. К ним относятся система F ω (полиморфизм + более высокий порядок), которая может точно выражать доказуемо полные функции в PA более высокого порядка, и исчисление Конструкции (CoC) - наиболее выразительное исчисление куба (все зависимости включены). Я не знаю характеристику выразительности CoC с точки зрения арифметических теорий или теорий множеств, но это должно быть довольно пугающим :-)ω
Я гораздо более невежественен в отношении исчислений, полученных путем простого включения зависимых типов (по существу, теории типов Мартина-Лёфа без равенства и натуральных чисел), типов более высокого порядка или обоих. В этих исчислениях типы мощные, но термины не могут получить доступ к этой силе, поэтому я не знаю, что вы получите. В вычислительном отношении я не думаю, что вы получите гораздо больше выразительности, чем с простыми типами, но я могу ошибаться.
Таким образом, мы остались с STLC. Насколько я знаю, это единственное исчисление Куба с интересными (то есть не чудовищно большими) верхними границами сложности. На TCS.SE есть вопрос без ответа , и на самом деле ситуация немного тонкая.
Во-первых, если вы исправите атом и определите N a t : = ( X → X ) → X → X , то есть результат Швичтенберга (я знаю, что где-то в Интернете есть перевод этой статьи на английский, но я не могу его найти теперь), который говорит вам, что функции типа N a t → N a t являются в точности расширенными полиномами (с if-then-else). Если вы допускаете некоторую «слабину», т.е. вы разрешаете создавать экземпляр параметра X по своему желанию и учитывает условия типа N a t [X Nat:=(X→X)→X→X Nat→Nat X спроизвольным A , можно представить гораздо больше. Например, любая башня экспонент (так что вы можете выйти далеко за пределы двукратной экспоненты), а также функция предшественника, но все равно без вычитания (если вы рассматриваете двоичные функции и пытаетесь набрать их с помощью N a t [ A ] → N a t [ A ′ ] → N a t ). Таким образом, класс числовых функций, представимых в STLC, немного странный, он является строгим подмножеством элементарных функций, но не соответствует никому из известных.Nat[A]→Nat A Nat[A]→Nat[A′]→Nat
В явном противоречии с вышесказанным есть статья Mairson, в которой показано, как кодировать функцию перехода произвольной машины Тьюринга , из которой вы получаете член типа N a t [ A ] → B o o l (для некоторого типа В зависимости от M ), который, учитывая входное целое число Церковного n , имитирует выполнение M, начиная с фиксированной начальной конфигурации для ряда шагов вида 2 2 ⋮ 2 n ,M Nat[A]→Bool A M n M
(Это теорема 3.4 в их статье).
(Кстати, я поделился своим удивлением в этом ответе на вопрос МО об «неизвестных теоремах»).
источник
Ответ на вопрос, который Дамиано поднял в своем превосходном ответе:
Я не знаю, какова сила нечеткого исчисления конструкций, если вы добавите индуктивные типы и большие исключения.
источник
Я постараюсь дополнить отличный ответ Дамиано.
В общем, это большой путь исследований, поэтому я просто ссылаюсь на один из моих предыдущих ответов .
источник