Haskell中数值表达式转Lambda演算的编码问题求助

首先先修正代码中的两处拼写/类型不一致错误，这是确保代码能正常编译的前提：

• 定义Lambda类型时，构造函数LamdaApp拼写错误，应改为LambdaApp
• subst和free函数的参数类型LambdaExpr不存在，应改为Lambda（对应你定义的data Lambda = ...）

乘法编码的修复 #

你已经明确乘法的Lambda演算标准编码是：

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

当前encode (Mul e1 e2)的实现完全偏离了这个结构，多了不必要的抽象层，且应用逻辑错误。修正后的完整encode函数如下：

encode:: ArithmeticExpr -> Lambda
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 -> Lambda
          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 $
    LambdaApp (encode e1) (LambdaApp (encode e2) (LambdaVar 0))
    `LambdaApp` (LambdaVar 1)

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))))

修正说明 #

• LambdaAbs 0对应标准编码中的\s，LambdaAbs 1对应\z
• LambdaApp (encode e2) (LambdaVar 0)实现了m s的逻辑
• 外层的LambdaApp (encode e1) ...实现了n (m s)的逻辑
• 最后应用LambdaVar 1（即z），得到完整的n (m s) z结构，完全匹配乘法的Lambda演算定义

验证示例 #

执行encode (Mul (ArithmeticNum 2) (ArithmeticNum 3))，生成的Lambda项对应标准乘法编码展开后的形式，你可以通过手动归约验证其正确性。

内容的提问来源于stack exchange，提问作者Student