Third-order matching in the presence of type constructors

Abstract

We show that it is decidable whether a third-order matching problem in λω (an extension of the simply typed lambda calculus with type constructors) has a solution or not. We present an algorithm which, given such a problem, returns a solution for this problem if the problem has a solution and returns fail otherwise. We also show that it is undecidable whether a third-order matching problem in λω has a closed solution or not.