在Haskell中将数值表达式转换为lambda演算

Question

尝试创建一个函数，将任意给定的数值表达式转换为其等效的lambda演算。

为此，我创建了两个函数;一个编码函数和subst。下面是我代码的相关部分。然而，当我运行我的encode函数时，它不能正确地编码乘法表达式;即我认为我已经写了我的添加/多行代码在编码功能错误。然而，我不知道如何解决这个问题。但是，当我运行encode (ArithmeticNum 2)和encode (SecApp (Section (ArithmeticNum 1)) (ArithmeticNum 1))时，它会产生预期的输出。有人可以帮助我修复编码功能的添加/多比特，使其在所有情况下都有效?

我知道编码的乘法语法看起来像mul n m = s -> z -> n (m s) z,但我不确定如何在我的编码函数中写这个。有人能帮我一下吗?谢谢。

data Lambda = LamdaApp Lambda Lambda | LambdaAbs Int Lambda | LambdaVar Int deriving (Show,Eq)
data ArithmeticExpr = Add ArithmeticExpr ArithmeticExpr | Mul ArithmeticExpr ArithmeticExpr | Section ArithmeticExpr | SecApp ArithmeticExpr ArithmeticExpr | ArithmeticNum Int deriving (Show, Eq,Read)
subst :: LambdaExpr -> Int -> LambdaExpr -> LambdaExpr
subst (LambdaVar x) y e | x == y = e
subst (LambdaVar x) y e | x /= y = LambdaVar x
subst (LambdaAbs x e1) y e |  
x /= y && not (free x e) = LambdaAbs x (subst e1 y e)
subst (LambdaAbs x e1) y e |
x /=y && (free x e) = let x' = rename x y in
subst (LambdaAbs x' (subst e1 x (LambdaVar x'))) y e
subst (LambdaAbs x e1) y e | x == y = LambdaAbs x e1
subst (LambdaApp e1 e2) y e = LambdaApp (subst e1 y e) (subst e2 y e)

free :: Int -> LambdaExpr -> Bool
free x (LambdaVar y) = x == y
free x (LambdaAbs y e) | x == y = False
free x (LambdaAbs y e) | x /= y = free x e
free x (LambdaApp e1 e2) = (free x e1) || (free x e2)

rename :: Int -> Int -> Int
rename x y = (max x y) + 1
encode:: ArithmeticExpr -> LambdaExpr
encode(ArithmeticNum 0) = LambdaAbs 0 (LambdaAbs 1 (LambdaVar 1))
encode(ArithmeticNum n) = LambdaAbs 0 (LambdaAbs 1 (helper n 0 1))
where helper :: Int -> Int -> Int -> LambdaExpr
helper 0 _ _ = LambdaVar 1
helper n f x = LambdaApp (LambdaVar f) (helper (n - 1) f x)
encode (Add e1 e2) = LambdaAbs 0 (LambdaAbs 1 ( LambdaApp (LambdaApp (encode e1) (LambdaVar 0)) (LambdaApp (LambdaApp (encode e2) (LambdaVar 0)) (LambdaVar 1))))
encode (Mul e1 e2) = LambdaAbs 0 (LambdaAbs 1 (LambdaAbs 2 (LambdaAbs 3 (LambdaApp (LambdaApp (LambdaVar 0) (encode e1)) (LambdaApp (LambdaVar 1) (encode e2))))))  
encode (SecApp (Section op) e1) = LambdaApp (LambdaApp (encode op) (encode e1)) (encode (ArithmeticNum 1))
encode (Section (ArithmeticNum n)) = LambdaAbs 0 (LambdaAbs 1 (LambdaApp (LambdaVar 0) (encode (ArithmeticNum n))))

Answer 1

正如您所说，教会编码(还有其他编码)中的乘法操作如下:

mul n m = s -> z -> n (m s) z

只看这一行:

encode (Mul e1 e2) = LambdaAbs 0 (LambdaAbs 1 (LambdaAbs 2 (LambdaAbs 3 (LambdaApp (LambdaApp (LambdaVar 0) (encode e1)) (LambdaApp (LambdaVar 1) (encode e2))))))

我想说它对应于更直接的表示法(假设数字是有效的变量名):

mul e1 e2 =  -> 1 -> 2 -> 3 -> (0 e1) (1 e2)

所以，我想说一个错误是让编码的乘法接受四个参数，而它应该只接受两个参数。乘法本身确实应该有四个参数，但是在这种情况下，您正在转换已经应用于参数e1和e2的乘法，因此只剩下两个。内体也是不正确的。你需要这样:

mul e1 e2 =  -> 1 -> e1 (e2 0) 1

等于这个答案上方的方程