3
$\begingroup$

When implementing a term rewriting system, one “optimization” one can do is to represent operators known to have certain equational properties with a more directly representative data structure. For example, one can use lists to represent uses of a binary operator known to be associative, rather than using the naïve syntax tree representation one is forced to use in the absence of any information about an operator.

I thought I recalled a result that stated that there was an algorithm that could take any (finite) set of equational rules about an operator and transform them into a data structure definition specialized for that set of equational rules. However, when I tried to look for this result, I couldn't find anything like it anywhere. Am I not looking hard enough or not in the right places, or did I just imagine this result entirely? If I did imagine it out of thin air, is there any less-powerful result of the same form that is known, or any counter-result that dashes my hopes of such a generic algorithm existing?

$\endgroup$
  • 1
    $\begingroup$ I assume you are thinking about Knuth-Bendix Completion and its improvements. It requires more information than just the equations, and it may not terminate. When it does, though, it effectively gives a term rewriting system that will reduce a term to a normal form at which point simple syntactic equality can be used. That said, I'm not sure there's an easy way to get a clear, compact description of what the set of all normal forms looks like. $\endgroup$ – Derek Elkins left SE Sep 7 '17 at 21:10
3
$\begingroup$

It sounds like what you are asking for is, for a given equational system $\cal E$, to give a canonical representation for equivalence classes modulo $\cal E$.

Indeed, if your signature is the binary operation $\_\cdot\_$, and your equation is $$ (x\cdot y)\cdot z=x\cdot(y\cdot z)$$

then you can represent any element as $a_1\cdot(a_2\cdot(\ldots\cdot a_n)\ldots)$ (where the $a_i$) are atoms. As Derek Elkins points out, a good way to do this is to apply Knuth-Bendix completion to $\cal E$, (possibly) obtaining a rewrite system $\cal R$ that is confluent and terminating and computes, for each term $t$, a unique element that is a representative of $t$'s equivalence class under $\cal E$.

Now it is useful to note that in this case, the set of canonical forms happens to be isomorphic to the data types of lists of atoms. The fact that elements of an algebraic datatype captures the equivalence classes is not obvious, and is not true in general: if you add commutativity, that is the equation $$ x\cdot y = y\cdot x$$ then it's clear that there is no algebraic (first-order) datatype that captures exactly the normal forms, as this is isomorphic to sorted lists of atoms.

A reasonable question is to ask whether there is always such a data structure using dependent types. In particular, there is a version of sorted list using dependent types, namely:

data SortedList =
  Nil : SortedList
  Cons : forall x:Atom, forall l:SortedList , x <= min l -> SortedList 

taking inspiration from this agda code. Note that min needs to be defined on SortedList, making this an inductive-recursive definition, but I'm pretty sure this can be avoided with a little more messiness (say, embedding list into sorted list).

I think the question needs to be made more precise though, because there is a type in extensional dependent type theory such that each element of that type represents exactly one equivalence class: namely, the type of all equivalence classes! It can be defined by

$$ \mathrm{Q}_E:=\{y|\exists x, \overline{x} = y\}$$ where $\overline{x}$ is defined by: $$\overline{x}=\{z| z=_E x\} $$

In general, quotient types are a tricky subject in type theory though, especially without sufficient extensionality, see e.g. Pragmatic Quotient Types by Cyril Cohen.

In conclusion:

  1. In the naive version of your question, the answer is that it is impossible to associate an inductive data type to an equational theory such that each element of the type represents a unique class.
  2. It is sometimes possible to compute a rewrite system which computes a unique representative of that class if the algorithm terminates and succeeds.
  3. When allowing for dependent types, the question becomes more complex and is, I believe, still somewhat open, with some progress.
$\endgroup$
  • $\begingroup$ Thank you! I guess I would refine my question, intent-wise, to intentional dependent type theories, since that seems like the most likely place to find an “interesting” answer. Regardless, this was very helpful. $\endgroup$ – Ptharien's Flame Sep 12 '17 at 18:42

Your Answer

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

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