摘要：高阶匹配问题是在简单类型λ-演算中确定术语是否是另一个术语的实例的问题，即解决方程a = b，其中a和b是简单类型λ-术语且b是基础的。该问题的可判定性仍然尚未确定。我们证明了变量在问题中最多是三阶的特殊情况的可判定性。
作者：Gilles Dowek
论文ID：2306.01473
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-05
PDF 下载： 英文版 中文版pdf翻译中