Suppose one has two rewrite rules $\to^\eta,\to^\beta$, both of which are confluent and such that $\to^A := \to^{(\eta \cup \beta)}$ is also confluent. Define a $\beta$-normal form relative to $\eta$ to be $m$ such that

  • $m$ is a $\beta$ normal form;
  • $m \to^\eta n$ implies $n \to_{\beta}^* m$

One may think of $\to^\eta$ as being some kind of expansion that could prevent any term from having an $\to^A$ normal form.

Does anyone know of a definition like this, and/or nice properties such as: "relative normal forms if they exist are unique."

One can show that if $\eta$ requests $\beta^*$ : i.e. if there is a divergence between $n \to^\eta n'$ and $n \to_{\beta}^* n''$ then there is a join $n' \to_{\beta}^* m$ and $n'' \to^\eta \cdot \to_\beta^* m$, then relative normal forms (if they exist) are unique.

In fact, one can show that if the confluence of $\to^A$ is proved by decreasing diagrams with $\eta$ bigger than $\beta$, then again the property holds. Essentially one proves the following first: if $m$ is a relative normal form with

$\newcommand{\ra}[1]{\kern-1.5ex\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} \newcommand{\ras}[1]{\kern-1.5ex\xrightarrow{\ \ \smash{#1}\ \ }\phantom{}\kern-1.5ex} \newcommand{\da}[1]{\bigg\downarrow\raise.5ex\rlap{\scriptstyle#1}} \begin{array}{c} s & \ra{\eta} & t \\ \da{\beta^*}\\ m \end{array}$

then $t \to_\beta^* m$.

The above then implies that any $\to^A$ sequence leaving a relative normal form will return by a $\beta$ sequence. This in turn, along with the confluence of $\to^A$ can be used to show that relative normal forms are unique.

I can certainly fill in the details if anyone likes; however, this seems like something that should be generally true. Does anyone know of any such results or counterexamples?



Your Answer

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