Использование лямбда-исчисления для определения сложности времени?

Есть ли какие-либо преимущества в расчете временной сложности алгоритма с использованием лямбда-исчисления? Или есть другая система, разработанная для этой цели?

Любые ссылки будут оценены.

Охад совершенно прав насчет проблем, с которыми сталкивается лямбда-исчисление, как основы для разговоров о классах сложности. Была проделана большая работа по характеристике сложности восстанавливаемости в лямбда-исчислении, особенно вокруг работы по меченым и оптимальным сокращениям из докторской диссертации Леви. Вообще говоря, модели с хорошими затратами для лямбда-исчисления не должны присваивать постоянный вес всем бета-сокращениям: интуитивно, подстановка большой подзадачи во многие места с различной областью действия должна стоить дороже, чем заключение небольшого K-пересчета, и, если нужно определенное количество неизменности стоимости при различных стратегиях переписывания, это становится существенным.

Две ссылки:

1. Lawall & Mairson, 1996, Оптимальность и неэффективность: что не является стоимостной моделью лямбда-исчисления? (.ps.gz) - оригинальный обзор вопросов, связанных с выбором модели затрат, и почему многие правдоподобные идеи не работают.
2. Dal Lago & Martini, 2008, «Слабое лямбда-исчисление как разумная машина». Предлагает модель стоимости для лямбда-исчисления по стоимости по стоимости вместе с хорошим обсуждением литературы.

$\lambda$$\lambda$

Что-то ближе к вашему вопросу, есть текущий проект, который разрабатывает и изучает систему типов (функциональный язык программирования), который статическим анализом может определять (полиномиальные) границы времени выполнения программ (а также другие ресурсы, используемые программы). Таким образом, в некотором смысле это может указывать на то, что может быть некоторое преимущество в использовании функционального программирования для анализа сложности во время выполнения. Домашняя страница проекта находится здесь .

Возможно, представительный документ этого проекта: Ян Хоффманн, Мартин Хофманн. Анализ амортизированных ресурсов с полиномиальным потенциалом - статический вывод полиномиальных границ для функциональных программ. В материалах 19-го Европейского симпозиума по программированию (ESOP'10). ссылка

$\lambda$$\lambda$

$\lambda$

http://arxiv.org/abs/1405.3311

Существует очень интересное направление работы, основанное на линейной логике, которая называется теорией неявной сложности, которая характеризует различные классы сложности, навязывая различные типы дисциплин лямбда-исчислению. IIRC, эта работа началась, когда Беллантони, Кук и Лейвант выяснили, как использовать систему типов, чтобы связать примитивную рекурсию для захвата различных классов сложности.

В общем, привлекательность работы с лямбда-исчислениями заключается в том, что иногда можно найти более экстенсиональные (то есть, более математически прослеживаемые) характеристики различных интенсиональных признаков, которые дают модели, подобным машинам Тьюринга, свою мощность. Например, одно различие между машинами Тьюринга и чистым лямбда-исчислением состоит в том, что, поскольку Тьюринг получает коды программ, клиент может вручную устанавливать тайм-ауты, реализовывать согласование - и, следовательно, может вычислять параллельно или. Тем не менее, таймауты также могут быть смоделированы метрически, и Эскардо предположил (я не знаю его статус), что метрические пространственные модели лямбда-исчисления полностью абстрактны для тайм-аутов PCF +. Метрические пространства - это очень хорошо изученные математические объекты, и очень приятно использовать эту теорию.

Однако сложность использования лямбда-исчисления состоит в том, что оно заставляет вас противостоять явлениям более высокого порядка прямо из стартовых ворот. Это может быть очень тонким, так как тезис Черча-Тьюринга проваливается при более высоком типе - естественные модели вычислений отличаются при более высоком типе, поскольку они отличаются тем, что вам разрешено делать с представлениями вычислений. (Параллельный или простой пример этого явления, поскольку он демонстрирует разницу между LC и TM.) Более того, между различными моделями нет даже строгого включения, поскольку противоположность функционального пространства означает, что более выразительная сила на один порядок подразумевает менее выразительную силу на порядок выше.

Насколько я знаю, лямбда-исчисление плохо подходит для этой цели, так как понятие времени / пространства сложно сформулировать в лямбда-исчислении.

Что такое 1 единица времени сложности? Бета-сокращение? А как насчет единиц космической сложности? Длина строки?

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

Вы также можете посмотреть исчисления явных подстановок, которые разбивают метауровневую подстановку лямбда-исчисления на ряд явных шагов редукции. Это затрагивает точку зрения Чарльза, что все замены не должны считаться одинаковыми при рассмотрении сложности времени.

См. Nils Anders Danielsson, Облегченный полуформальный анализ сложности времени для чисто функциональных структур данных, который реализован как библиотека в Agda. Цитаты, приведенные в статье, также выглядят очень многообещающе.

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