Symmetric Transrationals: The Data Type and the Algorithmic Degree of its Equational Theory

We introduce and investigate an arithmetical data type designed for computation with rational numbers. Called the symmetric transrationals, this data type comes about as a more algebraically symmetric modification of the arithmetical data type of transrational numbers [9], which was inspired by the transreals of Anderson et.al. [1]. We also define a bounded version of the symmetric transrationals thereby modelling some further key semantic properties of floating point arithmetic. We prove that the bounded symmetric transrationals constitute a data type. Next, we consider the equational theory and prove that deciding the validity of equations over the symmetric transrationals is 1-1 algorithmically equivalent with deciding unsolvability of Diophantine equations over the rational numbers, which is a longstanding open problem. The algorithmic degree of the bounded case remains open.