Экспресс XOR в комбайнах SKI - PullRequest
Новая
       72

Экспресс XOR в комбайнах SKI

0 голосов
/ 30 апреля 2018

Я пытаюсь решить уверен, но вы можете SKI на кодовых войнах. Это собирается выразить лямбда в комбинаторах SKI. Источник в https://repl.it/@delta4d/SKI.

После некоторых исследований, особенно Комбинаторная логика , я могу решить все случаи, кроме xor.

Сначала я перевожу xor на 

xor x y = if y 
          then if x
               then false
               else true
          else x

что составляет 

xor = \x y -> y (x false true) x
-- false = K I
-- true = K

применяя лямбду к правилам лыжного спорта, я получил 

\x.\y.y (x false true) x
\x.S (\y.y (x false true)) (K x)
\x.S (S I (K (x false true))) (K x)
S (\x.S (S I (K (x false true)))) K
S (S (K S) (\x.S I (K (x false true)))) K
S (S (K S) (S (K (S I)) (\x.K (x false true)))) K
S (S (K S) (S (K (S I)) (S (K K) (\x.x false true)))) K
S (S (K S) (S (K (S I)) (S (K K) (S (\x.x false) (K true))))) K
S (S (K S) (S (K (S I)) (S (K K) (S (S I (K false)) (K true))))) K

Я проверил презентацию SKI на http://ski.aditsu.net,, она отлично работает.

Исходники на Haskell компилируются, но получили ошибку во время выполнения.

Отчеты Codewars: 

Couldn't match type `a' with `Bool' a'
  `a' is a rigid type variable bound by
      a type expected by the context: a -> a -> a at Kata.hs:66:9
Expected type: SKI
                 (Bool' a -> (Bool' a -> Bool' a -> Bool' a) -> a -> a -> a)
  Actual type: SKI (Bool' (Bool' a))
In the second argument of `xorF', namely `true'
In the second argument of `($)', namely `xorF true true'

У меня тест по локальной сети с prettyPrintSKI $ Ap (Ap xor' false) true, и он сообщает: 

• Occurs check: cannot construct the infinite type: a20 ~ Bool' a20
  Expected type: SKI
                   (Bool' a20 -> (Bool' a20 -> Bool' a20 -> Bool' a20) -> Bool' a20)
    Actual type: SKI (Bool' (Bool' a20))
• In the second argument of ‘Ap’, namely ‘true’
  In the second argument of ‘($)’, namely ‘Ap (Ap xor' false) true’
  In the expression: prettyPrintSKI $ Ap (Ap xor' false) true

Что такое бесконечный тип? что такое жесткий тип?

Я делаю то же самое на or, что и or = \x y -> x true y, и все работает просто отлично.

  1. https://www.codewars.com/kata/sure-but-can-you-ski-i
  2. https://en.wikipedia.org/wiki/Combinatory_logic
  3. http://ski.aditsu.net

1 Ответ

0 голосов
/ 30 апреля 2018

Проблема возникает из-за двойного использования x в λxy.y (x false true) x. Вынужден иметь два типа одновременно. Поскольку y использует x, y должен возвращать что-то вроде, скажем, типа a. Теперь это означает, что x false true также имеет тип a. Поэтому что-то типа a должно быть (b -> b -> a) (для некоторых b). Но это невозможно, поскольку это означает, что a должен содержать себя.

Стоит отметить, что ваше решение верное по отношению к. SK, только не система типов Haskell. Так что для исправления нам не нужно дважды использовать x с разными типами. Так почему бы не сделать их одного типа с λxy.y(x false true)(x true false)?

...