4
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – Jonathan Gallagher
    Commented Oct 9, 2017 at 19:33
  • 1
    $\begingroup$ @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. $\endgroup$
    – cody
    Commented Oct 10, 2017 at 2:53
  • $\begingroup$ 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? $\endgroup$
    – Jonathan Gallagher
    Commented Oct 11, 2017 at 0:36
  • $\begingroup$ @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). $\endgroup$
    – cody
    Commented Oct 11, 2017 at 2:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.