Linear interpolation for the higher-order matching problem

Abstract

We present here a particular case of the higher order matching problem. the linear interpolation problem. The problem consists in solving a collection of higher order matching equations of the shape xM1… Mk = N, where x is the only unknown quantity. We prove recursive equivalence of the higher order matching problem and the linear interpolation problem. We also investigate decidability of a special case of the fifth order linear interpolation problem. The restriction we consider consists in that arguments of variables from the main abstraction in terms M1,… Mk cannot contain variables from the main abstraction.