在可表示原始递归函数的演算中模式匹配问题的不可判定性
计算机科学中的逻辑
2023-06-12 v1
摘要
我们通过将希尔伯特第十问题归约到模式匹配问题，证明了在多态 lambda 演算（如 Girard 的系统 F）以及支持归纳类型的演算（如 Gödel 的系统 T）中，模式匹配问题是不可判定的。更一般地，在一切能以某种精确意义公平表示原始递归函数的演算中，模式匹配均不可判定。
引用
@article{arxiv.2306.05876,
title = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2306.05876},
year = {2023}
}