Por favor revise mi cálculo ficticio (problema de detención, incompleto)

No podemos verificar su cálculo ficticio porque no nos lo proporcionó. Sin embargo, podemos mirar sus descripciones.

El ejemplo del problema de detención da una buena idea de lo que buscas. No hay solución al problema de la detención tal como lo definen los matemáticos. El lenguaje utilizado para describir el problema de la detención incluye formalmente las limitaciones del lenguaje utilizado para actuar sobre él.

Del mismo modo, el afeitado del barbero tiene un conjunto bien entendido de traducciones a la teoría de conjuntos, y esas definiciones formales no ofrecen oportunidades para liberarse con una nueva forma de cálculo. Así como nunca encontraremos un cálculo que demuestre 2 + 1 = 1, nunca encontraremos un cálculo que resuelva las cuestiones que surgen en la descripción del lenguaje formal de estos problemas.

Por supuesto, sigo lanzando esta frase, "lenguaje formal". Nos ha dado una glosa en inglés de varios problemas que ponen los pelos de punta a los matemáticos. Pero la versión en inglés no es tan mala. Usted mismo señala las lagunas que podrían resolver el problema del peluquero.

Con ese fin, me gustaría señalar el hermano mayor del problema de la detención: el teorema de Rice . Le invitamos a seguir el enlace para leer la versión en lenguaje formal del teorema, pero la glosa en inglés será suficiente aquí. El teorema de Rice establece que todas las propiedades semánticas no triviales de cualquier algoritmo son indecidibles. En este sentido, "semántico" significa que se refiere a lo que hace el algoritmo, a diferencia de las propiedades "sintácticas" que simplemente se refieren al contenido del algoritmo (como "¿tiene una rama si-entonces?"). Y no trivial solo significa que la propiedad es verdadera para algunos algoritmos y falsa para otros. Es trivial demostrar que un algoritmo "o se detiene o no se detiene", porque todos los programas hacen eso.

Llamo al teorema de Rice el "hermano mayor" del problema de la detención porque el problema de la detención es solo una instancia específica. Si su propiedad es "¿termina el programa?", el teorema de Rice se convierte en el problema de detención. Pero el teorema de Rice apunta al punto clave en el que parece estar trabajando su cálculo: la semántica. Su cálculo necesita operar sobre el significado semántico de estas frases, no solo sobre su sintaxis. Por ejemplo, el problema con el peluquero no es un problema en la semántica porque las lagunas son bastante explícitas.

¿Qué tan explícito? Bueno, usted habló de querer saber si había un caluclus existente para esto. Hay. Hay varios, porque la semántica es un gran problema. Ahora ninguno de ellos pretende ser "completo", pero todos tienen su lugar. La mayoría de los cálculos que se me ocurren son las lógicas de descripción (DL). Estas son herramientas semánticas que están diseñadas para permitir enfoques del estilo de "girar la manivela" para llegar a las respuestas. Por ejemplo, el problema del peluquero se puede representar en un lenguaje, OWL *:

# The class of men is a subset of the class of shaved things
SubClassOf(Man Shaved) 

# Everyone who is shaved is shaved by the barber.
EquivalentClasses(Shaved ObjectHasValue(shavedBy theBarber)) 

# Nobody shaves themselves
IrreflexiveObjectProperty(shavedBy)

# the person we seek is the person who shaves the barber
ObjectPropertyAssertion(shavedBy theBarber thePersonWeSeek)

Dentro de este constructo, podemos preguntar "¿es esto satisfactorio?" ¿Es teóricamente posible asignar valores a thePersonWeSeektal que se cumplan todos los criterios? Y la respuesta es sí. Por las reglas de inferencia de OWL, podemos determinar que este sistema funciona. Ahora, por supuesto, una forma es considerar que la clase "Hombre" tiene 0 elementos -- ¡no hay hombres en la ciudad! Para arreglar eso,

# Assert that there is at least one person (someone) who is a man
ClassAssertion(Man someone)

Ahora, con esa escapatoria cerrada, encontramos que sí, todavía es satisfacible. Incluso podemos hacer afirmaciones sobre el barbero, como ClassAssertion(ObjectComplement(Man) theBarber), que es la escapatoria que mencionaste: el barbero no es un hombre (el barbero es un miembro del complemento de la clase "Hombre").

Esto resuelve su caso de uso bastante limpio. Dependiendo de cómo traduzca las frases en inglés a OWL, encontrará diferentes lagunas, o incluso puede encontrar que cerró la laguna y todo el sistema se considera "insatisfactorio". Por ejemplo, si agrega reglas de que un barbero es un humano y que todos los humanos son hombres o mujeres, podría deducir que el barbero es una mujer.

