Как называется этот комбинатор?
-
16-10-2019 - |
Вопрос
Я недавно начал случайно читать в комбинаторной логике, и я заметил, что функция более высокого порядка, которую я регулярно использую, является комбинатором. Этот комбинатор на самом деле довольно полезен (например, вы можете использовать его для определения дополнения на полиномиальных уравнениях), но я никогда не давал ему приличное имя. Кто -нибудь узнает этого комбинатора? (игнорируя различия в функционировании карри)
unknown = function (h, f, g)
function (x) h( f(x), g(x) )
}
В исчислении Lambda полностью карриальная реализация будет $ lambda h. lambda f. lambda g. lambda x. H (FX) (GX) $. Другими словами, если $ m $ - это таинственный комбинатор, то его определяющее уравнение - $ m , h , f , g , x = h , (f , x) , (g , x) $.
Если требуется дополнительная информация, или у меня не хватает ключевой информации, пожалуйста, оставьте комментарий, и я отредактирую свой вопрос.
Решение
Это, вероятно, не стандартное имя, но в Реализация языков функционального программирования В разделе 16.2.4 Саймон Пейтон Джонс называет это S'
. Анкет Это определяется как комбинатор оптимизации
S (B x y) z = S' x y z
Следующий пример из упомянутого раздела. Рассмотреть возможность
λx_n...λx_1.PQ
куда P
а также Q
сложные выражения, которые оба используют все переменные. Устранение абстракций Lambda приводит к квадратичному увеличению размеров терминов в n
:
P Q
S P1 Q1
S (B S P2) Q2
S (B S (B (B S) P3)) Q3
S (B S (B (B S) (B (B (B S)) P4))) Q4
и т. д., где Pi
а также Qi
некоторые термины. С помощью S'
это становится линейным:
P Q
S P1 Q1
S' S P2 Q2
S (S' S) P3 Q3
S (S' (S' S)) P4 Q4