¿Es posible probar algorítmicamente si un número computable es racional o entero? En otras palabras, ¿sería posible que una biblioteca que implementa números computables proporcione las funciones isIntegero isRational?
Supongo que no es posible, y que esto está relacionado de alguna manera con el hecho de que no es posible probar si dos números son iguales, pero no veo cómo demostrarlo.
Editar: Un número computable viene dado por una función que puede devolver una aproximación racional de con precisión : , para cualquier . Dada tal función, ¿es posible probar si o ?
                    
                        computability
                                computing-over-reals
                                lambda-calculus
                                graph-theory
                                co.combinatorics
                                cc.complexity-theory
                                reference-request
                                graph-theory
                                proofs
                                np-complete
                                cc.complexity-theory
                                machine-learning
                                boolean-functions
                                combinatory-logic
                                boolean-formulas
                                reference-request
                                approximation-algorithms
                                optimization
                                cc.complexity-theory
                                co.combinatorics
                                permutations
                                cc.complexity-theory
                                cc.complexity-theory
                                ai.artificial-intel
                                p-vs-np
                                relativization
                                co.combinatorics
                                permutations
                                ds.algorithms
                                algebra
                                automata-theory
                                dfa
                                lo.logic
                                temporal-logic
                                linear-temporal-logic
                                circuit-complexity
                                lower-bounds
                                permanent
                                arithmetic-circuits
                                determinant
                                dc.parallel-comp
                                asymptotics
                                ds.algorithms
                                graph-theory
                                planar-graphs
                                physics
                                max-flow
                                max-flow-min-cut
                                fl.formal-languages
                                automata-theory
                                finite-model-theory
                                dfa
                                language-design
                                soft-question
                                machine-learning
                                linear-algebra
                                db.databases
                                arithmetic-circuits
                                ds.algorithms
                                machine-learning
                                ds.data-structures
                                tree
                                soft-question
                                security
                                project-topic
                                approximation-algorithms
                                linear-programming
                                primal-dual
                                reference-request
                                graph-theory
                                graph-algorithms
                                cr.crypto-security
                                quantum-computing
                                gr.group-theory
                                graph-theory
                                time-complexity
                                lower-bounds
                                matrices
                                sorting
                                asymptotics
                                approximation-algorithms
                                linear-algebra
                                matrices
                                max-cut
                                graph-theory
                                graph-algorithms
                                time-complexity
                                circuit-complexity
                                regular-language
                                graph-algorithms
                                approximation-algorithms
                                set-cover
                                clique
                                graph-theory
                                graph-algorithms
                                approximation-algorithms
                                clustering
                                partition-problem
                                time-complexity
                                turing-machines
                                term-rewriting-systems
                                cc.complexity-theory
                                time-complexity
                                nondeterminism
                                
                    
                    
                        dbarbosa
fuente
                
                fuente

