加载中…
2023-09-21
The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors
Gilles Dowek
文献摘要
We prove the undecidability of the third order pattern matching problem in typed lambda-calculi with dependent types and in those with type constructors by reducing the second order unification problem to them.
讨论
0讲解博客
生成讲解博客的中文版本
AI智能校验
生成AI智能校验的中文版本