【发布时间】：2018-08-24 10:38:25
【问题描述】：
这个问题是基于我的问题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 演算工具，仅具有句法操作？
【问题讨论】：
-
你想在证明的过程中执行这个重写吗？或者您是否要编辑提及
is的现有 Coq 定义，以便它们仅提及IS？ -
请注意，
is boss John在语法上等同于(is(boss))(John)，它比IS(John, boss)更简洁。 Coq 中通常首选链式函数应用程序。 -
我更喜欢两种不同的理论——一种是“is”，另一种是经过转换的——一种是“IS”。我将从 GrammaticalFramework 生成第一个理论，然后我想将其转换为第二个。
-
第二种“IS”形式可以更容易地转换为is-boss谓词，这就是我努力达到它的原因。谓词形式可用于推理 Coq 中机械化的对象逻辑，例如线性逻辑。
-
如果
boss的类型为e -> t，e表示“实体”，t表示布尔值，你不能只使用boss John吗？
标签： coq lambda-calculus coqide coq-plugin