Вопросы с тегом «combinatory-logic»

44
Как комбинатор Y иллюстрирует «несоответствие лямбда-исчисления»?

На странице Википедии для комбинаторов с фиксированной точкой написан довольно загадочный текст Y комбинатор является примером того, что делает лямбда-исчисление непоследовательным. Поэтому к этому следует относиться с подозрением. Однако комбинатор Y можно считать безопасным, если он определен...

28
Понятный, интуитивно понятный вывод комбинатора с фиксированной точкой (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....

26
Есть ли типизированное исчисление SKI?

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

19
Базисные наборы для комбинаторного исчисления

Хорошо известно, что комбинаторы S и K образуют базис для исчисления комбинаторов в том смысле, что все другие комбинаторы могут быть выражены через них. Существует также базис Карри B, C, K, W, который обладает тем же свойством. Таких баз должно быть бесконечное количество, но я не знаю других....

16
Противоречит ли Y комбинатор соответствию Карри-Ховарду?

Y комбинатор имеет тип . Согласно соответствию Карри-Говарда, поскольку тип является обитаемым, он должен соответствовать истинной теореме. Однако всегда истинно, поэтому кажется, что тип Y-комбинатора соответствует теореме , что не всегда верно. Как это может быть?( a → a ) → a(a→a)→a(a...

13
Какие функции могут вычислять выражения исчисления комбинатора?

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

10
Комбинаторная интерпретация лямбда-исчисления

По словам Питера Селинджера , Лямбда-исчисление алгебраическое (PDF). В начале этой статьи он говорит: Известно, что комбинаторная интерпретация лямбда-исчисления несовершенна, поскольку она не удовлетворяет правилу: при интерпретации не подразумевает (Barendregt, 1984).ξξξM=NM=NM =...

10
Является ли исчисление SK2 полным базисом, где K2 - перевернутый K комбинатор?

В частности, если я определил новый 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\} -счет вычисляться на основе конкуренции? Я предполагаю «нет» только потому, что я не могу...

9
Термины комбинаторной логики всегда больше?

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

9
Простейшая полная пара базисов комбинаторов для плоских выражений

В работе Криса Окасаки « Сглаживание комбинаторов: выживание без скобок » он показывает, что двух комбинаторов достаточно и необходимо в качестве основы для кодирования выражений по Тьюрингу без необходимости использования оператора приложения или скобок. По сравнению с кодировками комбинаторной...