Преобразование из кодировки Черча в цифры

Я пытаюсь преобразовать церковную кодировку в цифры. Я определил свое собственное определение Lambda следующим образом:

type Variable = String

data Lambda = Lam Variable Lambda
            | App Lambda Lambda
            | Var Variable
            deriving (Eq, Show)

Я уже написал преобразование цифр в церковную кодировку, и оно работает так, как я ожидаю, вот как я это определил:

toNumeral :: Integer -> Lambda
toNumeral n = Lam "s" (Lam "z" (wrapWithAppS n (Var "z")))
  where
    wrapWithAppS :: Integer -> Lambda -> Lambda
    wrapWithAppS i e
        | i == 0 = e
        | otherwise = wrapWithAppS (i-1) (App (Var "s") e)

Я провел свои собственные тесты, и вот результаты терминала при тестировании на 0, 1 и 2:

*Church> toNumeral 0
Lam "s" (Lam "z" (Var "z"))
*Church> toNumeral 1
Lam "s" (Lam "z" (App (Var "s") (Var "z")))
*Church> toNumeral 2
Lam "s" (Lam "z" (App (Var "s") (App (Var "s") (Var "z"))))

Теперь я пытаюсь сделать наоборот, и я просто не могу уложиться в голове аргументы, которые нужно передать. Вот что у меня есть:

fromNumeral :: Lambda -> Maybe Integer
fromNumeral  (Lam s (Lam z (App e (Var x))))
    | 0 == x = Just 0
    | ...

Я попытался заменить (App e (Var x)) на (Var x), но я получаю эту ошибку для обоих, когда пытаюсь проверить базовый случай преобразования церковной кодировки 0 в Just 0:

*** Exception: Church.hs:(166,1)-(167,23): Non-exhaustive patterns in function fromNumeral

То, как я понимаю лямбда-кодирование для трех чисел, таково:

0: \s. \z. z

1: \s. \z. s z

2: \s. \z. s (s z)

Итак, я предполагаю, что моя логика верна, но мне трудно понять, как будет происходить обратное преобразование. Я новичок в Haskell, поэтому любая помощь в объяснении того, что я могу делать неправильно, очень ценится.


haskell church-encoding lambda-calculus
person Budz Owein    schedule 04.11.2019    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вы должны сопоставлять внешние (Lam "s" (Lam "z" )), но внутреннюю цепочку App следует анализировать рекурсивно, отражая способ, которым она была построена:

fromNumeral (Lam s (Lam z apps)) = go apps
    where
        go (Var x) | x == z = Just 0
        go (App (Var f) e) | f == s = (+ 1) <$> go e
        go _ = Nothing

fromNumeral _ = Nothing
person Fyodor Soikin    schedule 04.11.2019
comment
Спасибо, это имеет смысл! Мне нужно было только переключить s на (Var s), чтобы это сработало, потому что я определяю переменные как строки, поэтому равенство не работает без этого изменения. Если я могу спросить, на что указывает вторая строка, я понимаю, что вы добавляете 1 к базовому регистру, но синтаксис с использованием ‹$› сбивает меня с толку. - person Budz Owein; 04.11.2019
comment
2. Извините, я пропустил там вложенный Var. Я обновил ответ. - person Fyodor Soikin; 04.11.2019