Эквивалентная формулировка теории сложности в лямбда-исчислении?

В теории сложности определение сложности времени и пространства ссылается на универсальную машину Тьюринга: соотв. количество шагов до остановки и количество ячеек на ленте, которых коснулись.

Учитывая тезис Черча-Тьюринга, должно быть возможно определить сложность и в терминах лямбда-исчисления.

Мое интуитивное представление состоит в том, что временная сложность может быть выражена в виде числа β-сокращений (мы можем определить α-преобразование без учета, используя индексы Де Бруджина, и η в любом случае едва ли является уменьшением), тогда как пространственную сложность можно определить как число символы (λ, DB-индексы, «применять» -символы) в наибольшем сокращении.

Это правильно? Если так, где я могу получить ссылку? Если нет, то как я ошибаюсь?

Как вы указали, λ-исчисление имеет, казалось бы, простое понятие сложности времени: просто посчитайте количество шагов β-редукции. К сожалению, все не так просто. Мы должны спросить:

 Is counting β-reduction steps a good complexity measure?

Чтобы ответить на этот вопрос, мы должны уточнить, что мы подразумеваем под мерой сложности в первую очередь. Один хороший ответ дает тезис Слота и Ван Эмде Боаса : любая хорошая мера сложности должна иметь полиномиальное отношение к каноническому понятию сложности времени, определенному с помощью машин Тьюринга. Другими словами, должно быть разумное кодирование tr (.) Из терминов λ-исчисления в машины Тьюринга, чтобы для каждого члена $M$ размера $|M|$: $M$ сводится к значению в $poly(|M|)$ именно тогда, когда $tr(M)$ уменьшает до значения в $poly(|tr(M)|)$ .

Долгое время было неясно, можно ли этого достичь в λ-исчислении. Основными проблемами являются следующие.

• Существуют термины, которые производят нормальные формы за полиномиальное число шагов экспоненциального размера. Смотрите (1). Даже на запись нормальных форм уходит экспоненциальное время.

• Выбранная стратегия сокращения также играет важную роль. Например, существует семейство терминов, которое уменьшает за полиномиальное число параллельных β-шагов (в смысле оптимального λ-редукции (2), но сложность которых не элементарна (3, 4)).

Статья (1) проясняет проблему, показывая разумную кодировку, которая сохраняет класс сложности PTIME, предполагая самые крайние слева сокращения Call-By-Name. Ключевым моментом, по-видимому, является то, что экспоненциальный взрыв может произойти только по неинтересным причинам, которые могут быть побеждены надлежащим разделением подслов.

Обратите внимание, что статьи, подобные (1), показывают, что классы грубой сложности, такие как PTIME, совпадают, считаете ли вы β-шаги или шаги машины Тьюринга. Это не означает, что классы более низкой сложности, такие как O (log n), также совпадают. Конечно, такие классы сложности также нестабильны при изменении модели машины Тьюринга (например, 1-ленточная или многоленточная).

Работа Д. Маззы (5) доказывает теорему Кука-Левина (𝖭𝖯-полноту SAT) с использованием функционального языка (вариант λ-исчисления) вместо машин Тьюринга. Ключевое понимание заключается в следующем:

$$\frac{\text{Boolean circuits}}{\text{Turing machines}}=\frac{\text{affine $\lambda$-terms}}{\text{$\lambda$-terms}}$$

Я не знаю, понятна ли ситуация с пространственной сложностью.

---

1. Б. Аккаттоли, У. Дал Лаго. Бета-сокращение действительно инвариантно .

2. Ж.-Ж. Levy, Сокращения корректирует и оптимизирует данные о лямбда-исчислении.

3. JL Lawall, HG Mairson, Оптимальность и неэффективность: что не является стоимостной моделью лямбда-исчисления ?

4. А. Асперти, Х. Марсон, Параллельное бета-редукция не элементарно рекурсивно .

5. Д. Мазза, Церковь встречает повара и Левина .

Подсчет $\beta$$\lambda$

$\mathsf L$$\mathsf P$$M\to^\ast N$$M$

$\beta$