Logica de predicados explicada para programadores

Hillel Wayne, autor del libro 'Logic for Programmers', ha publicado en su blog el segundo capitulo de su obra como articulo gratuito. El objetivo: ofrecer un recurso accesible para programadores que quieran aprender logica formal sin tener que comprar el libro (aunque el propio autor admite, con humor, que tambien es una forma de promocionarlo).

El capitulo, titulado 'A Crash Course in Logic', arranca con una idea sencilla: un predicado es, en esencia, una funcion que devuelve un booleano. Cualquier programador ha escrito decenas de ellos, como Positive(x) que comprueba si x es mayor que cero, o IsSum(x, y, z) que verifica si x + y = z. Pero Wayne matiza: los predicados son un concepto matematico, no de programacion. Una funcion de codigo necesita una forma de calcular el resultado, mientras que un predicado solo define cual es el resultado. Asi, RAMAtLeast(c, r) es verdadero si el ordenador c tiene al menos r bytes de RAM, sin importar como se implemente esa comprobacion.

Esta distincion permite que los predicados sean mas abstractos que las funciones de programacion. Pueden expresar cosas que ni siquiera sabemos computar, como NotAlone() (verdadero si existen los alienigenas) o RainyDayInCa(date) (si llovio en Canada ese dia). Para distinguir entre predicados concretos y abstractos, Wayne usa una convencion visual: los abstractos van entre comillas invertidas (...), y ademas los predicados se escriben en TitleCase mientras que las funciones normales van en snake_case.

El problema de la ambiguedad

Uno de los ejemplos mas ilustrativos del articulo es el de un programa con requisitos confusos. El enunciado decia: 'El ordenador debe tener suficiente RAM y una CPU rapida o una buena tarjeta grafica (GPU)'. En ingles suena natural, pero al formalizarlo con predicados aparece la ambiguedad: RAM(c) && CPU(c) || GPU(c) puede interpretarse como (RAM(c) && CPU(c)) || GPU(c) o como RAM(c) && (CPU(c) || GPU(c)). Ambas tienen sentido en lenguaje natural pero dan resultados distintos para ciertos ordenadores. Wayne monta una tabla de verdad para demostrarlo: hay dos combinaciones de valores donde una interpretacion devuelve verdadero y la otra falso.

El autor usa esto para defender que la logica formal es menos ambigua que el ingles. Y de paso, introduce el operador de implicacion =>, que en matematicas equivale a !P || Q. Este operador es util para expresar condiciones como 'si ejecutas la version nativa, entonces necesitas un ordenador potente, pero si no, cualquier ordenador vale'. La expresion Native(p) => Beefy(c) se lee como 'si Native(p) es verdadero, entonces Beefy(c) debe serlo tambien'.

Conjuntos y tipos

El capitulo tambien toca los conjuntos, que en logica sirven para acotar los tipos de los argumentos. En programacion, si una funcion espera un ordenador, no le pasarias un poodle con una GPU pegada (aunque el ejemplo es de Wayne). En matematica, se escribe c in Computer para indicar que c pertenece al conjunto de ordenadores. Wayne propone una sintaxis inspirada en la programacion: CanRunProgram(c: Computer) para indicar que c debe ser un elemento de Computer.

En definitiva, el articulo es un curso intensivo que mezcla teoria con ejemplos practicos y ejercicios con soluciones al final. Wayne no solo explica los conceptos, sino que muestra como aplicarlos a problemas reales de especificacion de sistemas. Para quien quiera profundizar, el libro completo ya esta a la venta, pero este capitulo gratuito es una puerta de entrada solida.

Lo que queda por ver es si el resto del libro mantiene este nivel de claridad. Si el autor logra convertir la logica formal en algo tan digerible para programadores como promete, puede que muchos desarrolladores dejen de verla como una materia oscura y la adopten como herramienta cotidiana.