Можно ли выразить XOR с помощью комбинаторов SKI?

У меня вопрос по поводу SKI-Combinators.

Можно ли выразить XOR (исключающее или) только с помощью комбинаторов S и K?

У меня есть

True = Cancel
False = (Swap Cancel)

куда

Cancel x y = K x y = x   
Swap: ff x y = S ff x y = ff y x

boolean logic combinators combinatory-logic lambda-calculus
person CWHsu    schedule 09.05.2016    source источник
comment
I можно представить как S K K. Итак, если вы можете выразить NOR с помощью SKI, вы можете сделать это и с помощью SK.   -  person Anton Trunov    schedule 09.05.2016
comment
Будет ли это инфиксным? а как насчет брекетинга? (p.s. я пробовал несколько способов, пока не увенчались успехом) Спасибо!   -  person CWHsu    schedule 09.05.2016
comment
Предполагая, что вы заключаете свои логические связки в круглые скобки, то есть NOR = (... some expression ...): (1) NOR не может быть выражено как постфиксный оператор (как AND) - чтобы увидеть это, обратите внимание, что T T NOR = T, независимо от того, что такое NOR (но должно быть F); (2) NOR не может быть выражен как инфиксный оператор -- F NOR F = F (но должен быть T)   -  person Anton Trunov    schedule 10.05.2016
comment
Ах да конечно! на самом деле я совершил огромную ошибку, задав неправильный вопрос! Я хотел спросить XOR, а не NOR! Очень жаль!   -  person CWHsu    schedule 10.05.2016

Ответы (1)


arrow_upward
4
arrow_downward

Булевы значения

Ваш вопрос немного неясен в деталях, но кажется, что вы имеете в виду, что у вас есть следующее представление логических значений:

T := K
F := S K

Это работает, потому что это означает, что выполняются следующие сокращения:

T t e => t
F t e => e

другими словами, b t e можно интерпретировать как IF b THEN t ELSE e.

Исключающее ИЛИ с точки зрения IF _ THEN _ ELSE _

Итак, учитывая эту структуру, как мы реализуем XOR? Мы можем сформулировать XOR как выражение IF:

xor x y := IF x THEN (not y) ELSE y = (IF x THEN not ELSE id) y

который может быть эта-сведен к

XOR x := IF x THEN not ELSE id = x not id

Некоторые комбинаторы функций

У нас стандартно id = SKK, а not может быть выражено как flip, так как flip b t e = b e t = IF b THEN e ELSE t = IF (not b) THEN t ELSE e. flip само по себе довольно сложно, но выполнимо как

flip := S (S (K (S (KS) K)) S) (KK)

Теперь нам просто нужно найти способ написать функцию, которая берет x и применяет его к двум терминам NOT и ID. Чтобы добраться туда, мы сначала заметим, что если мы установим

app := id

тогда

app f x = (id f) x = f x

так что,

(flip app) x f = f x

Мы почти у цели, так как пока все показывает, что

((flip app) id) ((flip app) not x) = ((flip app) not x) id = (x not) id = x not id

Последний шаг — сделать последнюю линию без точек на x. Мы можем сделать это с помощью оператора композиции функций:

((flip app) id) ((flip app) not x) = compose ((flip app) id) ((flip app) not) x

где требование на compose заключается в том, что

compose f g x = f (g x)

который мы можем получить, установив

compose f g := S (K f) g

Собираем все вместе

Подводя итог, мы получили

xor := compose ((flip app) id) ((flip app) not)

или, полностью расширенный:

xor = S (K ((flip app) id)) ((flip app) not)
    = S (K ((flip app) (SKK))) ((flip app) flip)
    = S (K ((flip SKK) (SKK))) ((flip SKK) flip)
    = S (K (((S (S (K (S (KS) K)) S) (KK)) SKK) (SKK))) (((S (S (K (S (KS) K)) S) (KK)) SKK) (S (S (K (S (KS) K)) S) (KK)))
person Cactus    schedule 22.06.2016