Могут ли типизированные лямбда-исчисления выражать * все * алгоритмы ниже заданной сложности?

21

Я знаю, что сложность большинства разновидностей типизированных лямбда-исчислений без примитива Y-комбинатора ограничена, т. Е. Могут быть выражены только функции ограниченной сложности, причем граница увеличивается с ростом выразительности системы типов. Напомню, что, например, исчисление конструкций может выражать, по крайней мере, двукратно экспоненциальную сложность.

Мой вопрос касается того, могут ли типизированные лямбда-исчисления выражать все алгоритмы с определенной степенью сложности или только некоторые? Например, существуют ли алгоритмы экспоненциального времени, не выражаемые никаким формализмом в лямбда-кубе? Какова «форма» пространства сложности, которое полностью покрыто различными вершинами Куба?

jkff
источник
Я думаю, что ответ да: мы можем выразить ограниченную универсальную машину Тьюринга.
Каве
3
Вы уверены в двоякой экспоненциальной верхней границе? Если я правильно помню, CoC - это самый выразительный «угол» лямбда-куба, что означает, что он включает в себя систему F (то есть полиморфный -calculus), который выходит далеко за пределы двукратно экспоненциального ... В любом случае, ответ определенно да, посмотрите, например, мой ответ здесь . Я могу опубликовать более подробный ответ, если хотите. λ
Дамиано Мазза
1
К сожалению, я неправильно понял ваш вопрос, вы не спрашиваете о некоторых типизированных -calculi но конкретно о типизированных -calculi из лямбда - куба. Боюсь, что здесь нет никакой интересной сложности, все они слишком выразительны, хотя я знаю точный ответ только для System F и System F . λ ωλλω
Дамиано Мазза
4
Функция Аккермана может быть выражена в исчислении конструкций, поэтому не может быть правильным, что эта функция является просто двукратно экспоненциальной.
Андрей Бауэр
Я думаю, что читал об этом обязательстве в книге Coq'Art, но я, скорее всего, ошибаюсь. Благодарность!
JKFF

Ответы:

19

Я дам частичный ответ, я надеюсь, что другие заполнят пробелы.

В типизированных -calculi можно дать тип обычным представлениям данных ( для целочисленных (унарных) чисел, для двоичных строк, для логических значений) и задаться вопросом, что является сложностью функций / задач, представимых / разрешимых типизированными терминами. Я знаю точный ответ только в некоторых случаях, и в случае с простым набором он зависит от соглашения, используемого при определении «представимого / разрешимого». Во всяком случае, я не знаю ни одного случая, в котором бы была двойная экспоненциальная верхняя граница.N a t S t r B o o lλNatStrBool

Сначала краткий обзор Лямбда-куба. Его 8 исчислений получены путем включения или выключения следующих 3 видов зависимостей поверх простого типа калькуляции (STLC):λ

  • полиморфизм : сроки могут зависеть от типов;
  • зависимые типы : типы могут зависеть от условий;
  • более высокий порядок : типы могут зависеть от типов.

(Зависимость терминов от терминов всегда есть).

Добавление полиморфизма Урожайность System F. Здесь вы можете ввести целые Церкви с , и аналогично для двоичных строк и логических значений. Жирар доказал, что члены системы F типа N a tN a t представляют в точности числовые функции, совокупность которых доказуема в арифметике Пеано второго порядка. Это в значительной степени повседневная математика (хотя и без какой-либо формы выбора), поэтому класс огромен, функция Аккермана является своего рода крошечным микробом, не говоря уже о функции 2 2Nat:=X.(XX)XXNatNat . Я не знаю ни одной «естественной» числовой функции, которая не может быть представлена ​​в Системе F. Примеры обычно строятся с помощью диагонализации или кодирования согласованности PA второго порядка или других трюков с собственнойссылкой(например, определениеβ-равенства в Системе Ф сам). Конечно, в системе F вы можете преобразовать между унарными целыми числамиNatи их двоичным представлениемStr, а затем проверить, например, является ли первый бит 1, таким образом, класс разрешимых задач (по типуStrBоол) одинаково огромен.22nβNatStrStrBool

Остальные 3 исчисления лямбда-куба, которые включают полиморфизм, следовательно, по меньшей мере так же выразительны, как и система F. К ним относятся система F ω (полиморфизм + более высокий порядок), которая может точно выражать доказуемо полные функции в PA более высокого порядка, и исчисление Конструкции (CoC) - наиболее выразительное исчисление куба (все зависимости включены). Я не знаю характеристику выразительности CoC с точки зрения арифметических теорий или теорий множеств, но это должно быть довольно пугающим :-)ω

