Hacia una ciencia matemática de Computación

DSN_XP recoge de la historia del software, los escritos que nos han parecido muy relevantes y dentro de este listado, en esta ocasión tomamos como referente la propuesta de John McCarthy denominada como Towards a Mathematical Science of Computation

Introducción (1996)

En este artículo discutiré las perspectivas de una ciencia matemática de computación. En una ciencia matemática, es posible deducir de los supuestos básicos, las propiedades importantes de las entidades tratadas por la Ciencia. Así, a partir de la ley de gravitación de Newton y sus leyes del movimiento, uno puede deducir que las órbitas planetarias obedecen a las leyes de Kepler.

¿Cuáles son las entidades de las que se ocupa la ciencia de la computación?
¿Qué tipo de hechos sobre estas entidades nos gustaría derivar?
¿Cuáles son los supuestos básicos de los que debemos partir?
¿Qué resultados importantes se han obtenido ya?
¿Cómo puede la ciencia matemática ayudar en la solución de problemas prácticos?

Me gustaría proponer algunas respuestas parciales a estas preguntas. Estas respuestas parciales sugieren algunos problemas para el trabajo futuro. Primero, daré algunas respuestas generales muy esquemáticas a las preguntas. Entonces presentare algunos resultados recientes sobre tres cuestiones específicas. Finalmente, intentaré dibujar algunas conclusiones sobre aplicaciones prácticas y problemas para trabajos futuros.

Este artículo debería considerarse junto con mi artículo anterior [McC63].

Los principales resultados del presente documento son nuevos, pero existe cierta superposición, por lo que este documento sería autónomo. Sin embargo, algunos de los temas de este escrito como expresiones condicionales, definición recursiva de funciones y prueba por inducción recursiva se consideran con mucho mayor detalle en el documento anterior.

¿Cuáles son las entidades con las que la ciencia del cómputo debe lidiar?

Estas son problemas, procedimientos, espacios de datos, programas que representan procedimientos en determinados lenguajes de programación y computadores.

Los problemas y los procedimientos a menudo se confunden.

Un problema se define por el criterio que determina si se acepta una solución propuesta. Uno puede comprender un problema completamente sin tener ningún método de solución.
Los procedimientos generalmente se construyen a partir de procedimientos elementales. Lo qué pueden ser estos procedimientos elementales y cómo los procesos más complejos se construyen a partir de ellos, este es uno de los primeros temas de la ciencia de la computación.

Esta temática no es difícil de entender desde que existe una noción precisa de una función computable para guiarnos y computablemente relativa a una colección dada de las funciones iniciales, es fácil de definirla.

Los procedimientos operan sobre miembros de ciertos espacios de datos y producen miembros de otros espacios de datos, utilizando en general otros espacios de datos como intermediarios. Se conocen varias operaciones para construir nuevos espacios de datos con los más simples, pero todavía no existe una teoría general de espacios de datos representables, comparables a la teoría de funciones computables. Algunos resultados están dados en [McC63].
Los programas son expresiones simbólicas que representan procedimientos. El mismo procedimiento puede estar representado por diferentes programas en diferentes lenguajes de programación.

Se discutirá el problema de definir semánticamente un lenguaje de programación indicando qué procedimientos representan los programas. En cuanto a la sintaxis de los lenguajes de programación, las reglas que nos permiten determinar si una expresión pertenece al lenguaje han sido formalizadas pero las partes de la sintaxis que se relacionan estrechamente con la semántica, no ha sido tan bien estudiadas

El problema de traducir procedimientos de un lenguaje de programación a otro ha sido muy estudiado y vamos a intentar dar una definición de la corrección de la traducción.

Las computadoras son autómatas finitos. Desde nuestro punto de vista, una computadora está definida por el efecto de ejecutar un programa con una entrada dada, en el estado de su memoria y de sus salidas.

La ciencia de la computación debe estudiar las diversas formas en la que los elementos de los espacios de datos se representan en memoria de la computadora y cómo los procedimientos están representados por programas de cómputo. Bajo esta perspectiva, la mayoría de los trabajos actuales sobre la teoría del autómata no viene al caso.

¿Qué tipos de hechos acerca de los problemas, procedimientos, espacios de datos, programas y computadores nos gustaría derivar?

Ante todo. nos gustaría poder demostrar que determinados procedimientos resuelven determinados problemas dados. Sin embargo, probar esto puede implicar probar una gran cantidad de otros tipos de afirmaciones como:

Dos procedimientos son equivalentes, por ejemplo, si calculan la misma función.
Varias funciones computables satisfacen una determinada relación, como una identidad algebraica o una fórmula del cálculo funcional.
Cierto procedimiento finaliza para ciertos datos iniciales, o para todos los datos iniciales.
Un cierto procedimiento de traducción, traduce correctamente los procedimientos entre un lenguaje de programación y otro.
Un procedimiento es más eficiente que otro procedimiento equivalente si en ese sentido se realiza en menos pasos o requiere menos memoria.
Una cierta transformación de los programas conserva la función expresada pero aumenta la eficiencia.
Cierta clase de problemas no se puede resolver mediante ningún procedimiento o requiere procedimientos de cierto tipo para su solución

