Понятия эффективного вычисления

Алгоритм машины Тьюринга за полиномиальное время считается эффективным, если его время выполнения, в худшем случае, ограничено полиномиальной функцией входного размера. Мне известен сильный тезис Черча-Тьюринга:

Любая разумная модель вычислений может быть эффективно смоделирована на машинах Тьюринга.

Тем не менее, я не знаю основательной теории для анализа вычислительной сложности алгоритмов -calculus.$\lambda$

Есть ли у нас понятие вычислительной эффективности для каждой известной модели вычислений? Существуют ли модели, которые полезны только для вопросов вычислимости, но бесполезны для вопросов сложности вычислений?

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

По счастливой случайности это может быть замечено, что машины Тьюринга, которые не являются, пожалуй, очень неэффективными машинами, также являются очень хорошей моделью сложности. То, что сделало вещи естественными, состоит в том, что существует множество трансформаций с участием ТМ, которые являются полиномиальными. (Универсальная машина, имитация лентной машины с 1-лентной машиной, от произвольного алфавита до двоичного, имитирующего PRAM , ...) и то, что многочлены - это класс функций, устойчивых арифметическими операциями и композицией - что делает их хорошим кандидатом для теории сложности.$n$

Чистое λ-исчисление само по себе бесполезно для сложности. Однако в игру вступила система простого типа, которая позволила гарантировать завершение некоторых λ-членов очень простым способом. Затем некоторые другие системы (системы T , F , ...) допускали большую выразительность при сохранении завершения.

Эффективность или сложность, являющиеся уточнением терминации, а типы, тесно связанные с логикой, позже стали легкой линейной логикой, которая характеризует несколько классов сложности. ( Элементарный , P и некоторые вариации для PSPACE и др.). Исследования в этой области очень активны и не ограничиваются этими классами сложности и даже не ограничиваются λ-исчислением.

tl; dr: λ-исчисление было полезно для вычислимости, терминации и теории сложности.

Однако, чтобы отдать должное должному, машины Тьюринга - хороший и единодушный способ определить, что такое сложность, но это справедливо только для свободных границ, таких как «полином», а не для точных границ, для которых модели, подобные PRAM, более подходят.

С точки зрения сложности времени, я думаю, что это трудно на лямбда-исчисление. Причина в том, что шаг вычисления единицы в лямбда-исчислении - это -reduction ( запись в Википедии ): Все выражения, независимо от их длины, потребовалось бы вычислительный шаг по этой модели.( λ x . t e r m ) v → t e r m [ x : = v ] $\beta$

О включении λ-исчисления в стандартную модель сложности, вот резюме некоторых (очень) свежих исследований по этому вопросу. Это дает ответ на этот вопрос для некоторой ограниченной формы β-редукции. По сути, сложность в стандартной модели затрат аналогична подсчету шагов β-сокращения, когда они ограничены сокращением напора (которое включает стратегии «вызов по имени» и «вызов по стоимости»).

Об инвариантности модели унитарных затрат для сокращения головы Бениамино Аккаттоли и Уго Дал Лаго. (WST2012, ссылка на материалы )

Λ-исчисление является широко принятой вычислительной моделью функциональных программ высшего порядка, однако для нее не существует какой-либо прямой и общепринятой модели затрат. Как следствие, вычислительная трудность приведения λ-членов к их нормальной форме обычно изучается путем рассуждения о конкретных алгоритмах реализации. Здесь мы показываем, что когда снижение напора является основной динамикой, модель унитарных затрат действительно инвариантна. Это улучшает известные результаты, которые имеют дело только со слабым сокращением (вызов по значению или вызов по имени). Инвариантность доказывается с помощью линейного исчисления явных подстановок, которое позволяет красиво разложить любой шаг редукции головы в λ-исчислении на более элементарные шаги замещения, тем самым облегчая рассуждение о комбинаторике редукции головы.