Higher order rewriting theory and critical pairs with the beta rule

In a higher-order pattern rewrite system, one specifies rewrites on beta
normal forms of terms. Is it possible to have a rewrite like:

$\gamma := \lambda x . F(m) \to F(\lambda x . m)$

for some function symbol $F$ and $m$ in $\beta$-normal form? If so, then there is a "critical pair" between $\gamma$ and $\beta$

$F(m) [t/x] \leftarrow (\lambda x . F(m)) t \rightarrow (F(\lambda x .m )) t $

On the other hand, is there any reason to require $\gamma$ go the other direction?:

$F(\lambda x . m) \to \lambda x . F(m)$

This would avoid critical pairs with $\beta$, but may in practice be less natural.

If the former is possible, can one still conclude confluence if all critical pairs are development closed?

The theory of higher-order critical pairs can indeed handle this example, as outlined in the following article:

Higher-Order Rewrite Systems and their Confluence, Richard Mayr & Tobias Nipkow

There are several different notions of higher-order rewrite systems, and several of them are able to handle your example, including those of the paper.

The critical pair lemma is still true: if every critical pair is development closed, and the system is terminating, then one can conclude that it is confluent. The second condition is necessary though, in particular, $\beta$-reduction on untyped terms can muck things up.

This means that completion is still a meaningful operation in this setting.

At any rate, your second rule seems a bit more natural in a termination context, where $F$ is "pushed towards the leaves", but obviously it depends on the meaning of the symbol.

StackExchange Computer Science Q#82118, answer score: 3