Kitabı oku: «Computación y programación funcional», sayfa 3
1.1.3 Otros
La máquina de Turing y el cálculo lambda no son los únicos modelos de computación. Existen muchos más e incluso hoy en día aparecen nuevos. Por otro lado, cada lenguaje de programación es, en sí mismo, un modelo de computación. Es por ello que se tiende a decir que un lenguaje como C++ o Python es «Turing completo», porque puede ser equivalente al funcionamiento de una máquina de Turing universal. Esto no acontece con otros lenguajes, como HTML o XML, que solo son de marcados y carecen de las características de un lenguaje de programación (condicionales, flujo de control, etc.).
Los modelos de computación, desde un punto de vista teórico de la computación, se pueden agrupar en tres categorías:
• Secuencial. En esta categoría caen los clásicos modelos de autómatas, finitos y con pila. Por otro lado, tenemos las máquinas de acceso aleatorio (RAM) y la máquina de Turing. Cada uno de ellos se cataloga como secuencial porque sigue un mecanismo paso a paso por cada operación.
• Funcional. El modelo de funciones recursivas, lógica combinatoria y, obviamente, el cálculo lambda. La idea principal no es la secuencia de paso, sino más bien construir la computación a través de funciones y reducción de estas.
• Concurrente. Algunos, como el autómata celular, la máquina paralela de acceso aleatorio (PRAM), el modelo en actores y la red de Petri, son modelos concurrentes. ¿Por qué concurrentes? Porque pueden suceder eventos que no siguen una secuencia y, en cambio, pueden «ejecutarse» fuera de un orden parcial sin afectar el resultado final de la computación.
1.2 TESIS DE CHURCH-TURING
Producto de la equivalencia entre los dos modelos, el cálculo lambda y la máquina de Turing, aparece el concepto de la tesis de Church-Turing, que reza lo siguiente:
Cualquiera que sea la función computable (algoritmo), esta es equivalente a una máquina de Turing.
Es decir, para que una función sea computable debe ser sí o sí computable por una máquina de Turing. En la actualidad, esto se sigue cumpliendo, y es difícil adherirse a la idea de que la tesis sea falsa, aunque es formalmente indemostrable. Esto radica en la incapacidad actual de definir qué es un «método efectivo» o «algoritmo», ya que no son conceptos fácilmente definibles. Simplemente se asume que cualquier algoritmo es una máquina de Turing.
Sobre esto, B. A. Trakhtenbrot, en su artículo: «Algorithms» de 1960, dijo lo siguiente sobre la incapacidad de demostrar esta tesis o hipótesis:
¿Cuál es la base de esta importante hipótesis? No podemos comprobarla como lo hacemos con un teorema matemático, puesto que es una declaración sobre el concepto general de algoritmo, que no está definido de manera precisa y no es, por tanto, un objeto propio de la discusión matemática. (Trakhtenbrot, 1960)
Sin embargo, en las últimas décadas se han añadido más datos que la han confirmado, por ejemplo, la equivalencia con otros modelos de computación (por ejemplo, lenguajes de programación), los cuales se suelen llamar «Turing completo».
1.2.1 Implicaciones filosóficas
Las implicaciones de la tesis no son solo técnicas o científicas. También trae consigo cuestiones filosóficas. Si llevamos el concepto de máquina de Turing al mundo físico, por ejemplo, se podría postular que el universo es una máquina de Turing universal, donde, dada la tabla de instrucción (leyes físicas), podemos crear una simulación de nuestro universo. Aunque claro, una objeción sería que las leyes físicas no son computables (aunque eso no está probado), pero incluso si lo asumimos, nada nos asegura que no se pueda construir otra máquina incluso más poderosa que la máquina de Turing.
Siguiendo este mismo razonamiento, Jack Copeland creó el concepto de «hipercomputación» (hypercomputation en inglés), el cual trata sobre la idea de poseer una máquina que no tenga los límites de una máquina de Turing. Con ello, se resolvería el problema de decisión. Aunque claro, la hipercomputación solo existe a nivel hipotético. Aun así, no se ha demostrado su imposibilidad.
Sin embargo, Martin Davis, en su artículo «The Myth of Hypercomputation» («El mito de la hipercomputación») del 2004, indicaría lo siguiente:
Si se permiten entradas no computables, entonces se pueden obtener salidas no computables. (Davis, 2004).
Con esta simple afirmación, Davis derriba la idea de la hipercomputación, ya que, si se aceptan valores no computables de entrada, entonces ¿por qué asumimos que siempre debería devolver una salida computable?
1.3 FILOSOFÍA DE LA CIENCIA DE LA COMPUTACIÓN
Es curioso ver la palabra «filosofía» en un libro de computación, y más si tiene como objetivo enseñar técnicas de programación. Quizá por este motivo existe este apartado. Tómelo como una persona que se autoinvita a su casa sin su consentimiento, pero que, a diferencia de ser una persona que viene con el propósito de hacerle perder el tiempo, este, en cambio, viene con noticias que «podrían» interesarle.
La filosofía de la ciencia de la computación es la búsqueda de respuestas a preguntas tales como las siguientes:
• ¿Qué es un programa computacional? ¿Un artefacto abstracto o concreto?
• ¿Cuáles son las diferencias entre programas computacionales y algoritmos?
• ¿Qué es una especificación e implementación?
• ¿Cuáles son los roles de los tipos de ciencias de la computación? ¿Es una ciencia o una ingeniería?
• ¿Qué es la abstracción en las ciencias de la computación? ¿Cómo se relaciona esta con la abstracción en las matemáticas?
• ¿La ingeniería de software plantea problemas filosóficos?
• ¿Cuál es el propósito de la programación?
• ¿Un algoritmo puede tener atributos estéticos?
• ¿Un algoritmo puede ser ético o solo es algo que corresponde a la persona que desarrolló el algoritmo?
En la filosofía, a diferencia de las ciencias, las preguntas ocupan un rol predominante por sobre las respuestas. Y esto no es casualidad, ocurre, como era de suponer, por la misma complejidad que supone encontrar respuestas a estas preguntas. Entonces, conceptos como hipótesis, experimento, refutación, falsación, etc. no forman parte de la filosofía; por el contrario, una teoría filosófica mide su valor sobre la base de su propia consistencia interna dentro del sistema propuesto.
Por lo mismo, el hecho de realizarnos preguntas trae consigo el mayor de los placeres, el intentar comprender mejor un área de estudio. Como todo profesional que busca la verdad, debe tener una visión crítica, abierta y evitar ideas dogmáticas que —generalmente en la computación— provienen de nuevas tecnologías de dudosa utilidad.
La computación no puede, simplemente, caer en un reduccionismo de aspectos técnicos o teóricos. Las implicaciones filosóficas de la computación son heterogéneas y, principalmente, inevitables. ¿Por qué? No solo por las cuestiones sobre si un sistema podrá alcanzar a emular o superar la inteligencia humana (inteligencia artificial fuerte) o sobre hasta qué límite un sistema que interactúa con humanos tiene responsabilidades éticas. Creemos, sin duda, que en los últimos años la orientación excesiva hacia la tecnología ha traído consigo cosas positivas y otras que no lo son tanto, especialmente por su parcial omisión y desvío de la atención hacia cuestiones que no tienen que ver con los principios de la computación.
Por ello, la filosofía de la ciencia de la computación se hace indispensable en un área que cada año se vuelve más compleja, especialista e imprecisa, y en la que surgen nuevos conjuntos de términos que muchas veces se usan de manera inexacta y que traen consigo una mayor confusión que claridad. La labor de una persona que pretenda abocarse a esta empresa desde un punto de vista filosófico es la búsqueda del orden y la sistematización general de toda el área. Para que a través de las preguntas adecuadas y propuestas sistémicas de cómo tratarlas (a saber: dar un orden y claridad a los conceptos que se usan a diario en los saberes que componen la computación), pueda y debiera, ser de ayuda a programadores, ingenieros y científicos. En consecuencia, la computación necesita de la filosofía.
Raymond Turner, en su libro Computational Artifacts. Towards a Philosophy of Computer Science («Artefactos computacionales. Hacia una filosofía de la ciencia de la computación»), que es uno de los referentes en cuanto a la filosofía de la ciencia de la computación, mencionó lo siguiente:
La ciencia de la computación es un área dominada por lenguajes. (Turner, 2018)
Creemos que no puede ser mejor afirmación para dar paso a los siguientes dos capítulos: (1) ¿qué es la programación? y (2) sobre los lenguajes de programación, en los cuales trataremos de demostrar que lo que dice Turner es verdad.
_________________
2 Conferencia en París, en el Congreso Internacional de Matemáticos de 1900.
3 Claramente Alan Turing no llamó a su modelo «Máquina de Turing». Él uso el término «a–machines» (la «a» por automática [máquinas automáticas]).
4 Hemos mantenido el nombre en inglés en los algoritmos en que, gracias a esto, se puede encontrar más literatura.
5 Para una breve introducción puede ver el apéndice A.
Capítulo 2
¿QUÉ ES LA PROGRAMACIÓN?
Haremos el trabajo de programar mucho mejor […] si respetamos las limitaciones intrínsecas de la mente humana y si nos acercamos a esta tarea como programadores humildes.
Edsger W. Dijkstra
La programación no es sinónimo de la ciencia de la computación ni de la ingeniería de software. Esta afirmación podría hacerle pensar a usted de manera implícita que la programación es algo informal, artesanal y, por ello, no tan importante. Pues no, todo lo contrario. La programación se erige sobre bases de la matemática y la lógica y hace uso de lenguajes formales a los que llamamos lenguajes de programación para crear artefactos abstractos: software, donde el medio para expresar estas ideas y llevarlas a la realidad son artefactos concretos: hardware. Prácticamente en cualquier área de la computación no podemos escapar de la actividad de programar. Algunas veces está más enfocada a la obtención de un producto comercial, y otras, en cambio, a la construcción de prototipos que nos ayudan a verificar hipótesis en nuestra investigación.
A mediados del siglo XX, la programación era una actividad que, ante todo, realizaban matemáticos con inclinación a la parte aplicada de su misma profesión, puesto que, por cuestiones obvias, en aquellos años no existía una carrera universitaria en computación, ya que el área estaba en pleno surgimiento. A ello se suman las dificultades para realizar ciertos trabajos en un ordenador que, por aquel entonces, tenía muchas limitaciones en cuanto a recursos (a saber: espacio de disco, velocidad de cómputo, memoria, etc.).
La programación es parte de un área más amplia que llamaremos simplemente computación. Pero por encima de la programación existe un término que convive en una simbiosis constante e inmutable que cubre toda la computación y, así, a la misma programación: algoritmo.
Objetivos de este capítulo:
• Entender qué son los algoritmos y cuál es su rol dentro de la computación.
• Conocer la importancia de la especificación y cómo esta se diferencia de la implementación.
2.1 ALGORITMOS
Yuri Gurevich dijo en su artículo «What is an algorithm?» («¿Qué es un algoritmo?») lo siguiente:
En nuestra opinión, bastante común en la computación, los algoritmos no son humanos o dispositivos; son entidades abstractas. (Gurevich, 2012)
Esta definición podría parecer obvia, al menos en su primera parte. Sabemos que un algoritmo no es una entidad humana o biológica, pero que sí puede afectar la vida de estas (principalmente con sistemas de inteligencia artificial). A continuación, dice que los algoritmos «son entidades abstractas»; esto nos da a entender que existe, para él, una relación directa con las matemáticas, que son el lenguaje de las entidades abstractas. Pero ¿qué tipo de entidad abstracta?
Nosotros definiremos el algoritmo desde un punto de vista formal siguiendo la afirmación de Gurevich, en conjunto con lo que menciona Leslie Lamport6 en su publicación «Who Builds a House Without Drawing Blueprints?» («¿Quién construye una casa sin dibujar los planos?»):
Necesitamos entender la tarea de programar a un nivel más alto antes de empezar a escribir código. (Lamport, 2015)
Concordamos con Lamport, por eso seguiremos su línea de pensamiento en este capítulo para tratar con los algoritmos, en busca de ese «nivel más alto».
Existen dos formas de ver lo que es un algoritmo: (1) desde un punto de vista de la especificación, es decir, la fase previa a implementarlo en un lenguaje de programación y donde podemos expresar nuestras soluciones usando el lenguaje universal de la ciencia: las matemáticas, o (2) la implementación de un algoritmo en un lenguaje de programación tradicional. Las dos no son excluyentes.
La capacidad de resolver problemas computacionales no implica que se deba usar el punto (2) sin el (1). Este es un error clásico de personas que están totalmente orientadas a la tecnología. En cambio, si seguimos la forma de trabajar de grandes informáticos del siglo XX, nos daremos cuenta de que usar las matemáticas para expresar nuestras ideas es enriquecedor y que, posteriormente, nos acercaremos a la parte de la implementación con mayor convicción y la posibilidad de cometer menos errores, ya que la rigurosidad es prioritaria y enriquecedora.
Ahora bien, la especificación hace referencia a algo formal, concreto, no simplemente a una lista de requerimientos junto a sus «posibles» soluciones. No; la idea es definir matemáticamente cómo funcionará el algoritmo para, así, evitar los posibles errores en una futura implementación. La implementación es involucrarnos directamente en los detalles de la herramienta para hacer realidad dicha especificación. Lamentablemente, en algunos círculos de programadores se tiende a omitir la primera etapa, tanto por responsabilidad personal (interna) como desde la empresa donde se trabaja (externa). Reducir el tiempo de desarrollo se prioriza a toda costa, aun dejando de lado la calidad que viene ligada a la especificación. Esto trae consigo una debilidad en el desarrollo de software, porque no se piensa antes de programar. Por ello, a continuación, analizaremos la fase de especificación.
2.2 ESPECIFICACIÓN
La especificación es la búsqueda de la exactitud (correctness en inglés) de un sistema computacional. Indudablemente, no es algo nuevo a la hora de construir algoritmos. Existen diversas formas de aplicarla, una de ellas, y la más clásica, es la verificación formal.
Puesto que hoy en día existe una omisión casi completa de este tema, es lo que explicaremos a continuación. Creemos que será de gran ayuda para un programador o programadora a quien le interese conocer nuevas técnicas para validar sus algoritmos y no tan solo usar pruebas unitarias como un mecanismo unívoco de aproximación a la reducción total de errores.
2.2.1 Verificación formal
Dentro de la computación tenemos la ingeniería de software, que es un área particularmente relacionada con el ciclo de vida de un producto, la gestión de personas, la metodología de desarrollo, la planificación y el diseño de pruebas, entre otras labores. Y dentro de la misma tenemos la verificación de software, la cual es una disciplina dividida en dos categorías: estática y dinámica.
La verificación formal es parte de la estática, y la dinámica está relacionada al conocido proceso de testing para encontrar errores (bugs en inglés) en un software (aunque esta última se podría ver más como una «validación» que una verificación).
La verificación formal es un área que trata sobre la correctitud de un algoritmo; es decir, hace referencia a si un algoritmo cumple o no con su especificación. Un algoritmo es correcto si cumple lo siguiente: (1) hace lo que dice la especificación; (2) los valores de entrada generan los valores «correctos» de salida, y (3) se ejecuta en un tiempo finito (es decir, evita caer en el problema de la parada [se refiere a que no se puede determinar si un algoritmo entrará en un ciclo infinito que nunca terminaría de ejecutarse]).
Esta área fue introducida por Robert W. Floyd en su artículo «Assigning Meanings to Programs» («Asignar significados a los programas»). Por medio de aserciones lógicas se comprueba la validez de un algoritmo haciendo uso de pruebas de correctitud, equivalencia y terminación. El mismo autor menciona en dicho artículo: «este documento intenta proporcionar una base adecuada para las definiciones formales de los significados de los programas en los lenguajes de programación apropiadamente definidos.».
Cada instrucción de un algoritmo es comprobada a través de expresiones lógicas (aserciones). Es decir, podemos comprobar la validez de un algoritmo en el ámbito de la especificación sin necesidad de ejecutarlo para saber si devolverá el valor correcto. Es por esto que se trata de una verificación estática.
Por su mismo mecanismo, la verificación formal es más compleja de realizar que el testing, ya que se debe pensar y analizar exhaustivamente cómo trabajará cada algoritmo, a través de un conjunto de aserciones bien definidas, desde los argumentos de entrada hasta los de salida. Una técnica formal que nos ayuda a trabajar con esto es la llamada lógica de Hoare.
Lógica de Hoare
Tony Hoare, en su artículo «An Axiomatic Basis for Computer Programming» («Una base axiomática para la programación computacional»), introdujo un sistema formal con un conjunto de reglas lógicas aplicadas sobre declaraciones en un lenguaje determinado para verificar la correctitud de un algoritmo (se le conoce como lógica de Hoare o lógica de Floyd-Hoare).
Básicamente es una forma de axiomatizar un algoritmo. Se le dice «Hoare Triple» a la fórmula {ϕ1} A {ϕ2}, donde A es un algoritmo definido en algún lenguaje formal imperativo, ϕ1 es una precondición y ϕ2 una poscondición. (En la literatura se usa la palabra «program» [que vendría siendo un programa computacional] en vez de «algoritmo», dado que se enfoca más en un conjunto de estos últimos; en nuestro caso, para simplificar esto, usaremos solamente «algoritmo».)
Por ejemplo, podemos crear la gramática de un simple lenguaje imperativo utilizando la notación EBNF (esta la veremos en detalle en el capítulo 4):
Así, esta gramática puede soportar, por ejemplo, los siguientes códigos fuente:
A continuación, veamos cuatro ejemplos —bastante triviales pero instructivos— donde podemos verificar un posible defecto en un algoritmo escrito en este lenguaje usando la lógica de Hoare:
1. {x > 0} x := * 2; {x ≥ 2}
2. {x == y – 1} x := x + 1; y := y + 2; {x == y}
3. {x == y == z} x := y + 1; z := x + 1; {(x > y) < z}
4. {(x > y) ∧ (x ≥ 0) ∧ (y > 0)}
if x > 0 begin
x := y – 1;
else
x := y * –2;
end
{x < y}
Cada uno de los ejemplos anteriores es válido. Siempre que la precondición sea verdadera, la poscondición debe cumplirse; en caso contrario, tenemos un error en nuestro algoritmo. Por ejemplo, si vemos el caso de (1), si reemplazamos por cualquier número mayor a 0, el valor de x después de la ejecución del algoritmo debe ser mayor o igual a 2. Y, dado que el algoritmo incrementa x por su doble, esto siempre será verdadero. Lo mismo ocurre en los ejemplos siguientes. En caso contrario, si la precondición o la poscondición no se cumplen, entonces el algoritmo no concreta la verificación y, por tanto, no es válido. Entonces, si se le asigna el valor 0 a x en (1), este no sería válido porque no puede cumplir con la primera precondición: x > 0.
La lógica de Hoare nos permite pensar en las condiciones exactas de los valores de entrada y salida. O sea, podemos definir correctamente el estado previo y posterior a la ejecución del algoritmo. ¿Cómo? Usando reglas. Conozcamos algunas de ellas:
Regla de composición. Utiliza reglas de inferencias, que tienen la siguiente estructura:
Si tenemos dos axiomas en la parte superior,
podemos inferir la siguiente regla: {ϕ1} A1; A2; {ϕ3}. Esto quiere decir que, si las instrucciones superiores son verdaderas por inferencia, las inferiores también lo serán.
Por ejemplo, las siguientes instrucciones cumplen esta regla:
Regla de iteraciones. La podemos usar cuando necesitamos comprobar la correctitud de un algoritmo que usa ciclos o bucles (por ejemplo, while).
Nos permite comprobar si una variable se mantiene «invariante»7, es decir, si su estado se mantiene igual antes y después del ciclo.
Esta regla quiere decir que ϕ1 es la expresión lógica que se mantiene invariante antes y después de A1; por otro lado, ϕ2 es la expresión que permite terminar el while (evitando así un bucle infinito).
Un ejemplo de esta regla es el siguiente:
En el ejemplo superior, vemos que el axioma (x > 0 ∧ x < 10) es ϕ2, y dado aquello, se evaluará en el while hasta que x sea igual o superior a 10. Por tanto, la variable se irá incrementando, pero seguirá siendo invariante a la expresión y < 10.
Herramientas para la verificación formal
Es posible aplicar estas técnicas a ambientes productivos. Las siguientes herramientas permiten realizar verificación formal en distintos lenguajes de programación:
• Boogie8: es un lenguaje de verificación formal intermedio. Permite utilizar otros lenguajes diseñados para la verificación (por ejemplo, Havoc para C y Spec# para C#).
• Why39: es una plataforma para verificación de software. Provee un lenguaje llamado Why3ML que también puede servir como intermediario de otros lenguajes de verificación.
No obstante, también existen los lenguajes de especificación que están diseñados puramente para la verificación formal. No son lenguajes de programación. Estos tienen la ventaja de omitir detalles innecesarios que contienen los lenguajes de programación para, en cambio, centrarse en algo importante: pensar en un alto nivel el diseño de un software. Dos de los más relevantes están a continuación:
• TLA+10: es un pequeño lenguaje de verificación formal similar a las matemáticas. Especialmente utilizado para algoritmos distribuidos y concurrentes. Según el mismo sitio web «it’s the software equivalent of a blueprint» («es el equivalente a un plano en el software»). Su creador fue Leslie Lamport.
• Coq11: es un sistema formal para realizar demostraciones matemáticas (proofs en inglés) de algoritmos y teoremas.
Hemos incorporado en el apéndice B un pequeño tutorial de TLA+ que es, en cierta medida, nuestro lenguaje de especificación preferido. Por su sencillez y elegancia para expresar operaciones matemáticas y por aplicar el concepto de «invariancia inductiva», cuyo significado puede descubrir en dicho apartado.
En consecuencia, la verificación formal aspira a pensar cómo debe funcionar un algoritmo y no, simplemente, seguir una estrategia de prueba y error. Persigue el siguiente lema: debemos pensar antes de programar.