Del mismo modo, DL también respalda su objetivo de eludir el problema de la detención. Si puede describir un programa semánticamente, a veces puede manipularlo para llegar a la respuesta que busca. Esto es lo que hacen los compiladores de optimización. Encuentran una manera de describir su programa que les permite hacer declaraciones útiles.

Ahora DL no es absolutamente una panacea. No reescribe las matemáticas. Los DL se diseñaron cuidadosamente para ser herramientas semánticas bastante poderosas, pero para ser siempre decidibles . Si activa cualquier consulta de coherencia que pueda realizar en un sistema DL, siempre puede encontrar una respuesta. No hay indecidibilidad aquí. ¿Cómo lo hicieron? Bueno, están intencionalmente debilitados para eludir el tipo de problemas aquí. En realidad, no pueden describir las máquinas de Turing lo suficiente como para armar la frase "¿esta máquina de Turing se detiene?" Lo hacen evitando contar (entre otras pequeñas y brillantes elecciones). No se puede hacer inducción matemática en ellos, porque no tienen forma de anotar n+1de una manera que permita probar nada.

Pero sí creo que son lo más cercano a un "cálculo" para responder a su tipo de preguntas que he encontrado. También son bestias fascinantes. Mirando hacia arriba desde este cálculo fácil y agradable hacia el mundo más amplio de la semántica, está la teoría de modelos , donde decimos "dado este conjunto de declaraciones verdaderas en nuestro modelo, ¿qué otras declaraciones verdaderas podemos hacer?" La regla de la Lógica de Descripción sigue de cerca los conceptos de vinculación de la Teoría de Modelos, simplemente operan en un lenguaje particular que tiene buenas propiedades. Puedes hacer Model Theory con las frases en inglés, sin traducirlo a OWL. Simplemente es más difícil llegar a algún lado cuando tus oraciones están en un lenguaje natural. Teoría de categoríaspuede ayudar con eso. Hay quienes investigan la teoría de categorías que afirman que es la base fundamental del lenguaje: todas las frases del lenguaje natural pueden transformarse en el lenguaje de las categorías. ¡Una afirmación de enormes proporciones en verdad!

Entonces, leyendo mucho entre líneas, su caluclus es probablemente un cálculo de semántica. Y, debido a que busca hacer que algunas pruebas sean fáciles, probablemente tenga un núcleo fácil de algo como DL que es decidible. Pero, si desea mantenerlo ficticio, debe saltar de este núcleo de DL decidible a algo más mágico. Algo así como la psicohistoria , un cálculo estadístico ficticio que utilizó Asimov para construir un personaje que predijo el curso de toda la humanidad durante miles de años.

* Uso OWL, en lugar del idioma nativo de DL, porque es un poco más accesible. DL está lleno de simbología concisa y exigente. Podría verse como:

Si bien esta es una notación muy bien definida, creo que es más difícil de leer con todos los símbolos. Las palabras usadas en OWL parecen ayudar. Si está interesado en la conexión, el dialecto de OWL que estoy usando, OWL-DL es un${\displaystyle {\mathcal {SHOIN}}^{\mathcal {(D)}}}$lenguaje, donde ese lío de mayúsculas matemáticas describe un tipo particular de Lógica de Descripción. Resulta ser uno que ha recibido mucha atención gracias al éxito de OWL.

Ya que ha etiquetado esto como ciencia dura: No, no tiene sentido. Hay pruebas para el problema de la detención. Tampoco es una prueba tan difícil de seguir si no recuerdo mal.

Si está tratando de establecer una ciencia dura, todo es lo mismo, pero esta cosa es diferente. Eso es genial, pero solo agita los detalles a mano. Pantalla de lámpara sin tecnoparloteo, continúa con la historia. Solo asegúrese de que los lectores comprendan los límites de la herramienta; de lo contrario, podría encontrarse con el problema de "lo hizo un mago".

Si debe tener alguna tecnocharla plausible, sería mejor que dijera algo como "tiene pruebas de que np==p". (De lo cual actualmente no tenemos pruebas). Lo que disminuiría el tiempo de resolución de muchos problemas difíciles. Que parece ser lo que buscas.

Mejor aún, solo diga que sus protagonistas tienen mejores computadoras con algunos asistentes de IA fuertes. Afecto más plausible y similar. No insinúa romper teoremas probados.