Decidible

En informática teórica , una propiedad se denomina decidible en un conjunto (también recursivamente , recursivamente derivable ) si existe un procedimiento de decisión para ello. Un procedimiento de decisión es un algoritmo que puede responder por cada elemento del conjunto si tiene la propiedad o no. Si "no" tal proceso de toma de decisiones, entonces la propiedad se llama indecidible . Un problema de decisión es la cuestión de si y cómo se puede formular un procedimiento de decisión para una propiedad dada.

Si bien las propiedades sintácticas más importantes de los programas son decidibles, en general, según el teorema de Rice, cualquier propiedad semántica (no trivial) de los programas es indecidible, por ejemplo, la terminación de un programa en una entrada ( problema de retención ) o la igualdad funciones de dos programas ( problema de equivalencia ).

Originalmente destinado específicamente a la validez de fórmulas, el término ahora se usa para cualquier propiedad en conjuntos contables . El concepto de algoritmo presupone un modelo de cálculo ; A menos que se indique lo contrario, se hace referencia a las máquinas de Turing o un modelo equivalente.

definición

Un subconjunto de un conjunto contable se llama decidible si su función característica está definida por ${\ Displaystyle T}$${\ Displaystyle M}$ ${\ Displaystyle \ chi _ {T} \ dos puntos M \ a \ {0,1 \}}$

${\ displaystyle \ chi _ {T} (t) = {\ begin {cases} 1, & {\ mbox {if t}} \ in T \\ 0, & {\ textrm {de lo contrario}} \ end {cases} }}$

es predecible . Por tanto, el concepto de decidibilidad se remonta al concepto de calculabilidad.

Esta definición asume que todos los elementos del conjunto se pueden representar en la computadora. La cantidad debe ser godelizable . En teoría, para facilitar la comparación, se presupone directo o se presupone. En el último caso, el problema se ha presentado como el problema verbal de un lenguaje formal . ${\ Displaystyle M}$${\ Displaystyle M}$${\ Displaystyle M = \ mathbb {N}}$${\ Displaystyle M = \ {0.1 \} ^ {*}}$

Dado que solo se pueden godelizar conjuntos contables, el concepto de decidibilidad no se define para conjuntos incontables como el de los números reales . Sin embargo, hay intentos de extender el concepto de calculabilidad a números reales mediante un modelo de máquina extendido (por ejemplo, el modelo Blum-Shub-Smale ).

Demarcación

La indecidibilidad no debe confundirse con la imposibilidad práctica o fundamental de asignar un valor de verdad a un enunciado . En detalle, están involucrados los siguientes términos:

1. Inconsistencia: las paradojas o antinomias muestran que un cálculo contiene contradicciones, es decir, que no está libre de contradicciones . La paradoja de Russell , por ejemplo, mostró que la teoría de conjuntos ingenua contiene contradicciones.
2. Independencia: las declaraciones que se pueden agregar a un cálculo consistente sin crear una contradicción se denominan relativamente libres de contradicciones en relación con este cálculo. Si su negación está relativamente libre de contradicciones, entonces el enunciado es independiente . Por ejemplo, el axioma de elección es independiente de la teoría de conjuntos de Zermelo-Fraenkel .
3. Incompletitud: En los cálculos consistentes, que tienen al menos la expresividad de la aritmética , hay afirmaciones verdaderas que no se pueden probar en el cálculo. Estos cálculos se denominan incompletos .

La decidibilidad es una propiedad de los predicados y no de los enunciados. Se supone que el predicado está bien definido , por lo que ofrece un valor de verdad definido para cada elemento del conjunto. La indecidibilidad solo significa que el predicado no puede calcularse mediante un algoritmo.

Las declaraciones vistas como predicados de lugar cero siempre son decidibles, incluso si su valor de verdad aún no está claro. Si la afirmación es verdadera, entonces el algoritmo que siempre devuelve uno es un proceso de toma de decisiones. De lo contrario, el algoritmo, que siempre devuelve cero, es un proceso de toma de decisiones.

historia

El problema de la decisión es "el problema de determinar la generalidad de las expresiones". "Se trata de especificar un procedimiento general para una teoría deductiva dada, lo que nos permite decidir si una oración dada, formulada en los términos de la teoría, puede probarse dentro de la teoría o no".

