Lean4 Lambda演算DSL宏左结合性问题求助

问题背景 #

参考Lean4官方算术示例实现了支持多参数lambda的lambda项DSL，但存在两个问题：

1. 应用表达式解析为右结合：输入[λ+| (λ x y. x) a b ]被展开为

   Λ.apl (Λ.abstr "x" (Λ.abstr y (Λ.var "x"))) (Λ.apl (Λ.var "a") (Λ.var "b"))
   

   预期应为左结合的

   Λ.apl (Λ.apl (Λ.abstr "x" (Λ.abstr y (Λ.var "x"))) (Λ.var "a")) (Λ.var "b")
   

   怀疑问题出在语法声明syntax lcplus lcplus+ : lcplus。
2. 希望用fold替代当前实现中的do notation递归逻辑。

解决方案 #

1. 修复左结合性问题 #

你对语法声明的怀疑是正确的：syntax lcplus lcplus+ : lcplus默认会触发右结合解析。要实现左结合，无需修改语法规则，只需在宏展开阶段对连续的应用节点做左折叠处理即可。

修改宏展开逻辑，用foldl处理应用的左结合：

macro_rules
  | `([λ+| $e:lcplus]) => do
    let rec expand : Syntax → Lean.MacroM Expr
      | `(lcplus| $args:lcplus+) => do
        let args' ← args.mapM expand
        return args'.foldl (fun acc arg => mkAppM ``Λ.apl #[acc, arg]) (args'.head!)
      | `(lcplus| λ $xs:ident+. $body:lcplus) => do
        let body' ← expand body
        return xs.foldr (fun x acc => mkAppM ``Λ.abstr #[mkStrLit x.getId.toString, acc]) body'
      | `(lcplus| $x:ident) => return mkAppM ``Λ.var #[mkStrLit x.getId.toString]
    expand e

核心逻辑：

• 对于连续的应用节点$args:lcplus+，用foldl从左到右依次组合，将f a b转换为(f a) b。
• 多参数lambda保持foldr处理，因为lambda抽象本身是右结合的（λx y. x等价于λx. λy. x）。

2. 用fold替代do notation递归 #

上述代码已经完全用foldl和foldr替代了手动的do notation递归：

• 应用表达式：args'.foldl遍历所有应用项，从左到右构建左结合的应用结构。
• 多参数抽象：xs.foldr遍历参数列表，从右到左嵌套构建抽象结构。

验证结果 #

修改后，输入[λ+| (λ x y. x) a b ]会被正确展开为预期的左结合形式：

Λ.apl (Λ.apl (Λ.abstr "x" (Λ.abstr "y" (Λ.var "x"))) (Λ.var "a")) (Λ.var "b")

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