Respuestas:
Es fácil confundirse acerca de lo que significa "representar" o "implementar" un número real. De hecho, estamos presenciando una discusión en los comentarios donde la representación es contenciosa. Así que déjame abordar esto primero.
¿Cómo sabemos que una implementación es correcta?
La teoría que explica cómo representar cosas en una computadora es la realizabilidad . La idea básica es que, dado un conjunto , elegimos un tipo de datos τ y para cada x ∈ X un conjunto de valores de tipo τ que lo dan cuenta. Escribimos v ⊢ x ∈ X cuando v es un valor que realiza x . Por ejemplo (usaré Haskell sin una buena razón), una implementación sensata de N podría ser el tipo de datos donde v ⊢ k ∈ N cuando vX τ x∈X τ v⊢x∈X v x N v⊢k∈N v evalúa el número  (por lo tanto, en particular , no representa un número natural, y tampoco lo hace un programa divergente). Pero algún bromista podría pasar y sugerir que usemos para representar números naturales con T r u e F a l s e ⊢ n ∈ N para n ≠ 42 . ¿Por qué es esto incorrecto? Necesitamos un criterio .k¯¯¯ True⊢42∈N False⊢n∈N n≠42 
Integer-42BoolyEn el caso de los "números comodín", la observación fácil es que no se puede implementar la suma. Supongamos que le digo que tengo dos números, ambos representados por . ¿Puedes dar un realizador por su suma? Bueno, eso depende de si la suma es 42, pero no se puede saber. Dado que la suma es una "parte esencial de lo que son los números naturales", esto es inaceptable. En otras palabras, la implementación no se trata de conjuntos, sino de estructuras , es decir, tenemos que representar conjuntos de tal manera que sea posible implementar también la estructura relevante. Déjame enfatizar esto:False 
Si no cumple con este principio, debe sugerir un criterio matemático alternativo de corrección. No se de uno.
Ejemplo: representación de números naturales.
Para los números naturales, la estructura relevante es descrita por los axiomas de Peano, y el axioma crucial que debe implementarse es la inducción (pero también , sucesor, + y × ). Podemos calcular, utilizando la realizabilidad, lo que hace la implementación de la inducción. Resulta ser un mapa (dondeestá el tipo de datos aún desconocido que representa los números naturales)0 + × 
natsatisfactorioX↦1+X 
induction x f zero = xyinduction x f (succ n) = f n (induction x f n). Todo esto surge de la realizabilidad. Tenemos un criterio: una implementación de números naturales es correcta cuando permite una implementación de axiomas de Peano. Un resultado similar se obtendría si se utilizó la caracterización de los números como el álgebra inicial para el funtor .Correcta implementación de números reales
Volvamos la atención a los números reales y la pregunta en cuestión. La primera pregunta es "¿cuál es la estructura relevante de los números reales?" La respuesta es: Archimedean Cauchy completa el campo ordenado . Este es el significado establecido de "números reales". No puede cambiarlo, otros lo han arreglado para usted (en nuestro caso, los reales alternativos de Dedekind resultan ser isomorfos a los reales de Cauchy, que estamos considerando aquí). No puede quitarle ninguna parte. no puede decir "No me importa implementar la adición" o "No me importa la orden". Si hace eso, no debe llamarlo "números reales", sino algo así como "números reales donde olvidamos el orden lineal".
No voy a entrar en todos los detalles, pero permítanme explicarles cómo las diversas partes de la estructura ofrecen varias operaciones en reales:
lim : (nat -> real) -> realque toma una (representación de) secuencia rápida de Cauchy y devuelve su límite. (Una secuencia es rápida si | x n - x m | ≤ 2 min ( n , m )Que hacemos no obtenemos es una función de prueba para la igualdad. No hay nada en los axiomas para los reales que pida que sea decidible. (En contraste, los axiomas de Peano implican que los números naturales son decidibles, y puede probarlo implementando el uso solo como un ejercicio divertido).= 
eq : nat -> nat -> BoolinductionEs un hecho que la representación decimal habitual de los reales que usa la humanidad es mala porque con ella ni siquiera podemos implementar la suma. El punto flotante con mantisa infinita también falla (ejercicio: ¿por qué?). Sin embargo, lo que funciona es la representación de dígitos con signo , es decir, una en la que permitimos dígitos negativos y positivos. O podríamos usar secuencias de racionales que satisfagan la prueba rápida de Cauchy, como se indicó anteriormente.
La representación de Tsuyoshi también implementa algo, pero noR 
Consideremos la siguiente representación de números reales: una verdadera está representada por un par ( q , b ) donde ( q n ) n es una secuencia de Cauchy rápida convergiendo a x y b es un valor booleano que indica si x es un entero. Para que esto sea una representación de los reales, tendríamos que implementar la suma, pero resulta que no podemos calcular las banderas booleanas. Entonces esto no es una representación de los reales. Pero todavía representa algo, es decir, el subconjunto de los reales Z ∪ ( R ∖ Z )x (q,b) (qn)n x b x Z∪(R∖Z) . De hecho, de acuerdo con la interpretación realizabilidad una unión se lleva a cabo con una bandera que indica qué parte de la unión que estamos. Por cierto,  es un no igual a R , a menos que crea en medio excluido, lo cual no se puede implementar y, por lo tanto, es bastante irrelevante para esta discusión. Las computadoras nos obligan a hacer cosas intuitivamente.Z∪(R∖Z) R 
No podemos probar si un real es un entero
Finalmente, déjame responder la pregunta que se hizo. Ahora sabemos que una representación aceptable de los reales es una de las rápidas secuencias de racionales de Cauchy. (Un teorema importante afirma que dos representaciones de reales que son aceptables son en realidad computacionalmente isomorfas).
Teorema: probar si un real es un entero no es decidible.
Prueba. Supongamos que pudiéramos probar si un real es un entero (por supuesto, el real se realiza mediante una secuencia rápida de Cauchy). La idea, que le permitirá probar un teorema mucho más general si lo desea, es construir una secuencia de Cauchy rápida de no enteros que converja a un entero. Esto es fácil, solo toma x n = 2 - n . A continuación, resuelva el problema de detención de la siguiente manera. Dada una máquina Turing T , defina una nueva secuencia ( y n ) n por y n = { x n si(xn)n xn=2−n T (yn)n  
Es decir, las nuevas miradas de secuencia como la secuencia(xn)n, siempre y cuandoTcarreras, pero luego se queda "atrapado" enxmsiT sedetiene en el pasom. Muy importante, la nueva secuencia también es una secuencia rápida de Cauchy (y podemos probar esto sin saber siT sedetiene). Por lo tanto, podemos calcular su límitez=limnyn
Ejercicio: adapte la prueba anterior para mostrar que no podemos probar números racionales. Luego, adáptelo para mostrar que no podemos probar nada no trivial (esto es un poco más difícil).
A veces las personas se confunden con todo este negocio de pruebas. Piensan que hemos demostrado que nunca podemos probar si un real es un número entero. Pero seguramente, 42 es real y podemos decir si es un número entero. De hecho, cualquier real particular que se nos ocurra, , 88 ln 89 , e π √sin11 88ln89  , etc., podemos decir perfectamente si son enteros. Precisamente,podemosdecirlo porquetenemosinformación adicional: estos reales no se nos dan como secuencias, sino como expresiones simbólicas a partir de las cuales podemos calcular el bit Tsuyoshi. Tan pronto como la única información que tenemos sobre lo real es una secuencia de aproximaciones racionales que convergen a la misma (y yonosignifica una expresión simbólica que describe la secuencia, pero un cuadro negro que da salida a laNtérmino -ésima en la entradaneπ163√ n n  ) entonces será tan indefenso como las máquinas.
La moraleja de la historia
No tiene sentido hablar sobre la implementación de un conjunto a menos que sepamos qué tipo de operaciones queremos realizar en él.
fuente
Tiendo a pensar que esto es indecidible:
Sea un número irracional computable. Considere una MT M . Puede construir una función que ejecute M en ϵ , y en paralelo calcula x con precisión creciente. Si M se detiene, deja de calcular x , de lo contrario continúa.x M M ϵ x M x 
Decidir si esta función calcula un número racional es equivalente al problema de detención.
fuente
Suponiendo que un real se da como una secuencia de aproximaciones racionales con el error delimitado por alguna función computable conocida que tiende a cero (todas esas aproximaciones son equivalentes y corresponden a la topología habitual en los reales).
Las funciones computables son continuas. IsRational e IsInteger no son continuos y, por lo tanto, no son computables.
EsEntero es semi -computable: existe un procedimiento que con el tiempo de salida "falso" si la entrada no es un entero, pero siempre se ejecutará si la entrada es un entero. Este procedimiento simplemente analiza cada aproximación y comprueba si hay un número entero dentro del límite de error. Esta función es continua cuando usamos la topología de Sierpiński en {verdadero, falso} (es decir, {falso} es un conjunto abierto pero {verdadero} no lo es).
fuente
Es indecidible si un número computable dado es igual a cero .
(¿Entonces su oráculo de aproximación racional devuelve 0 por cada ε que ha intentado? Tal vez simplemente no le haya dado un ε lo suficientemente pequeño).
Por lo tanto, es indecidible si un número computable dado entre -½ y + ½ es un número entero.
fuente
Una función que es computable es más fuerte que la función que es continua, es decir, cualquier función computable debe ser continua en la topología de la información.
Desea ver si la función definida porF:R→{Yes,No} 
es computable
Entonces su función no es continua y, por lo tanto, no es computable.
La prueba de que cualquier función computable debe ser continua es similar.
fuente