[Termtools] Haskell libraries for rewriting [ CfP Workshop on Haskell and Rewriting Techniques ]

[Johannes Waldmann]

Dear all,


I'd like to draw your attention to this new workshop
"Haskell and Rewriting Techniques" to be held during RDP.
http://www.imn.htwk-leipzig.de/HART2013/


In addition to the topics mentioned in the CfP,
I think this is a nice opportunity to discuss
Haskell libraries for term rewriting
(as they may be used in termination/complexity provers).

I know of these, at least:
http://cl-informatik.uibk.ac.at/software/tct/projects/termlib/
http://hackage.haskell.org/package/tpdb/
but there may be more, and it may be worthwhile
to announce and compare their goals and properties
as well as possible extensions, mergers, etc.


Let me give a few concrete examples.
Even very basic things are not as simple as they seem.
For instance, perhaps we all agree on

    data Term v s = Var v | Node f [ Term v s ]

but this has at least the following problems:

* with current ghc and libraries,
  one needs to be careful when rendering tree structures,
  cf. http://hackage.haskell.org/trac/ghc/ticket/7666

* if speed is important, deriving (Eq, Ord) is probably
  not a good idea (because "==" and "compare" may visit
  large parts of trees). One could add a hash value (in each Node)
  but even then, equality is expensive (in the positive case).
  One could switch to a term representation with globally
  unique node identifiers -  and has to uglify (monadify)
  all of the program, or rely on unsafePerformIO.

* why  Term v s  and not  Term s v? I put the variable type
  first because then I can write  instance Functor (Term v),
  for mapping symbols, while keeping variables,
  which may be needed more often than the other way around.

* But the type may be wrong altogether,
  and higher order people would probably want
     data Tree s = Node s [ Tree s ]
     type Term v s = Tree (Either v s)


If you have some thoughts on these or other issues,
consider submitting to the workshop.


Best regards - Johannes.



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20130218/4fec6606/attachment.pgp>