Are there any known reversible pairing functions $f: \mathbb N \times \mathbb N \to \mathbb N$ that can be computed in constant time (FAC⁰)?



Are there any pairing functions computable in constant time (AC⁰) 
Interleaving the binary encodings of the two numbers a and b seems to be the best solution:


For example the encoding of   

a = 20d = 10100b  

b = 5d = 101b  

We interleave the bits starting with the least significant bits (we pad shorter numbers with 0's so they are the same length).  

The resulting paired number is 0100110010b = 306d


This pairing function can be computed and reversed by a constant depth (depth 1?) circuit and so is in FAC0.


See:  

 - <http://mathworld.wolfram.com/PairingFunction.html>  

 - Pigeon, P. Contributions à la compression de données. Ph.D. thesis. Montreal, Université de Montréal, 2001. (page 115) 


