На странице Википедии для комбинаторов с фиксированной точкой написан довольно загадочный текст Y комбинатор является примером того, что делает лямбда-исчисление непоследовательным. Поэтому к этому следует относиться с подозрением. Однако комбинатор Y можно считать безопасным, если он определен...
Комбинатор FIX с фиксированной запятой (он же Y-комбинатор) в (нетипизированном) лямбда-исчислении ( λλ\lambda ) определяется как: FIX ≜λf.(λx.f (λy.x x y)) (λx.f (λy.x x y))≜λf.(λx.f (λy.x x y)) (λx.f (λy.x x y))\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y....
Большинство из нас знает соответствие между комбинаторной логикой и лямбда-исчислением . Но я никогда не видел (может быть, я недостаточно глубоко изучил) эквивалент «типизированных комбинаторов», соответствующих простейшему типу лямбда-исчисления. Существует ли такая вещь? Где можно найти...
Хорошо известно, что комбинаторы S и K образуют базис для исчисления комбинаторов в том смысле, что все другие комбинаторы могут быть выражены через них. Существует также базис Карри B, C, K, W, который обладает тем же свойством. Таких баз должно быть бесконечное количество, но я не знаю других....
Y комбинатор имеет тип . Согласно соответствию Карри-Говарда, поскольку тип является обитаемым, он должен соответствовать истинной теореме. Однако всегда истинно, поэтому кажется, что тип Y-комбинатора соответствует теореме , что не всегда верно. Как это может быть?( a → a ) → a(a→a)→a(a...
Выражение комбинатора (скажем, в основе SK) можно рассматривать как функцию, которая отображает выражения исчисления комбинатора в выражения исчисления комбинатора. То есть выражение как функцию , где - множество всех синтаксически допустимых выражений комбинатора в базисе SK. Это отображение...
По словам Питера Селинджера , Лямбда-исчисление алгебраическое (PDF). В начале этой статьи он говорит: Известно, что комбинаторная интерпретация лямбда-исчисления несовершенна, поскольку она не удовлетворяет правилу: при интерпретации не подразумевает (Barendregt, 1984).ξξξM=NM=NM =...
В частности, если я определил новый K2K2K_2 как K2=λx.(λy.y)K2=λx.(λy.y)K_2 = \lambda x. (\lambda y. y) вместо K=λx.(λy.x)K=λx.(λy.x)K = \lambda x. (\lambda y. x) будет ли {S,K2,I}{S,K2,I}\{S, K_2,I\} -счет вычисляться на основе конкуренции? Я предполагаю «нет» только потому, что я не могу...
Таким образом, существует алгоритм преобразования терминов лямбда-исчисления в комбинаторную логику с использованием комбинаторов SK. Это производит вещи, которые взрываются в размере. Я хотел бы знать больше об этом взрыве в размере. Однако я не могу придумать лучшего алгоритма. Я слышал, что...
В работе Криса Окасаки « Сглаживание комбинаторов: выживание без скобок » он показывает, что двух комбинаторов достаточно и необходимо в качестве основы для кодирования выражений по Тьюрингу без необходимости использования оператора приложения или скобок. По сравнению с кодировками комбинаторной...