Можно ли эффективно оценить коэффициенты лямбда-исчисления?

В последнее время я писал множество программ в исчислении лямбда, и мне хотелось бы запустить некоторые из них в режиме реального времени. Тем не менее, насколько теоретическая функциональная парадигма основывается на исчислении лямбда и правиле B-сокращений, я не мог найти ни одного оценщика, который не является игрушкой, не предназначенной для повышения эффективности. Функциональные языки должны быть быстрыми, но те, кого я знаю, фактически не обеспечивают доступ к нормальным формам (см. Hazell lazy оценщик, закрытия схем и т.д.), Поэтому не работайте в качестве оценщиков LC.

Это заставляет меня задаться вопросом: просто невозможно оценить термины исчисления лямбда эффективно, это просто исторический случай/отсутствие интереса, что никто не решил создать для него быстрый оценщик, или я просто что-то пропустил?

Ответ 1

При современном состоянии знаний наилучшим способом оценки лямбда-терминов является так называемая оптимальная технология сокращения графа. Эта техника была введена в 1989 году J.Lamping - это его статья POPL "" Алгоритм оптимального сокращения лямбда-исчисления", а затем пересмотрена и улучшена несколькими авторы. Вы можете найти обзор в моей книге с S.Guerrini " Оптимальная реализация языков функционального программирования ", Cambridge Tracts of Theoretical Computer Science n.45, 1998.

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

На чистых лямбда-членах оптимальное сокращение графа быстрее, чем все другие известные (среда машины, суперкомбинаторы или что-то еще). Некоторые контрольные показатели приведены в вышеупомянутой книге (см. Стр. 296-301), где мы доказали, что наша реализация превзошла как caml-light (предшественник of ocaml) и Haskell (очень медленно). Итак, если вы слышите, что люди говорят, что никогда не было доказано, что оптимальные сокращение быстрее, чем другие методы, это неверно: было доказано, что в теории и экспериментально.

Причина, по которой функциональные языки еще не реализованы, заключается в том, что в практике функционального программирования вы очень редко используете функционалы с действительно высоким рангом, а когда вы делаете, они часто линейны. Как только вы поднимаете ранг, внутренняя сложность лямбда условия могут стать опасно высокими. Имея технику, которая позволяет вам для уменьшения члена во времени O (2 ^ n) вместо O (2 ^ (2 ^ n)) не делает все эта разница на практике: оба вычисления просто неосуществимы.

Недавно я написал короткую статью, которая попыталась объяснить эти проблемы: " Об эффективном сокращении лямбда-терминов". В той же статье я также обсуждаю возможность получения супероптимальных методы сокращения.

Ответ 2

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

Оценщики больших шагов

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

например. если термин, который вы хотите нормализовать, это t u, тогда вы нормализуете как t, так и u, и если norm t является абстракцией лямбда, вы запускаете соответствующее redex и перезапускаете нормализацию по термину, который вы только что получили.

Аннотация/Виртуальные машины

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

Историческим примером является SECD machine.

Danvy et al. показали, что известные абстрактные машины могут быть получены из оценщиков, упомянутых ранее, комбинацией стиля продолжения прохождения и defunctionalisation.

Чтобы вернуть лямбда-терм обратно с абстрактной машины, вам нужно реализовать функцию reification/read back, создающую лямбда-термин на основе состояния, в котором находится устройство. Grégoire и Leroy показывают, как это можно сделать в контексте, где теория типов языка является одной из Coq.

Нормализация по оценке

Нормализация путем оценки - это практика использования механизма оценки языка хоста для реализации процедуры нормализации для другого языка.

Абстракция Lambda превращается в функции на языке хоста, приложение становится приложением на языке хоста и т.д. и т.д.

Этот метод можно использовать типизированным образом (например, нормализовать просто типизированное лямбда-исчисление в Haskell или в OCaml) или нетипизированный (например, просто типизированное лямбда-исчисление еще раз или Условия Coq, скомпилированные в OCaml (!)).