¿Cuáles son los axiomas y reglas de inferencia de una ciencia matemática de computación?

Idealmente, nos gustaría una teoría matemática en la que todo enunciado verdadero acerca de los procedimientos tendría una prueba y preferiblemente una prueba que sea fácil de encontrar, no demasiado larga y fácil de comprobar.

En 1931, Gödel demostró un resultado, uno cuyas consecuencias inmediatas fueron que no hay teoría matemáticas completa de la computación. Dada cualquier teoría matemática de la computación, hay enunciados verdaderos que pueden expresarse y que no tienen pruebas. Sin embargo, podemos esperar una teoría que sea adecuada para propósitos prácticos, como demostrar que los compiladores funcionan; las declaraciones no demostrables tienden a ser de un carácter bastante arrollador, como que el sistema en sí es consistente.

Es casi posible hacerse cargo de uno de los sistemas de la teoría de los números elementales como la expuesta en el libro de Mostowski "Sentences Undecidable in Formalized Arithmetic" desde que el contenido de una teoría de la computación es bastante similar. Desafortunadamente, este y otros sistemas similares se diseñaron para facilitar la demostración de meta teoremas sobre el sistema, en lugar de probar teoremas en el sistema. Como resultado, a los enteros se les dio un papel tan especial que pruebas de afirmaciones bastante fáciles sobre procedimientos simples podrían ser extremadamente largas.

Por lo tanto, es necesario construir un nuevo pensamiento similar, teoría en la que ni los números enteros, ni ningún otro dominio (por ejemplo, cadenas de símbolos) se les de un papel especial. Se describen algunos resultados parciales en esta dirección en este escrito. A saber, un formalismo libre de números enteros para describir cálculos ha sido desarrollado y ha demostrado ser adecuado en los casos en que los que puede ser comparado con otros formalismos.

Se han desarrollado algunos métodos de prueba, pero todavía existe una brecha en lo que respecta a los métodos para demostrar que un procedimiento finaliza. La teoría también requiere extensión para tratar las propiedades de los espacios de datos.

¿Qué resultados relevantes se han obtenido para una ciencia matemática de computación?

En 1936, Turing aclaró la noción de función computable y demostró la existencia de computadores universales que, con un adecuado programa, podría calcular cualquier cosa calculada por cualquier otra computadora.

Todo nuestros programas almacenados de computadoras, cuando se les proporciona almacenamiento auxiliar ilimitado, son universales, en el sentido de Turing. En cierto sentido subconsciente, incluso las ventas de los departamentos de los fabricantes de computadoras son conscientes de esto y no anuncian instrucciones mágicas que no pueden ser simuladas en máquinas competidoras, pero solo se anuncia que sus máquinas son más rápidas, más baratas, tienen más memoria, o son más fáciles de programar.

El segundo resultado importante fueron la existencia de clases de problemas irresolubles. Esto mantiene a todas las empresas menos a las más ignorantes de nosotros tratando de inventar un procedimiento de depuración que pueda infaliblemente decir si un programa que se está examinando entrará en un bucle.

Más adelante en este escrito, discutiremos la relevancia de los resultados de la lógica matemática a un grupo de problemas creativos sobre si es posible que la máquina pueda ser tan inteligente como un ser humano. En mi opinión es muy importante construir un puente más firme entre la lógica y la teoría de funciones recursivas por un lado y la práctica de la computación por el otro.

Gran parte del trabajo sobre la teoría de los autómatas finitos ha sido motivado con la esperanza de aplicarlo en la computación. Pienso que esta esperanza en su mayoría es en vano porque el hecho de la finitud se usa para mostrar que el autómata eventualmente repetirá un estado. Sin embargo, cualquiera que espere que un IBM 7090 repita un estado, únicamente porque es un autómata finito, está en una espera muy larga.

¿Cómo puede la ciencia matemática de la computación ayudar a la solución práctica de problemas?

Naturalmente, no se pueden prever las aplicaciones más importantes de una ciencia cuando recién comienza. Sin embargo, se pueden prever las siguientes aplicaciones:

En la actualidad, los lenguajes de programación se construyen de una manera muy poco sistemática. Se inventan una serie de características propuestas y luego argumentamos sobre si cada función vale su costo. Una mejor comprensión de la estructura de los cálculos y de los espacios de datos facilitará ver qué las características son realmente deseables.
Debería ser posible casi eliminar la depuración. La depuración son las pruebas de un programa en los casos que uno espera sean típicos, hasta que parece que funcionan. Esta esperanza es frecuentemente vana.

En lugar de depurar un programa, se debe demostrar que cumple con sus especificaciones y esta prueba debe ser verificada por un programa de computadora. Para que esto sea posible, se requieren sistemas formales en los que sea fácil escribir pruebas.

Hay una buena posibilidad de hacer esto, porque podemos requerir de la computadora hacer mucho más trabajo en la verificación de cada paso de lo que un humano está dispuesto a hacer. Por lo tanto, los pasos pueden ser mayores que con los sistemas formales actuales. las perspectivas para esto se discuten en [McC62].

