Cannonical output

[sorry to come in here, but I couldn't resist]

> The basic idea is that you compare (for ordering) two anonymous nodes as
> a function
> of the properties they have, which often ends up being very recursive,
> and in screw cases, being circular.  You can, afetr all, have a graph
> which is syymetric in the two arbitrary names _:a and _:b.

that's exactly what we do while mathing bnodes
with some (Java) code [1] which should be refactored

///
  final boolean unify(Euler t, Euler r, stack s) {
    if (t == null) return false;
    if (ref != null && object == null) return ref.unify(t, r, s);
    if (t.ref != null && t.object == null) return unify(t.ref, r, s);
    if (bound && t.bound) {
      if (varid != -1) {
        Euler el = new Euler();
        Euler ev = t.deref();
        el.verb = ev.verb;
        el.cverb = ev.cverb;
        el.varid = ev.varid;
        el.bound = ev.bound;
        if (!deref().unify(el, r, s)) return false;
      }
      if (subject == null && t.subject == null && object != null &&
t.object != null) {
        Euler el = this;
        Euler elt = t;
        if (s == null) {  // no stack
          while (el != null && elt != null) {
            el = el.near;
            elt = elt.near;
          }
          if (el != null || elt != null) return false;
          el = this;
          elt = t;
        }
        while (elt != null) {
          el = this;
          while (el != null) {
            if (bound && t.bound && (elt.verb == null ||
                el.verb != null && el.deref().verb == elt.deref().verb)) {
              if (el.object != null && !el.object.unify(elt.object, r, s))
{
                if (r.uniq.get(el.deref().verb) != null) return false;
              }
              else break;
            }
            el = el.near;
          }
          if (el == null) return false;
          elt = elt.near;
        }
      }
      else {
        if (varid == -1 && verb != null && t.verb != null && deref().verb !
= t.deref().verb) return false;
        if (subject != null && !subject.unify(t.subject, r, s)) return
false;
        if (object != null && !object.unify(t.object, r, s)) return false;
      }
      return true;
    }
    if (bound) return t.unify(this, r, s);
    if (s != null) {
      if (subject != null && !subject.unify(t.subject, r, s)) return false;
      if (object != null && !object.unify(t.object, r, s)) return false;
      deref().ref = t;
      bound = true;
      s.push(this, 0);
    }
    return true;
  }
///

and such a bnode funtional term is an Euler object with
subject == null and object != null tied together with near links
and indeed the matching (unification) is very recursive
(actually 9 times unify within unify I just see)

--
Jos De Roo

[1](See attached file: Euler.java)(See attached file: Parser.java)

Received on Friday, 24 May 2002 06:46:40 UTC