I try to read the paper by Prof. Fateman mentioned previously. Hcons are
easy to obtain, uconsalt.lisp from MockMMA project works for me:
(C1) load(uconsalt)$
(C2) q1:sin(x)$
(C3) q2:q1$
(C4) ?eq(q1,q2);
(D4) TRUE
(C5) q2:sin(x)$
(C6) ?eq(q1,q2);
(D6) FALSE
(C7) q1:?uniq(q1);
(D7) SIN(x)
(C8) q2:?uniq(q2);
(D8) SIN(x)
(C9) ?eq(q1,q2);
(D9) TRUE
But the tagging procedure is still unclear to me. Should the tags be
placed in cdar? What does the binary search tree contain exaclty? Are
there any examples/drafts available?
--
Andrei Zorine