El uso de expresiones condicionales para definir funciones recursivas

En el lenguaje matemático ordinario, existen ciertas herramientas para definir nuevas funciones en términos de las antiguas. Estas herramientas son la composición y la identificación de variables. Da la casualidad de que estas herramientas son inadecuadas computablemente en términos de las anteriores. Entonces se acostumbra definir todas las funciones que pueden razonablemente considerarse que dan una definición verbal. Por ejemplo, la función | x | generalmente se define en palabras.

Si agregamos una sola herramienta formal, a saber, expresiones condicionales a nuestra notación matemática y si permitimos que se utilicen expresiones condicionales recursivamente de una manera que pueda describirse, podemos definir, de una manera completamente formal, todas las funciones que razonablemente pueden considerarse computables en términos de un conjunto inicial.

Usaremos la notación ALGOL 60 para expresiones condicionales en este documento.

Usaremos expresiones condicionales en la forma simple

si p entonces a si no b

donde p es una expresión proposicional cuyo valor es verdadero o falso. El valor de la expresión condicional es a si p tiene el valor verdadero y b si p tiene el valor falso. Cuando se utilizan expresiones condicionales, el stock de predicados que uno tiene disponible para construir p es tan importante como el stock de funciones ordinarias que se utilizarán para formar las a y las b por composición.

A continuación, se muestran ejemplos de funciones definidas por expresiones condicionales:

La primera de ellas es la única definición no recursiva del grupo. Luego, tenemos tres procedimientos diferentes para calcular n !; les puede parecer ser equivalentes por los métodos que se describirán en este documento. Entonces definimos la función predecesora n- para enteros positivos (3- = 2) en términos de la función sucesora n´(2´ = 3) Finalmente, definimos la suma en términos del sucesor, antecesor e igualdad. En todas las definiciones, excepto en la primera, el dominio de las variables se toma como el conjunto de valores no negativos enteros.

Como ejemplo del uso de estas definiciones, mostraremos cómo computar 2! según la segunda definición de n !. Tenemos

Tenga en cuenta que si intentamos calcular n! para cualquier n pero entero no negativo las sucesivas reducciones no terminarían. En tales casos decimos que el cálculo no converge. Algunas funciones recursivas convergen para todos los valores de sus argumentos, algunas convergen para algunos valores de sus argumentos y algunos nunca convergen. Las funciones que siempre convergen se llaman funciones totales, y las otras se llaman funciones parciales. Uno de los resultados más importantes de la teoría de la función recursiva es que no hay formalismo que obtenga todas las funciones totales computables y no funciones parciales.

