Neat! That particular bijection's well-know to those who know it, but I hadn't seen the pairing function before.
The pairing function is similar to Cantor's surjective mapping from integers to rationals, and appears in a footnote of The Emperor's New Mind (Penrose). (I re-discovered this pairing when I wanted a way to express an unbounded two-dimensional array of bits in an unbounded one- dimensional array, by converting between the pair of indices and a single index. This was necessary for me to store an unbounded array of naturals, which are themselves unbounded binary strings, in a one-dimensional tape for a computer in Conway's Game of Life.)
You may also enjoy Chris Barker's Iota, Jot and Zot: http://semarch.linguistics.fas.nyu.edu/barker/Iota/
Thank you very much! I only had a broken link before to Iota and Jot, and had never even heard of Zot.
as well as John Tromp's Binary Lambda Calculus and Binary Combinatory Logic: http://homepages.cwi.nl/~tromp/cl/cl.html
Yes, I've seen this before. Very elegant! (I prefer BCL to BLC, as it is simpler, despite being less efficient.)
My own design, Keraia, is here: http://arxiv.org/abs/cs/0508056
Ooh, interesting! I like your approach of considering Turing machines as being functions between strings, rather than the original formulation (which includes the state and position of the read/write head). Sincerely, Adam P. Goucher