|
Abstract : |
Abstract. Second-order uni cation is undecidable in general. Miller showed that uni cation of so-called higher-order patterns is decidable and unitary. Weshow that the uni cation of a linear higher-order pattern s with an arbitrary second-order term that shares no variables with s is decidable and nitary. A few extensions of this uni cation problem are still decidable: unifying two second-order terms, where one term is linear, is undecidable if the terms contain bound variables but decidable if they don't. 1, |
