Таким образом, существует алгоритм преобразования терминов лямбда-исчисления в комбинаторную логику с использованием комбинаторов SK. Это производит вещи, которые взрываются в размере. Я хотел бы знать больше об этом взрыве в размере. Однако я не могу придумать лучшего алгоритма. Я слышал, что функциональные языки практически компилируются в комбинаторы, поэтому кажется, что должен существовать лучший алгоритм. Я посмотрел статью Дэвида Тернера на эту тему, и он в основном говорит, что нужно применить несколько оптимизаций, и они вызывают «значительное улучшение».
Означает ли "значительное улучшение", что размер уменьшается только до полиномиального увеличения? Есть ли известный способ преобразования лямбда-терминов в комбинаторную логику только с полиномиальным (или меньшим?) Увеличением? Если такой алгоритм существует, это практично?
Ответы:
Я не специалист по этому вопросу, но вот две исторические работы, которые, похоже, тесно связаны с этим вопросом, и, возможно, это полуактивная область исследований. Тернер предложил набор комбинаторов, которые можно сократить до комбинаторов SK. В следующей статье утверждается, что комбинаторы Тернера, даже не сводимые к комбинаторам SK, приводят к экспоненциальному взрыву (и что, по-видимому, сокращение до условий SK будет еще большим). но затем во 2-й статье говорится, что существует эффективный O (n log n) пространственный алгоритм, основанный на комбинаторах Тернера. (кажется, возможно, были сделаны заявления о полиномиальной эффективности, которые рассматриваются как не полностью продемонстрированные / недоказанные и, следовательно, рассматриваются как предположения ...
Что такое эффективная реализация λ-исчисления? / Frandsen, Sturtivant (1991) (см. С.18)
Перевод комбинаторов Тернера в O (n log n) пространстве / Noshita (1985)
источник