3
$\begingroup$

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?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.