## Paper: Third order matching is decidable (at LICS 1992)

**Gilles Dowek**

### Abstract

The problem of determining whether a term is an instance of another in the simply typed λ-calculus, i.e. of solving the equation a=b where a and b are simply typed λ-terms and b is ground, is addressed. An algorithm that decides whether a matching problem in which all the variables are at most third order has a solution is given. The main idea is that if the problem a=b has a solution, then it also has a solution whose depth is bounded by some integer s depending only on the problem a=b, so a simple enumeration of the substitutions whose depth is bounded by s gives a decision algorithm. This result can also be used to bound the depth of the search tree in Huet's semi-decision algorithm and thus to turn it into an always-terminating algorithm. The problems that occur in trying to generalize the proof given to higher-order matching are discussed

### BibTeX

@InProceedings{Dowek-Thirdordermatchingi, author = {Gilles Dowek}, title = {Third order matching is decidable}, booktitle = {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)}, year = {1992}, month = {June}, pages = {2--10}, location = {Santa Cruz, CA, USA}, publisher = {IEEE Computer Society Press} }