Symmetric Transrationals: The Data Type and the Algorithmic Degree of its Equational Theory - John Tucker (Lecture Notes in Computer Science, 2022)
We introduce and investigate an arithmetical data typedesigned for computation with rational numbers. Called the symmetrictransrationals, this data type comes about as a more algebraicallysymmetric modification of the arithmetical data type of transrationalnumbers [9], which was inspired by the transreals of Anderson et.al. [1].We also define a bounded version of the symmetric transrationals therebymodelling some further key semantic properties of floating point arithmetic.We prove that the bounded symmetric transrationals constitutea data type. Next, we consider the equational theory and prove thatdeciding the validity of equations over the symmetric transrationals is1-1 algorithmically equivalent with deciding unsolvability of Diophantineequations over the rational numbers, which is a longstanding openproblem. The algorithmic degree of the bounded case remains open.