Subject: Re: representing terms canonically

From: "Richard A. O'Keefe" <[email-masked]>
Date: Thu, 10 Aug 2000 13:31:43 +1200 (NZST)

* no loss of information
	    + an equivalent term should be reconstructable from the foreign repn.
	      (I can do this :-)
	    + preserve internal order of any variables (I can see how to do this)
	
	 * compactly
	    + cyclic terms have finite representations
	    + recombinant terms are not "exploded"
	    + common atoms, variables (of course) and subterms are factored out
	
	 * canonically
	    + all (inc. cyclic) terms denoting the "same" term (apart from renaming
	      of variables) have a single common representation
	
	I suspect it is obvious to some others that canonical repn of
	cyclic terms is in general impossible, or infeasible to compute?

We can number the variables canonically by doing a left-to-right
depth-first traversal, marking nodes as we go.

A possibly cyclic term is a node-labelled edge-labelled digraph:
- some nodes are labelled with variables (_1 ... _N) or with
  non-symbolic constants (numbers, say).
  Those nodes have no out-edges.
- some nodes are labelled with atoms.
  Those nodes have out-edges labelled 1...N, where N is the arity
  of the functor concerned.  (I incluude N=0 here.)

Let's restructure that slightly.  Move the labels out of the
nodes onto edges. 	            0/x
	(x)		=>	( ) ---> (*)		(*) is the end state
             n                      n/x 
	(x) ---> (y)	=>	( ) ---> ( ) --->
What we get is a deterministic finite state automata.
(*) is the unique final state.
Symbols are 0/Var 0/Number 0/Atom or ArgNo/Atom pairs.

Given a deterministic finite state automaton of this form,
we can reconstruct a possibly cyclic term.

Two cyclic terms are equivalent if and only if the corresponding
finite state automata generate the same language (because the language
generated characterises the set of possible paths through a term).

So the following procedure is guaranteed to find a canonical
representation for terms:
	enumerate all deterministic finite state automata
	with the right label set (which is fixed and finite!)
	in some canonical order (there are only countably many
	and they _can_ be enumerated), and stop when you have
	one that is equivalent to the term you started with.

The rest is a small matter of programming.

I don't know whether automaton minimisation would yield a canonical
form, but it sounds like a good thing to try.