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 回答