Seventh Annual IEEE Symposium on

Logic in Computer Science (LICS 1992)

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

Authors: Dowek, G.


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


    author = 	 {Dowek, G.},
    title = 	 {Third order matching is decidable},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {2--10},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}