Я гораздо более невежественен в отношении исчислений, полученных путем простого включения зависимых типов (по существу, теории типов Мартина-Лёфа без равенства и натуральных чисел), типов более высокого порядка или обоих. В этих исчислениях типы мощные, но термины не могут получить доступ к этой силе, поэтому я не знаю, что вы получите. В вычислительном отношении я не думаю, что вы получите гораздо больше выразительности, чем с простыми типами, но я могу ошибаться.

Таким образом, мы остались с STLC. Насколько я знаю, это единственное исчисление Куба с интересными (то есть не чудовищно большими) верхними границами сложности. На TCS.SE есть вопрос без ответа , и на самом деле ситуация немного тонкая.

Во-первых, если вы исправите атом и определите N a t : = ( X X ) X X , то есть результат Швичтенберга (я знаю, что где-то в Интернете есть перевод этой статьи на английский, но я не могу его найти теперь), который говорит вам, что функции типа N a tN a t являются в точности расширенными полиномами (с if-then-else). Если вы допускаете некоторую «слабину», т.е. вы разрешаете создавать экземпляр параметра X по своему желанию и учитывает условия типа N a t [XNat:=(XX)XXNatNatX спроизвольным A , можно представить гораздо больше. Например, любая башня экспонент (так что вы можете выйти далеко за пределы двукратной экспоненты), а также функция предшественника, но все равно без вычитания (если вы рассматриваете двоичные функции и пытаетесь набрать их с помощью N a t [ A ] N a t [ A ] N a t ). Таким образом, класс числовых функций, представимых в STLC, немного странный, он является строгим подмножеством элементарных функций, но не соответствует никому из известных.Nat[A]NatANat[A]Nat[A]Nat

В явном противоречии с вышесказанным есть статья Mairson, в которой показано, как кодировать функцию перехода произвольной машины Тьюринга , из которой вы получаете член типа N a t [ A ] B o o l (для некоторого типа В зависимости от M ), который, учитывая входное целое число Церковного n , имитирует выполнение M, начиная с фиксированной начальной конфигурации для ряда шагов вида 2 2 2 n ,MNat[A]BoolAMnM

222n,
с фиксированной высотой башни. Это не показывает, что каждая элементарная проблема разрешима STLC, потому что в STLC нет способа преобразования двоичной строки (типа ), представляющей ввод M, в тип, используемый для представления конфигураций M в Кодировка Марсона. Таким образом, кодировка как-то «неоднородна»: вы можете имитировать элементарно длинные исполнения с фиксированного входа, используя отдельный термин для каждого входа, но нет термина, который обрабатывает произвольные входы.StrMM

CSTStr[A]BoolACSTCSTLINTIMELINTIMECST


CST

CST=REG{0,1}

(Это теорема 3.4 в их статье).

CSTLINTIMEλCST

(Кстати, я поделился своим удивлением в этом ответе на вопрос МО об «неизвестных теоремах»).

Дамиано Мазза
источник
3
Закончил читать ответ только чтобы снова увидеть это имя. Я думаю, что вы уже научили меня больше, чем мои собственные профессора. Интернет прекрасная вещь. Спасибо.
MaiaVictor
@Damiano Mazza. Понравился ваш ответ, но понятие «единообразие» не так тривиально, не так ли?
Андреа Асперти
λλ
12

Ответ на вопрос, который Дамиано поднял в своем превосходном ответе:

Я гораздо более невежественен в отношении исчислений, полученных путем простого включения зависимых типов (по существу, теории типов Мартина-Лёфа без равенства и натуральных чисел), типов более высокого порядка или обоих. В этих исчислениях типы мощные, но термины не могут получить доступ к этой силе, поэтому я не знаю, что вы получите.

ω

λPλPω

Я не знаю, какова сила нечеткого исчисления конструкций, если вы добавите индуктивные типы и большие исключения.

Нил Кришнасвами
источник
Спасибо @Neel! Я думаю, что теперь у нас есть полная картина.
Дамиано Мазза
7

Я постараюсь дополнить отличный ответ Дамиано.

λF HA2

TLTL

L

  • FHA2

  • TPAF

λPTIME

В общем, это большой путь исследований, поэтому я просто ссылаюсь на один из моих предыдущих ответов .

Коди
источник
3
Ср Стивен Кук и Аласдэр Уркхарт " Функциональные интерпретации выполнимо конструктивной арифметики ", 1993, для варианта теории сложности.
Каве