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

Authors: 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}
  }