El factor decisivo es si existe un procedimiento puramente aplicable mecánicamente, un algoritmo , que aclare en un número finito de pasos si una expresión, una fórmula es válida en un sistema o no.

Según Frege , Whitehead y Russell , la "cuestión central de los lógicos y matemáticos era: ¿Existe un algoritmo [...] que determine a partir de cualquier fórmula de un cálculo lógico si se sigue de ciertos axiomas dados o no (el llamado problema de decisión)? "

Kurt Gödel publicó un trabajo sobre el problema de la decisión en 1931; El británico Alan Turing (1912-1954) reformuló los resultados de Gödel de 1931 en su obra Sobre números computables, con una aplicación al “problema de decisión” (28 de mayo de 1936), fundamental para esta rama de las matemáticas . Reemplazó el lenguaje formal universal, basado en la aritmética, de Gödel con dispositivos formales simples que se conocieron como la máquina de Turing .

El lógico Heinrich Scholz (1884-1956) solicitó (y recibió) una copia de este trabajo de Turing en 1936. Sobre la base de este trabajo, Scholz celebró (según Achim Clausing) "el primer seminario mundial sobre informática".

Ejemplos de

Todos los conjuntos finitos , el conjunto de todos los números pares y el conjunto de todos los números primos son decidibles. Para cada conjunto decidible, su complemento también puede ser decidible. La intersección y la unión de dos conjuntos decidibles son decidibles.

Sosteniendo problemas

El problema de la parada describe la cuestión de si un algoritmo termina con una entrada . Alan Turing demostró la indecidibilidad de esta pregunta. Más formalmente, el problema de retención es propiedad de pares de algoritmo y entradas que el algoritmo termina para la entrada , es decir, solo calcula de forma finita. El problema de la retención uniforme, es decir, la propiedad de los algoritmos de mantenerse finalmente para cada entrada, también es indecidible.

Sin embargo, se puede decidir el problema de parada para muchos modelos de cálculo más débiles, como las máquinas de Turing con restricción lineal .

Validez en la lógica proposicional

La validez en el cálculo proposicional es decidible. Se conoce el complemento a esto, el problema de satisfacibilidad de la lógica proposicional . Un proceso de toma de decisiones es el método de la tabla de verdad .

Validez en la lógica de predicados

El problema de decisión especial para la lógica de predicados fue planteado por David Hilbert en 1928 (véase el programa de Hilbert ). Alan Turing y Alonzo Church encontraron que el problema en 1936 era irresoluble (ver problema de retención ).

El problema de decisión no se resuelve para la lógica de predicados general, sino solo para las subáreas de la lógica de predicados, como la lógica de predicados con predicados de primer orden de un solo dígito.

Solvabilidad de las ecuaciones diofánticas

Una ecuación polinomial se llama diofántica si todos los coeficientes son números enteros y solo se buscan soluciones enteras. La propiedad de las ecuaciones diofánticas de tener una solución ( el décimo problema de Hilbert ) es indecidible. La solubilidad de las ecuaciones diofánticas lineales, por otro lado, es decidible.

Problema de correspondencia de la publicación

Una lista finita de pares de palabras no vacías sobre un alfabeto finito se denomina caso problema. Una solución a un problema es una secuencia de números finita y no vacía para pares de palabras en la lista, de modo que los primeros componentes de los pares de palabras, cuando se juntan, dan como resultado la misma palabra que los segundos componentes de los pares de palabras.

Ejemplo: tiene la solución porque se aplica . ${\ Displaystyle \ left (a, aba \ right), (ab, bb), (baa, aa)}$${\ Displaystyle \ left (1,3,2,3 \ right)}$${\ Displaystyle a \ cdot baa \ cdot ab \ cdot baa = abaaabbaa = aba \ cdot aa \ cdot bb \ cdot aa}$

El problema de correspondencia Postsche , que es la propiedad de los casos problema de tener una solución que es indecidible.

física

