4

我正在研究编译器/证明检查器，我想知道是否有这样的语法树，例如：

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

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

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

换句话说，给定两个Exprs，如何有效地找到从一个重命名到另一个的重命名？这种组合问题有 NP 完全问题的味道。

4

2 回答 2

6

参数的交换性确实暗示了指数比较，真的。

但我怀疑您可以规范化参数列表，因此您只需按单个顺序比较它们。然后，与重命名相比，树的大小基本上是线性的。

我建议做的是，对于每个参数列表，访问子树（按顺序，后序，只要你一致），并按照访问第一次遇到的顺序的索引对参数进行排序参数使用。所以如果你有

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

您将参数列表排序为：

  lambda(b,a)

因为你先遇到 b，然后是第二个，然后再遇到 b 并不重要。将树与标准化参数列表进行比较。

如果您坚持 lambda 子句中的运算符可以是可交换的，那么生活会变得更加混乱。我的猜测是你仍然可以正常化它。

于 2012-02-27T11:19:24.967 回答
4

我们可以向 Daan Leijen 的HMF寻求一些想法。（他处理“foralls”的活页夹，这也被认为是可交换的。

特别是，他重新绑定了正文中出现顺序的变量。

然后，术语的比较涉及以相同的方式进行 sklemizing 并比较结果。

我们可以通过用本地无名表示替换那个 skolemization pass 来做得更好。

data Bound t a = Bound {-# UNPACK #-} !Int t | Unbound a

instance Functor (Bound t) where ...
instance Bifunctor Bound where ...

data Expr a
  = Lambdas {-# UNPACK #-} !Int (Expr (Bound () a))
  | Var a

所以现在在 lambda 下出现的 Bound 是直接被 lambda 绑定的变量，以及你想在出现中放入的任何类型信息，这里我只是使用了 ()。

现在封闭项在 'a' 中是多态的，如果您按其使用站点对 lambda 的元素进行排序（并且可以确保您始终通过删除未使用的项来规范化 lambda），则 alpha 等效项仅与 (==) 进行比较，并且如果您需要开放条款，您可以使用 Expr String 或其他一些表示形式。

Expr 和 Bound 签名的更具肛门保留性的版本将使用存在类型和类型级别 natural 来识别被绑定的变量的数量，并在 Bound 构造函数中使用“Fin”，但是因为您已经必须维护不变量你绑定的变量不超过 lambda 中出现的 # ，并且类型信息在所有变量中都Var (Bound n _)一致n，维护另一个不是太大的负担。

更新：您可以使用我的bound包以完全独立的方式对此进行改进！

于 2012-02-27T15:31:12.713 回答