比较语法树模数alpha转换

Question

我正在编写一个编译器/校对检查器,我想知道,如果我有一个这样的语法树,例如:

data Expr
    = Lambdas (Set String) Expr
    | Var String
    | ...

如果有办法检查Exprs 的alpha等价(等价模重命名).Expr然而,这与lambda演算的不同之处在于lambda中的变量集是可交换的 - 即参数的顺序不会影响检查.

(但是,为了简单起见,与此Lambda ["x","y"] ...不同Lambda ["x"] (Lambda ["y"] ...),在这种情况下,顺序确实很重要).

换句话说,给定两个Exprs,如何才能有效地找到从一个到另一个的重命名？NP-complete这种组合问题的气味.

Answer 1

参数的可交换性暗示了指数比较,真实.

但我怀疑你可以规范化参数列表,所以你只需要按单个顺序比较它们.然后,与重命名比较的树将在树的大小上基本上是线性的.

我建议做的是,对于每个参数列表,访问子树(按顺序,后序,只要您保持一致无关紧要)并按参数首次遇到的顺序索引对参数进行排序参数使用.所以,如果你有

  lambda(a,b):  .... b .....  a  ... b ....

你将参数列表排序为:

  lambda(b,a)

因为你首先遇到b,然后是第二次,而b的额外遭遇并不重要.将树与规范化参数列表进行比较.

如果你坚持lambda子句中的运算符可以是可交换的,那么生活会变得更加混乱.我的猜测是你仍然可以将它标准化.