3

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

  • σ| e (x n ) = 如果 x n ∈ FV(e) 则 σ(x n ) 否则 x n

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

编辑：

作为参考，这是一个使用有限映射的简单解决方案。每次将限制操作应用于替换 σ 和表达式 e 时，找到 e 的自由变量的集合 FV ( e )。对于σ 域中的每个变量 x n ，如果 x n ∈ FV( e ) 则设置 σ'(x n ) = x n。返回 σ'。假设 σ'(x n ) = x n如果 x n ∉ dom(σ')。

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

4

1 回答 1

4

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

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是专门编写的，其行为类似于整数函数，但允许在单个点进行有效修改（正如人们希望使用替换函数一样）。如果您的变量由整数唯一标识，您可以直接使用它，否则您可以模拟字符串或您正在使用的任何内容的样式。

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

于 2011-10-11T03:25:33.497 回答