[McC63] Hemos probado que el método anterior para definir funciones computables, comenzando solo con la función sucesora n` y la igualdad, produce todas las funciones computables de los enteros. Esto nos lleva a afirmar que tenemos el conjunto completo de herramientas para definir funciones que son computables en términos de las dadas funciones base.

Si examinamos la penúltima línea de nuestro cálculo de 2! vemos eso no podemos simplemente considerar la expresión condicional

si p entonces a si no b

como función de las tres cantidades p, a y b. Si lo hiciéramos, estaríamos obligados a calcular g (−1,0) antes de evaluar la expresión condicional y este cálculo no convergería. Lo que debe pasar es que cuando p es cierto, tomamos a como el valor de la expresión condicional sin regresar a ver a b.

Cualquier referencia a funciones recursivas en el resto de este artículo se refiere a funciones definidas por los métodos anteriores.

Probar afirmaciones sobre funciones recursivas

En la sección anterior presentamos un formalismo para dadas funciones base describir funciones que son computables en términos de estas. Nos gustaría tener una teoría matemática lo suficientemente fuerte como para admitir pruebas de esos hechos acerca de los procedimientos de computación que uno normalmente necesita para mostrar que los programas computables cumplen con sus especificaciones.

En [McC63] mostramos que nuestro formalismo para expresar funciones computables, era lo suficientemente fuerte como para que todos las funciones recursivas de enteros se pueden obtener a partir de la función sucesora y la igualdad. Ahora nos gustaría una teoría lo suficientemente fuerte para que la adición de alguna forma de axiomas de Peano permitiría la demostración de todos los teoremas de una de las formas de la teoría de números elementales.

Aún no tenemos tal teoría. La dificultad radica en mantener los axiomas y reglas de inferencia de la teoría libres de los enteros u otros dominios, tal como lo hemos logrado con el formalismo para construir funciones. Ahora enumeraremos las herramientas que tenemos hasta ahora para probar las relaciones entre funciones recursivas. Se comentan con más detalle en [McC63].

Sustitución de expresiones por variables libres en ecuaciones y otras relaciones.
Reemplazo de una subexpresión en una relación por una expresión que se ha demostrado que es igual a la subexpresión. (Esto se conoce en matemáticas elementales como sustitución de iguales por iguales.)

Cuando estamos tratando con expresiones condicionales, una forma de esta regla más fuerte que la habitual es válida. Supongamos que tenemos una expresión de la forma

si p entonces a si no (si q entonces b si no c)

y deseamos reemplazar b por d. En estas circunstancias, no tenemos que probar la ecuación b = d en general, pero solo el enunciado más débil

∼ p ∧ q ⊃ b = d

Esto se debe a que b afecta el valor de la expresión condicional solo en el caso ∼ p ∧ q es cierto.
Las expresiones condicionales satisfacen una serie de identidades y una teoría completa de las expresiones condicionales, muy similar al cálculo proposicional, es tratada a fondo en [McC63]. Enumeraremos algunas de las identidades tomadas como axiomas aquí.
Finalmente, tenemos una regla llamada inducción de recursividad para hacer argumentos que en las formulaciones habituales se realizan por inducción matemática. Esta regla puede considerarse que toma uno de los teoremas de la teoría de la función recursiva y dándole el estatus de regla de inferencia. Inducción de recursividad puede describirse de la siguiente manera:

Supongamos que tenemos una ecuación de recursión que define una función f, a saber

f (x 1 , ..., x n ) = ε {f, x 1 , ..., x n } (1)

donde el lado derecho será una expresión condicional en todos los no triviales casos y supongamos que:

1. El cálculo de f (x 1 , ..., x n ) de acuerdo con esta regla converge para un cierto conjunto A de n-tuplas,
2. las funciones g (x 1 , ..., x n ) y h (x 1 , ..., x n ) satisfacen cada una la ecuación (1) cuando g o h se sustituye por f. Entonces podemos concluir que g (x 1 , ..., x n ) = h (x 1 , ..., x n ) para todas las n-tuplas (x 1 , ..., x n ) del conjunto A.

Como ejemplo del uso de la inducción recursiva demostraremos que la función g definida por

g (n, s) = si n = 0 entonces s si no g (n - 1, n × s)

satisface g (n, s) = n! × s dados los datos habituales sobre n !, Tomaremos por dado el hecho de que g (n, s) converge para todas las integrales n y s no negativas. Entonces solo necesitamos mostrar que n! × s satisface la ecuación para g (n, s), tenemos

n! × s = si n = 0 entonces n! × s else n! × s

si n = 0 entonces s else (n - 1)! × (n × s)

y esto tiene la misma forma que la ecuación satisfecha por g (n, s). Los pasos en esta derivación son bastante obvios pero también siguen los axiomas mencionados anteriormente y las reglas de inferencia. En particular, la regla extendida de reemplazo se utilizan varios ejemplos adicionales de demostración por inducción de recursividad se dan en [McC63] y se ha utilizado para probar algunas relaciones bastante complicadas entre funciones computables.

Funciones recursivas, diagramas de flujo y programas algolic

En esta sección quiero establecer una relación entre el uso de funciones recursivas para definir cálculos, la notación del diagrama de flujo y programas expresados como una secuencia de sentencias de asignación de tipos ALGOL, junto con la condicional Go To. A este último lo llamaremos programas Algolic con la idea de ampliar posteriormente la notación y los métodos de prueba para cubrir más el lenguaje ALGOL. Recuerda que nuestro propósito aquí no es crear todavía otro lenguaje de programación, sino proporcionar herramientas para probar hechos sobre programas.

Para considerar los programas como funciones recursivas, definiremos el estado del vector ξ de un programa en un momento dado, para ser el conjunto de valores actualmente asignados a las variables del programa. En el caso de un programa en lenguaje de máquina, el estado del vector es el conjunto de contenidos actuales de esos registros cuyo contenido cambia durante el curso de la ejecución del programa.

Cuando se ejecuta un bloque de programa que tiene una sola entrada y salida, el efecto de esta ejecución en el estado del vector puede ser descrito por una función ξ` = r (ξ) dando el nuevo estado del vector en términos del antiguo.

Considere un programa descrito por el diagrama de flujo de la fig. 1.

Los dos bloques internos de cómputo se describen mediante las funciones f (ξ) y g (ξ), indicando cómo estos bloques afectan el estado del vector. Los óvalos de decisión se describen mediante los predicados p (ξ), q 1 (ξ) y q 2 (ξ) que define las condiciones para tomar varios caminos. Deseamos describir la función r (ξ) que da el efecto a todo el bloque, en términos de las funciones f y g y los predicados p, q 1 y q 2 . Esto se hace con la ayuda de dos funciones auxiliares s y t. s (ξ) describe el cambio en ξ entre el punto etiquetado como s en el gráfico y la salida final del bloque; t se define de manera similar con respecto al punto etiquetado t. Podemos leer las siguientes ecuaciones directamente del diagrama de flujo:

r (ξ) = s (f (ξ))

s (ξ) = si p (ξ) entonces r (ξ) si no t (g (ξ))

t (ξ) = si q 1 (ξ) entonces r (ξ) si no q 2 (ξ) entonces ξ si no t (g (ξ))

De hecho, estas ecuaciones contienen exactamente la misma información que el diagrama de flujo.

Considere la función mencionada anteriormente, dada por

g (n, s) = si n = 0 entonces s si no g (n - 1, n × s)

Corresponde, como dejamos que el lector se convenza a sí mismo, al programa Algolic

