Описание тега k-combinator

Используйте k-комбинатор для вопросов, связанных с программным созданием постоянной функции.
2 ответа

Как создать K комбинатор в заколдованном лесу? (Издеваться над пересмешником)

Напомним, что комбинатор K является постоянной функцией. Он всегда возвращает свой первый аргумент: Kxy = x for all y В книге " Чтобы издеваться над пересмешником" автор представляет пример заколдованного леса с говорящими птицами. Птицы имеют повед…
1 ответ

Конвертировать лямбда флип в ски условия

У меня проблемы с преобразованием лямбда-флип в комбинаторы SKI (надеюсь, это имеет смысл). Вот мое обращение: /fxy.fyx /f./x./y.fyx /f./x.S (/y.fy) (/y.x) /f./x.S f (/y.x) /f./x.S f (K x) /f.S (/x.S f) (/x.K x) /f.S (/x.S f) K /f.S (S (/x.S) (/x.f)…
1 ответ

(Kestrel) K-комбинатор: почему он полезен?

Я недавно занимался F# (мой опыт работы с C#) и читаю сайт http://fsharpforfunandprofit.com/, который я считаю очень полезным. Я попал на http://fsharpforfunandprofit.com/posts/defining-functions/ где находится раздел о комбинаторах. Я понимаю их вс…
1 ответ

Функция подписи Тап (К-комбинатор)

Я читал в книге, что функция подписи функции крана (также называемой K-Combinator) ниже: tap :: (a -> *) -> a -> a "Эта функция принимает входной объект a и функцию, которая выполняет некоторое действие над a. Она выполняет данную функцию с…
1 ответ

Как набрать простейший термин лямбда-исчисление (S K K)

Я пытаюсь реализовать простой тип проверки типа лямбда-исчисления. Во время выполнения тестов здравомыслия я попытался набрать (S K K), и моя программа проверки типов выдает эту ошибку: TypeMismatch {firstType = t -> t, secondType = t -> t -&g…
4 ответа

Преобразование лямбда-термина в комбинаторный термин

Предположим, есть несколько типов данных для выражения лямбда и комбинаторных терминов: data Lam α = Var α -- v | Abs α (Lam α) -- λv . e1 | App (Lam α) (Lam α) -- e1 e2 deriving (Eq, Show) infixl 0 :@ data SKI α = V α -- x | SKI α :@ SKI α -- e1 e2…
2 ответа

Чтобы доказать, что SKK и II бета-эквивалент, лямбда-исчисление

Я новичок в лямбда-исчислении и пытаюсь доказать следующее. SKK и II являются бета-эквивалентом. где S = лямбда xyz.xz(yz) K = лямбда xy.x I = лямбда xx Я пытался уменьшить SKK, открыв его, но ничего не получилось, он стал грязным. Не думайте, что S…
1 ответ

Лямбда-сокращения доказывают S K = K I

Здравствуйте, у меня возникли проблемы с доказательством этих комбинаторов S K = K I Шаги с квадратными скобками [] просто показывают вам шаг, который я делаю. Например, [λxy.x / x] в λyz.x z(y z) означает, что я собираюсь заменить (λxy.x) на каждый…
1 ответ

Фиксированная точка K комбинатора

K комбинатор есть K := (λxy.x) и комбинатор с фиксированной точкой Y := λf.(λx.f x x) (λx.f x x), Я пытался посчитать YK: YK = (λx.Kxx)(λx.Kxx) = (λx.x)(λx.x) = (λx.x) = I Потому, что YK является фиксированной точкой K: K(YK) = YK KI = I KIe = Ie = …
1 ответ

Как создать последовательность действий в середине выражения в ReasonML (и не создавать кортеж)?

Я хочу отказаться от функции раньше, если приведены неподходящие аргументы. Обязательное решение в Javascript элегантно: arg=>{ if(arg>limit) return 42; //perform complex operations return x+y } ReasonML как функциональный язык не имеет return…
05 апр '20 в 20:30
2 ответа

Оценка SKI-комбинаторов без достаточных аргументов

Мне было поручено показать, что S(KK)I = K Поскольку S принимает три аргумента, я просто застрял в начале, не зная, как с этим справиться. Я вижу два аргумента, а именно (К.К.) и я, но третьего, который я могу "заметить", нет. Что происходит в этой …
1 ответ

SKS равен SKK?

Контекст Вчера вечером я начал изучать лямбда-исчисление, и я пытаюсь определить, правильно ли то, что я понимаю до сих пор. Понимание SKK эквивалентен комбинатору Identity I. Где L означает лямбда: S = LxLyLz((xz)(yz)) К = LxLy(x) K по существу бер…