# 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.

• Thank you for the reply. I also found this other reference: ac.els-cdn.com/S0304397596001739/… by van Oostrom, in particular Corollary 28. Here the hypotheses of left linearity and development closed seem to yield confluence without termination. What I find confusing is that the reduction is on normal forms modulo beta (or beta-eta), and it's not clear that if I want to make beta and eta rewrites, what else I need to get confluence. – Jonathan Gallagher Oct 9 '17 at 19:33
• @JonathanGallagher I wonder if you're not confusing the internal $\beta$-reductions (and $\eta$-expansions) with the rules called $\beta$ and $\eta$, defined by pattern matching on the defined constants $\mathrm{app}$ and $\mathrm{abs}$ respectively. The first is used to define higher-order terms and their semantics, the second is used to study rewrite systems and their confluence inside the theory of rewrite rules. It's a slightly subtle point. – cody Oct 10 '17 at 2:53
• Yes, I think I am very much confusing that point! Is there a reference that treats this delicately, or is it sufficient to simply note that the internal and external reductions are independent? – Jonathan Gallagher Oct 11 '17 at 0:36
• @JonathanGallagher I'm not sure of any reference that details this complication, unfortunately, though it might be useful to note that the internal rules are done on simply-typed terms, and so is rather well behaved (terminating, confluent, and admits $\eta$-long forms). – cody Oct 11 '17 at 2:57