Este diagrama de flujo se muestra en la fig. 2.

En el diagrama de flujo se describe mediante la función fac (ξ) y la ecuación

fac (ξ) = si p (ξ) entonces ξ si no fac (g (f (ξ)))

donde p (ξ) corresponde a la condición n = 0, f (ξ) al enunciado n: = n - 1 y

g (ξ) al enunciado s: = n × s.

dónde

p (ξ) ≡ c (n, ξ) = 0,

f (ξ) = a (s, c (n, ξ) ∗ c (s, ξ), ξ),

g (ξ) = a (n, c (n, ξ) - 1, ξ)

y así

fac (ξ) = a (n, 0, a (s, c (n, ξ)! × c (s, ξ))).

Consideraremos que el estado del vector tiene muchos componentes, pero los únicos componentes afectados por el presente programa son el componente s y el componente n.

Para calcular explícitamente con los estados del vector, introducimos la función c (var, ξ) que denota el valor asignado a la variable var en el estado del vector ξ, y también introducimos la función a (var, val, ξ) que denota el estado del vector que resulta cuando el valor asignado a var en ξ se cambia a val y los valores de las otras variables no se modifican.

Los predicados y funciones de los estados del vector mencionados anteriormente serían:

p (ξ) = (c (n, ξ) = 0)

g (ξ) = a (n, c (n, ξ) - 1, ξ)

f (ξ) = a (s, c (n, ξ) × c (s, ξ), ξ)

