Hi! not touching the partiality issue the answer to the question about decidability is positive. Decidability follows from the results, proved in our paper "Kleene Monads: Handling Iteration in a Framework of Generic Effects", accepted for the upcoming CALCO conference. The paper should be soon available on my homepage: http://www.informatik.uni-bremen.de/~sergey/papers_e.htm It does contain a confluent and strongly normalising rewrite system but the proof details will show up (hopefully) only in the journal version. The proofs are also included into my PhD thesis, which is under development and thus still unpublished but in case of interest I can make available some parts of it containing the proofs under discussion. Best regards, -------------------------------------- Sergey Goncharov Junior Researcher DFKI Bremen Safe and Secure Cognitive Systems Cartesium, Enrique-Schmidt-Str. 5 D-28359 Bremen phone: +49-421-218-64276 Fax: +49-421-218-9864276 mail: Sergey.Goncharov@dfki.de www.dfki.de/sks/staff/sergey -------------------------------------- ------------------------------------------------------------- Deutsches Forschungszentrum für Künstliche Intelligenz GmbH Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern Geschäftsführung: Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender) Dr. Walter Olthoff Vorsitzender des Aufsichtsrats: Prof. Dr. h.c. Hans A. Aukes Amtsgericht Kaiserslautern, HRB 2313 ------------------------------------------------------------- [For admin and other information see: http://www.mta.ca/~cat-dist/ ]