从教会编码转换为数字

Question

我正在尝试将 Church 编码转换为数字。我定义了自己的 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
    | ...

我尝试用 (Var x) 替换 (App e (Var x)) 但是当我尝试测试将教堂编码从 0 转换为 Just 0 的基本情况时，我得到了这两个错误：

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

我对 3 个数字的 lambda 编码的理解是这样的：

0: \s. \z. z

1: \s. \z. s z

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

所以我假设我的逻辑是正确的，但我很难弄清楚反向转换是怎样的。我是 Haskell 的新手，所以非常感谢任何帮助解释我可能做错的事情。

Answer 1

你应该匹配外部 (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

从教会编码转换为数字

Converting from Church Encoding to Numerals

haskell

lambda-calculus

church-encoding