Podemos probar por inducción de recursividad que fac (ξ) = a (n, 0, a (s, c (n, ξ)! × c (s, ξ), ξ),

pero para hacerlo debemos utilizar los siguientes hechos sobre las funciones del estado básico del vector:

c (u, a (v, α, ξ)) = si u = v entonces α si no c (u, ξ)
a (v, c (v, ξ), ξ) = ξ
a (u, α, a (v, β, ξ)) = si u = v entonces a (u, α, ξ) de lo contrario a (v, β, a (u, α, ξ))
La prueba es paralela a la prueba anterior de que
g (n, s) = n! × s,

pero las fórmulas son más largas.

Si bien todos los diagramas de flujo corresponden inmediatamente a funciones recursivas de el estado del vector, lo contrario no es el caso. La traducción desde la función recursiva al diagrama de flujo y por lo tanto al programa Algolic es inmediata, sólo si las ecuaciones de recursividad están en forma iterativa. Supongamos que tenemos una ecuación de recursividad

r (x 1 , ..., x n ) = E {r, x 1 , ..., x n , f 1 , ..., f m }

donde E {r, x 1 , = ldots, x n , f 1 , ..., f m } es una expresión condicional que define la función r en términos de las funciones f 1 , ..., f m . Se dice que E está en modo iterativo si r nunca aparece como el argumento de una función, sino sólo en términos de expresión condicional principal en la forma

... luego r (...).

En los ejemplos, todas las definiciones recursivas excepto

n! = si n = 0 entonces 1 si no n × (n - 1)!

están en forma interactiva. En ese, (n - 1)! ocurre como un término de un producto.

Las funciones recursivas no iterativas se traducen en programas Algolic que se utiliza recursivamente como procedimiento. Los cálculos numéricos generalmente pueden transformarse en forma iterativa, pero los cálculos con expresión simbólica usualmente no pueden, a menos que las cantidades que juegan el papel de listas introducido explícitamente.

Inducción de recursividad en programas Algolic

En esta sección ampliamos el principio de inducción de recursividad para que pueda aplicarse directamente a los programas de Algolic sin antes transformarlos en funciones recursivas. Considere el programa Algolic

Queremos demostrar que es equivalente al programa

Antes de dar esta prueba describiremos el principio de inducción de recursividad tal como se aplica a una clase simple de diagramas de flujo. Supongamos que tenemos un bloque de programa representado por la fig. 3a. Supongamos que hemos probado que este bloque es equivalente al diagrama de flujo de la fig. 3b donde el bloque sombreado es el bloque original de nuevo. Esto corresponde a la idea de una función que satisface una ecuación funcional. Ahora podemos concluir que el bloque de la fig. 3a es equivalente al diagrama de flujo de la fig. 3c para aquellos estados del vector para los que el programa no quede atascado en un bucle en la fig. 3c.

Esto se puede ver de la siguiente manera, suponga que, para una entrada particular, el programa de la fig. 3c da la vuelta al bucle n veces antes de salir. Considere el diagrama de flujo que resulta cuando toda la fig. 3b se sustituye por el bloque sombreado (o amarillo) y luego sustituido en esta figura nuevamente, etc., un total de n sustituciones. El estado del vector al pasar por este diagrama de flujo se someterá exactamente a las mismas pruebas y cambios que al pasar por el flujo. 3c y, por lo tanto, saldrá en n pasos sin pasar por el bloque sombreado (o amarillo). Por tanto, debe salir con el mismo valor como en la fig. 3c. Por lo tanto, para cualquier vector para el que el cálculo de la fig. 3c converge, fig. 3a es equivalente a la fig. 3c.

Por tanto, para utilizar este principio para demostrar la equivalencia de dos bloques, probamos que satisfacen la misma relación, de tipo 3a-3b, y que el 3c correspondiente converge.

Aplicaremos este método para demostrar que los dos programas mencionados anteriormente son equivalentes. El primer programa se puede transformar de la siguiente manera:

La operación utilizada para transformar el programa es simplemente escribir por separado la primera ejecución de un bucle.

En el caso del segundo programa vamos:

Las operaciones utilizadas aquí son: primero, la introducción de una rama espuria, después de lo cual se realiza la misma acción independientemente de la forma en que la rama vaya; segundo, una simplificación basada en el hecho de que si la rama va por la primera vía, luego n = 0, junto con la reescritura de uno de los lados derechos de una declaración asignada y tercero, eliminación de una etiqueta correspondiente a una declaración nula y lo que podría llamarse una anti-simplificación de una secuencia de declaraciones de asignación. Aún no hemos elaborado un conjunto de reglas formales que justifique estos pasos, pero las reglas se pueden obtener de las reglas dadas anteriormente para sustitución, reemplazo y manipulación de expresiones condicionales.

El resultado de estas transformaciones es mostrar que los dos programas, satisface cada uno una relación de la forma: programa es equivalente a

El programa correspondiente a la fig. 3c en este caso, es precisamente el primer programa que asumiremos siempre converge. Esto completa la prueba.

La descripción de los lenguajes de programación

Los lenguajes de programación deben describirse sintácticamente y semánticamente. Esta es la distinción. La descripción sintáctica incluye:

Una descripción de la morfología, es decir, qué expresiones simbólicas representan programas gramaticales.
Las reglas para el análisis de un programa en partes y su síntesis de las partes. Por tanto, debemos ser capaces de reconocer un término que represente un suma y extraer de ella los términos que representan los sumandos.

La descripción semántica del lenguaje debe decir lo que los programas significan. El significado de un programa es su efecto sobre el estado del vector en el caso de un lenguaje independiente de la máquina, y su efecto sobre el contenido de la memoria en el caso de un programa en lenguaje máquina.

Sintaxis abstracta de los lenguajes de programación

La forma normal de Backus que se utiliza en el informe ALGOL describe la morfología de los programas ALGOL de forma sintética. Es decir, describe cómo se construyen los distintos tipos de programas a partir de sus partes. Esto sería mejor para traducir a ALGOL que para el problema más habitual de traducir desde ALGOL.

La forma de sintaxis que describiremos ahora difiere de la forma normal de Backus de dos maneras. Primero, es analítico en lugar de sintético; dice cómo desarmar un programa, en lugar de cómo armarlo. En segundo lugar, es abstracto en el sentido de que es independiente de la notación utilizada para su representación, digamos sumas, pero solo afirma que pueden ser reconocidas y desmontadas.

Considere un fragmento de los términos aritméticos de ALGOL, incluidas las constantes y las variables y sumas y productos. Como simplificación adicional, se debe considerar que las sumas y los productos tienen exactamente dos argumentos, aunque el caso general no es muy difícil. Supongamos que tenemos un término t. Desde la perspectiva de traducción, primero debemos determinar si representa una constante, una variable, una suma o un producto. Por lo tanto, postulamos la existencia de cuatro predicados: isconst (t), isvar (t), issum (t) e isprod (t). Supondremos que cada término satisface exactamente uno de estos predicados.

Considere los términos que son variables. Un traductor deberá poder saber si dos símbolos son ocurrencias de la misma variable, por lo que necesitamos un predicado de igualdad en el espacio de variables. Si las variables tienen que ser ordenadas se requiere una relación de ordenación.

Considere las sumas. Nuestro traductor debe poder seleccionar los sumandos y por lo tanto postulamos la existencia de funciones addend (t) y augend (t) definidas en aquellos términos que satisfacen issum (t). Del mismo modo, tenemos las funciones mplier (t) y mpcand (t) definidas en los productos. Desde el análisis de un término debe terminar, el predicado definido recursivamente

debe converger y tener el valor verdadero para todos los términos.

Los predicados y funciones cuya existencia y relaciones definen la sintaxis, son precisamente las necesarias para traducir del lenguaje, o para definir la semántica. Por eso no es necesario que nos importe si las sumas están representadas por a + b, o + ab, o (PLUS AB), o incluso por los números de Gödel 7 a 11 b .

Es útil considerar lenguajes que tienen tanto una analítica como una sintaxis sintética que satisface ciertas relaciones. Continuando con nuestro ejemplo de términos, la sintaxis sintética está definida por dos funciones mksum(t, u) y mkprod (t, u) que, cuando se dan dos términos t y u, dan su suma y producto respectivamente. Llamaremos regular a la sintaxis si las sintaxis analítica y sintética están relacionadas por las relaciones plausibles:

Una vez que se ha decidido la sintaxis abstracta de un lenguaje, se puede elegir el dominio de las expresiones simbólicas que se utilizarán. Entonces uno puede definir las funciones sintácticas explícitamente y se satisfacen a si mismas, preferiblemente probando que satisfagan las relaciones adecuadas. Si tanto el analítico como el sintético se dan funciones, no tenemos las difíciles y a veces insolubles problemas de análisis que surgen cuando los lenguajes se describen sólo sintéticamente.

En ALGOL las relaciones entre las funciones analítica y sintética no son del todo regulares, es decir, las relaciones sólo se mantienen hasta una equivalencia. Por tanto, se permiten paréntesis redundantes, etc.

Semántica

Las funciones sintácticas analíticas se pueden utilizar para definir la semántica de un lenguaje de programación. Para definir el significado de los términos aritméticos descritos anteriormente, necesitamos dos funciones más de naturaleza semántica, uno analítico y otro sintético. Si el término t es una constante, entonces val (t) es el número que t denota. Si α es un número mkconst (α) es la expresión simbólica que denota este número. Tenemos las relaciones obvias

val (mkconst (α)) = α
isconst (mkconst (α))
isconst (t) ⊃ mkconst (val (t)) = t

Ahora podemos definir el significado de los términos diciendo que el valor de un término para un vector de estado ξ viene dado por

Podemos ir más lejos y describir el significado de un programa en un lenguaje de programación de la siguiente manera: El significado de un programa se define por su efecto en el estado del vector. Es cierto que esta definición deberá elaborarse para tener en cuenta la entrada y la salida.

En el caso de ALGOL deberíamos tener una función

ξ = algol (π, ξ),

que da el valor ξ del vector de estado después de que el programa ALGOL π se haya detenido, dado que se inició al principio y que el vector de estadoin icialmente era ξ. Esperamos publicar en otro lugar una descripción recursiva del significado de un pequeño subconjunto de ALGOL.

Las reglas de traducción también se pueden describir formalmente. A saber,

Una máquina se describe mediante una función
x = máquina (p, x)
dando el efecto de operar el programa de máquina p en un vector de máquina x.
Una representación invertible x = rep (ξ) de un vector de estado como una máquina se da el vector.
Una función p = trans (π) que traduce programas fuente a máquina se dan programas.
La exactitud de la traducción se define por la ecuación

rep (algol (π, ξ)) = máquina (trans (π), rep (ξ)).

Cabe señalar que trans (π) es una función abstracta y no un programa de máquina . Para describir los compiladores, necesitamos otra función abstracta invertible , u = repp (π), que da una representación del programa fuente en la memoria de la máquina lista para ser traducida. Un compilador es entonces un programa de máquina tal que trans (π) = máquina (compilador, repp (π)).

Las limitaciones de las máquinas y los hombres como solucionadores de problemas

¿Puede un hombre hacer un programa de computadora que sea tan inteligente como él? La pregunta tiene dos partes. Primero, preguntamos si es posible en principio, en vista de los resultados matemáticos sobre indecidibilidad e incompletitud, la segunda parte es una cuestión del estado de la programación en lo que respecta a inteligencia artificial. Incluso si la respuesta a la primera pregunta es "no", uno todavía puede intentar llegar lo más lejos posible en la resolución de problemas por máquina.

Supongo que, en principio, no existe tal limitación. Sin embargo, la discusión completa involucra las partes más profundas de la teoría de la función recursiva y no se han desarrollado todas las matemáticas necesarias.

Considere el problema de decidir si una oración de cálculo bajo de predicados es un teorema. Muchos problemas de las matemáticas actuales o de interés científico puede formularse de esta forma y este problema resulta equivalente a muchos otros problemas, incluido el problema de determinar si un programa en una computadora con memoria ilimitada se detendrá alguna vez.

Según Post, esto equivale a decidir si un número entero es un miembro de lo que Post llama un conjunto creativo. Myhill demostró que todo conjunto creativo es equivalentes en un sentido bastante fuerte, de modo que en realidad sólo hay un clase de problemas en este nivel de insolubilidad.

Sobre este problema se conocen los siguientes hechos:

Existe un procedimiento que hará lo siguiente: Si el número está en el conjunto creativo, el procedimiento dirá "sí" y si el número no está en el conjunto creativo, el procedimiento no dirá "sí", puede decir "no" o puede ejecutarse de forma indefinida.
No existe un procedimiento que siempre diga "sí" cuando la respuesta es "sí", y siempre dirá "no" cuando la respuesta sea "no", si un procedimiento tiene la propiedad (1) que a veces debe ejecutarse indefinidamente. Por tanto, no hay procedimiento que siempre puede decidir definitivamente si un número es miembro de un conjunto creativo, o de manera equivalente, si una oración del predicado inferior el cálculo es un teorema, o si un programa ALGOL con una entrada dada nunca parará. Este es el sentido en el que estos problemas no tienen solución.
Ahora llegamos al sorprendente resultado de Post. Podríamos intentar hacerlo también como sea posible. Es decir, podemos intentar encontrar un procedimiento que siempre diga "sí" cuando la respuesta es "sí", y nunca dice "sí" cuando la respuesta es "no" y que dice "no" para una clase tan grande de casos negativos como sea posible, por lo tanto delimitando el conjunto de casos en los que el procedimiento continúa indefinidamente tanto como podamos. Post demostró que ni siquiera se puede hacer lo mejor posible. Es decir, Post dio un procedimiento que, al recibir cualquier otra decisión parcial procedimiento, daría uno mejor. El mejor procedimiento decide todos los casos el primer procedimiento decidido, y una clase infinita de nuevos. Primero vista esto parece sugerir que Emil Post era más inteligente que cualquier otro posible máquina, aunque el propio Post se abstuvo modestamente de dibujar este conclusión. Cualquiera que sea el programa que proponga, Post puede hacerlo mejor. Sin embargo, esto es injusto para los programas. A saber, el procedimiento de mejora de Post es en sí mismo mecánico y puede llevarse a cabo por máquina, de modo que la máquina puede mejorar su propio procedimiento o incluso puede mejorar la publicación, si se le da una descripción de los propios métodos de Post para tratar de decidir oraciones del predicado inferior cálculo. Es como un concurso para ver quién puede nombrar el mayor número. El hecho de que pueda sumar uno a cualquier número que des, no prueba que sea mejor que tu.
Sin embargo, la situación es más complicada que esto. Obviamente, el proceso de mejora puede llevarse a cabo un número finito de veces y poco pensamiento muestra que el proceso se puede llevar a cabo un número infinito de veces. Es decir, sea p el procedimiento original y la mejora de Post procedimiento se llamará P, entonces P n p representa el procedimiento original mejorado n veces. Podemos definir P ω p como un procedimiento que aplica p durante un tiempo, luego P D por un tiempo, luego p nuevamente, luego P p , luego P 2 p, luego p, luego P p , luego P 2 p, entonces P 3 p, etc. Este procedimiento decidirá cualquier problema que cualquier P n voluntad decidir, por lo que con razón puede llamarse P ω p. Sin embargo, P ω p es en sí mismo sujeto al proceso de mejora original de Post y el resultado puede llamarse P ω + 1 p. ¿Hasta dónde puede llegar esto? La respuesta es técnica. Es decir, dado cualquier recursivoα ordinal transfinito, se puede definir P α p. Un ordinal recursivo es un recursivo ordenamiento de los enteros que es un buen ordenamiento en el sentido de que cualquier subconjunto delos números enteros tienen un miembro mínimo en el sentido del orden. Por lo tanto, tenemos un concurso para tratar de nombrar el ordinal recursivo más grande. Aquí parece que estamos atascado, porque el límite de los ordinales recursivos no es recursivo. Sin embargo, esto no excluye la posibilidad de que haya una mejora diferente proceso Q, de modo que Qp es mejor que P α p para cualquier α ordinal recursivo.
Hay otra complicación más. Suponga que alguien nombra lo que reclamaciones es un gran ordinal recursivo. Nosotros, o nuestro programa, podemos nombrar un agregando uno, pero ¿Cómo sabemos que el procedimiento que él afirma es un ordenamiento recursivo, ¿de verdad? Dice que lo ha probado en algún sistema de la aritmética. En primer lugar, puede que no estemos seguros de que su sistema dela aritmética es correcta o incluso consistente. Pero incluso si el sistema es correcto, según el teorema de Gödel, está incompleto. En particular, hay ordinales que no se puede probar que sean así en ese sistema. Rosenbloom, en su libro "Elementos de lógica matemática" llegó a la conclusión de que el hombre era en principio superior a las máquinas porque, dado cualquier sistema formal de aritmetica, podría dar un sistema más fuerte que contenga oraciones verdaderas y probables eso no se pudo probar en el sistema original. Lo que Rosenbloom se perdió presumiblemente por razones sentimentales, es que el procedimiento de mejora es en sí mismo mecánico, y sujeto a iteración a través de los ordinales recursivos, por lo queque estamos de vuelta en la gran carrera ordinal. De nuevo nos enfrentamos a la complicación de probar que nuestros grandes ordinales son realmente ordinales.
Estas consideraciones tienen poca importancia práctica en su presente formar. Es decir, el proceso de mejora original es tal que la mejora Es probable que el proceso sea demasiado lento para obtener resultados en un tiempo razonable, ya sea realizado por el hombre o por la máquina. Sin embargo, puede ser posible poner este jerarquía en alguna forma utilizable. Para concluir, permítanme reafirmar que la cuestión de si existen limitaciones en principio de los problemas que el hombre puede hacer que las máquinas resuelvan comparado con su propia capacidad para resolver problemas, realmente es una técnica pregunta en la teoría de la función recursiva.

Referencias

[McC62] John McCarthy. Verificación de pruebas matemáticas por computadora. En Proceedings Symposium on Recursive Function Theory (1961). Sociedad Americana de Matemáticas, 1962.

[McC63] J. McCarthy. Una base para una teoría matemática de la computación. 1 en
P. Braffort y D. Hirschberg, editores, Programación informática y Sistemas formales, páginas 33–70. Holanda Septentrional, Amsterdam, 1963

ARQUITECTURA DSN_XP

Páginas

DSN_XP y las Ciencias matemáticas de la computación