Según Toby Cubitt, David Pérez-García, Michael Wolf, el siguiente problema de la teoría de la mecánica cuántica de muchos cuerpos es indecidible. Se da la función de Hamilton de un problema de mecánica cuántica de muchos cuerpos. ¿Tiene el espectro un espacio entre el primer estado excitado y el estado fundamental o no? Los autores construyeron explícitamente una familia de sistemas de espín cuántico en una red bidimensional con interacción del vecino más cercano invariante en la traducción, por lo que la cuestión de la brecha espectral es indecidible. Combinaron la teoría de la complejidad de los operadores de Hamilton con técnicas de mosaico aperiódico y tradujeron el problema en un problema de retención de una máquina de Turing. Otras propiedades de baja energía del sistema también son indecidibles.

Términos relacionados

Una clase más general que los conjuntos decidibles son los conjuntos recursivamente enumerables o semidecidibles , donde el único requisito para "sí" es que el cálculo debe detenerse en un tiempo finito. Si tanto un conjunto como su complemento son semidecidibles, entonces el conjunto es decidible. El problema de la detención es semi-decidible porque la respuesta “sí” siempre se puede dar ejecutando el programa. Sin embargo, el complemento del problema de la tenencia no es semidecidible.

Ver también

• Problema de equivalencia
• Previsibilidad
• Problema de finitud
• Problema de vacío
• Problema de correspondencia postal
• Conjunto semidecidible

literatura

• Lothar Czayka : Lógica formal y filosofía de la ciencia. Introducción para economistas. Oldenbourg, Munich y otros 1991, ISBN 3-486-20987-6 , pág.45 y siguientes.
• Willard Van Orman Quine : Principios de lógica. 8ª edición. Suhrkamp, ​​Frankfurt am Main 1993, ISBN 3-518-27665-4 , p. 142 y siguientes ( Suhrkamp-Taschenbuch Wissenschaft 65), en detalle.
• Paul Hoyningen-Huene : Lógica formal. Una introducción filosófica. Reclam, Stuttgart 1998, ISBN 3-15-009692-8 , p. 226 y siguientes ( Biblioteca Universal de Reclam 9692)
• Hartley Rogers: Teoría de funciones recursivas y computabilidad efectiva . McGraw-Hill, 1967. 
• Uwe Schöning : Informática teórica, en pocas palabras . 4ª edición. Spectrum, 2000, ISBN 3-8274-1099-1 , págs. 122 ff . 

Evidencia individual

1. ↑ Arnim Regenbogen, Uwe Meyer (Ed.): Diccionario de términos filosóficos. Edición especial. Meiner, Hamburgo 2006, ISBN 3-7873-1761-9 , “decidible”.
2. ↑ David Hilbert , W. Ackermann : Fundamentos de lógica teórica. 6ª edición. Springer, Berlín y col. 1972, ISBN 0-387-05843-5 , p. 119 ( Las enseñanzas básicas de las ciencias matemáticas 27).
3. ↑ Alfred Tarski : Introducción a la lógica matemática. 5ª edición, ampliada para incluir el artículo "Verdad y evidencia". Vandenhoeck & Ruprecht, Göttingen 1977, ISBN 3-525-40540-5 , p. 145 ( Matemáticas modernas en representación elemental 5).
4. ↑ Patrick Brandt, Rolf-Albert Dietrich, Georg Schön: Lingüística. Un hilo conductor para estudiar el idioma alemán. 2ª edición revisada y actualizada. Böhlau, Colonia y otros 2006, ISBN 3-412-00606-8 , pág.14 ( UTB 8331).
5. ↑ La copia fue encontrada por Achim Clausing en el Instituto de Ciencias de la Computación de la Universidad Wilhelms de Westfalia en Münster ( Westfälische Nachrichten . 28 de enero de 2013: Tras los pasos de un pionero: las impresiones originales del científico informático Alan Turing se encuentran en la Biblioteca de la Universidad de Münster. ; en línea ).
6. ↑ Hilbert / Ackermann: Funciones básicas. 6ª edición. (1972), pág.119.
7. ↑ Willard Van Orman Quine : Principios de lógica. 8ª edición. Suhrkamp, ​​Fráncfort del Meno 1993, ISBN 3-518-27665-4 , p. 247.
8. ^ Lothar Czayka: lógica formal y filosofía de la ciencia. Introducción para economistas. Oldenbourg, Munich y otros 1991, ISBN 3-486-20987-6 , pág.45 .
9. ↑ Cubitt, Pérez-García, Wolf, Indecidibilidad de la brecha espectral, Nature, Volumen 528, 2015, p. 207, Preprint Arxiv