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.

翻译：通过将二阶统一问题归约到依赖类型及带有类型构造子的类型化λ演算中，我们证明了其中三阶模式匹配问题的不可判定性。