我正在尝试将教会编码转换为数字。我定义了自己的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
我理解这3个数字的lambda编码的方式是这样的:
0:\ s。 \ z。 z
1:\ s。 \ z。 s z
2:\ s。 \ z。 s(s z)
因此,我假设我的逻辑是正确的,但是我很难弄清楚反向转换的方式。我对Haskell相当陌生,因此非常感谢您为我做错事提供的帮助。
您应该在外部(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