Higher-order associative commutative pattern matching for component retrieval

In this paper we describe a higher-order associative commutative pattern matching algorithm. We are motivated by the need for developing tool support for matching user requirements against library component interfaces, both specified using a formal language. In developing such tool support we aim for a maximum level of recall, while at the same time maintaining a reasonable level of automation and effciency. In order to support adaptation of library components we assume the library components may contain higher-order parameters (representing types, functions and relations) - components are adapted by instantiating parameters to suit the requirements of the user. However with this assumption, the usual specification matching techniques, based on proving equivalence using a theorem prover based on first-order logic, are no longer useful in general. We therefore propose building tool support based on pattern matching, and increasing recall by providing (partial) support for matching expressions that can be shown to be equivalent by applying the laws of associativity and commutativity