coq - 如何在 Coq 中进行高阶项重写？

Question

这个问题是基于我的问题https://cs.stackexchange.com/questions/96533/how-to-transform-lambda-function-to-multi-argument-lambda-function-and-how-to-re有该问题中的两个功能和两个术语：

功能：

is: (e->t)->(e->t)
IS: e->(e->t)->t

条款：

(is(boss))(John): t
IS(John, boss): t

我的问题是：如何重写涉及is只有 的术语的术语IS？Coq（或第三方工具）是否有这样的重写功能？Coq 是否有工具来检查重写条款的相等性？

也许这样的重写可以在 Coq 世界之外完成，也许还有其他纯粹的 lambda 演算工具仅具有句法操作？

Answer 1

没有工具可以对您直接描述的 Coq 代码进行那种文本转换。在不了解 GrammaticalFramework 的情况下，我想您最好的选择是编写一个 Sed 脚本，该脚本查找is应用于参数的出现，并用IS.

第二种“IS”形式可以更容易地转换为 is-boss 谓词，这就是我努力达到它的原因。

我认为，如果您使用 Sed 脚本，您可以IS_BOSS直接访问表单，而无需使用IS.