kframework - K 中的 Alpha 等价比较？

Question

两个 K 项之间是否有内置的结构等价和 alpha 等价比较？

由于似乎有一个替代模块可以进行 alpha 转换，我想知道是否有一个等效模块。

如果没有，是否有可能以从被检查的特定语法中抽象出来的方式定义这样一个函数？例如，使用解析器的活页夹注释来检查任何两个术语，但是语法定义了它们。

Answer 1

您似乎指的是 KVar 排序、SUBSTITUTION 模块和 binder 属性，它们一起用于在依赖于此的语言中实现变量捕获感知替换，例如 lambda 演算。目前，==K 对于包含 binders 的术语的行为是两个 binder 只有在术语 bound 具有相同名称时才会比较相等。与自由变量和绑定变量在绑定器中的出现不同，它们比较相等，如果它们引用相同的变量，绑定器本身的变量名称（当前）不知道 alpha 转换，并将根据它们的名称进行比较. 因此，例如，lambda x . x将比较等于lambda x . x，而不是lambda y . y。

话虽如此，没有什么能阻止您编写一个遍历包含绑定器的表达式并规范化其变量名称的函数。然后，您可以用两个不同的术语调用它，并使用 ==K 比较每个术语的结果。然后，结果比较将比较两个表达式是否相等模重命名。一种简单的方法是用它所在的嵌套绑定器的级别数重命名每个绑定器的变量，例如，lambda _1 . ((lambda _2 . _2) (lambda _2 . _1))。

如果您尝试此方法并遇到您认为不正确的崩溃或行为，请随时在 GitHub 上提交问题。我将优先修复报告的任何错误。