oooh, heavyweight maths, delicious.. ++

just want to point out a couple of things - first, a minor ommission, at the top you want norm(z) < norm(y)
second, I was commenting on the impossibility to define that for general groups - looking at the cyclic group generated by y and its coset generated by x, there's no obvious element to be called 'the remainder'. When you go to rings, things are different, indeed.

my algebra is a little rusty by now, but I think you need your principal ideal ring to be an integral domain as well, before you get UFD ( ie, no Z_6 and the like ), this relating to your second paragraph.. Looking further down, I see that you talk about domains only, so fair enough, and we don't want to look at ugly non-domain PIRs anyway..

I think the issue with multivariate polynomials is that they are UFDs, but definitely not PIDs ( e.g. <x,y^2> ), but in any case, now I'm just getting depressed realizing how much I've forgotten, so I'll drop it here, and go back to my leaking recursive closures...