Is it possible to define a MACHINE configuration with a 64 Bit kernel and 32 Bit user space ?

The user space should not be using a  x32 ABI.

Thank you!

best regards