Higher order pattern matching problems are equations in the form F X = B, to be solved for X up to convertibility, in the simply typed lambda calculus. They arise in e.g. the computer implementation of higher order logics. The decidability of these problems is a long-standing open question, raised by Huet in 1977.

Work of Padovani, Schmidt-Schauss and myself led to a very elegant presentation of the minimal model of the simply typed lambda calculus, and to corresponding algorithms for "atomic" higher order matching. This presentation is in terms of certain combinators, which can be viewed as representing strategies in certain games.

Building on this, I give extensions of these constructions to effectively present models in which any higher-order matching problem can be faithfully represented. This reduces the decidability of higher-order matching to the very plausible conjecture that definability in the models in question is decidable.