haskell - 具有无限域的映射(替换)

Question

有限域的有限 map 模型替换。我要么需要模拟无限域的替换操作，要么找到一种合适的方法来表示无限域的替换。例如，考虑替换的限制操作:

• σ|_e(x_n) = 如果 x_n ∈ FV(e) 则 σ(x_n)子>) 否则 x_n

由于限制操作适用于可能无限的集合中的所有变量，因此像有限映射这样的数据类型无法“向前”预测添加新绑定(bind)时的限制。当然，使用具有无限域的有限映射会导致不终止。有没有一种方法可以模拟操作，例如使用有限映射的限制，或者另一种替换表示，允许人们轻松地编写诸如限制之类的操作？我觉得我忽略了一个明显的解决方案 - 例如，利用惰性求值或函数替换。

编辑:

作为引用，这里是使用有限映射的简单解决方案。每次对替换 σ 和表达式 e 应用限制运算时，求 e 的自由变量的集合 FV(e)。对于 σ 域中的每个变量 x_n，如果 x_n ∈ FV(e)，则设置 σ'(x_n ) = x_n.返回 σ'。假设 σ'(x_n) = x_n 如果 x_n ∉ dom(σ')。

编辑:这是我忽略的明显解决方案。

Answer 1

嗯，最直接的替换模型就是函数本身。

newtype Subst = Subst { apply :: Var -> Expr }

singleton :: Var -> Expr -> Subst
singleton v e = Subst (\v' -> if v == v' then e else Var v')
-- etc.

对于实现语言的第一步，这可能是我在有限映射崩溃后立即使用的。它并不快(当 n 是域的大小时，需要 O(n) 时间)，但它很简单。将其封装起来，以便稍后更换。

如果你开始遇到 O(n) 时间问题，那么你可以切换到 trie。 data-inttrie是专门编写的，其行为就像整数上的函数一样，但允许在单点上进行有效的修改(就像人们希望使用替换函数一样)。如果您的变量由整数唯一标识，您可以直接使用它，否则您可以模拟字符串或您正在使用的任何内容的样式。

但在我看来，你需要“向前看”也很奇怪。我在我的语言实现中从来不需要这个；如果将新绑定(bind)添加到受限替换，则该限制不会应用于新绑定(bind)(如果适用，则语义将是错误的)。当我没有做一些 absurd 的奇怪的事情时(而且那些通常不会成功)，有限 map 已经在所有情况下完成了技巧。