Quartz 4

2026-03-25

6 min read

¿Qué significa que dos cosas sean iguales?

Si hablamos de todas las cosas en general, parece una pregunta filosófica. Una respuesta válida podría ser: depende de qué cosas estemos hablando.

En lógica proposicional, dos proposiciones (digamos, y ) son iguales si podemos demostrar que son lógicamente equivalentes, es decir, demostrar que .

¿Y en Matemáticas? Todos los matemáticos estarían de acuerdo en que $0 + x = x$ y $x + 0 = x$ son ambas igualdades matemáticas verdaderas. Sin embargo, en Ciencias de la Computación, necesitamos ser mucho más precisos y distinguimos entre 3 tipos de igualdades.

1. Igualdad Sintáctica

Dos expresiones son iguales solo si están escritas exactamente con los mismos caracteres y en el mismo orden.

  • Ejemplo: x + 0 y x + 0 son sintácticamente iguales.
  • Contraejemplo: x + 0 y x no son sintácticamente iguales (aunque sepamos que matemáticamente valen lo mismo).

2. Igualdad por Definición

Como sugiere el nombre, este tipo de igualdad depende estrictamente de las definiciones y de los detalles de implementación en nuestro código. Por ejemplo, la suma en los números naturales se define comúnmente por recursividad:

data Nat = Zero | Succ Nat
 
add :: Nat -> Nat -> Nat
add x Zero = x
add x (Succ y) = Succ (add x y)

Si x y y son números naturales, en la definición de add x y tenemos que elegir sobre cuál variable hacer la recursión. Aquí optamos por y.

  • Esto significa que add x Zero se define directamente como x.
  • Dicho de otro modo, x + 0 y x son iguales por definición. Notemos que esta es una igualdad más débil que la sintáctica: dos cosas pueden ser iguales por definición sin serlo visualmente.

Por otro lado, ¿qué pasa con ? Para demostrar esto en nuestro programa, necesitamos algo más que recurrir a la definición base; necesitamos hacer una demostración por inducción. Por lo tanto, aunque es verdadero, no es verdadero por definición bajo nuestra implementación actual. (Nota: Si hubiéramos definido la suma haciendo recursión sobre la primera variable, las conclusiones serían exactamente las opuestas).

3. Igualdad Proposicional

Este es el tipo de igualdad más flexible y el más familiar para los matemáticos. Dos términos y son proposicionalmente iguales si se puede construir una demostración de tipo .

Por ejemplo, si x es un número natural, entonces x, x + 0, 0 + x y x + 3 - 3 son todos proposicionalmente iguales.

Así, si y son dos elementos del mismo tipo ( y ), podemos decir que son iguales si existe una prueba .

Equivalencia de Tipos: ¿Cuándo dos tipos son “iguales”?

Si tenemos no uno, sino dos tipos distintos y , ¿cómo podemos saber si son equivalentes? Para esto, necesitamos construir un elemento . Para construir dicho elemento, necesitamos demostrar 4 cosas:

  1. Una función
  2. Una función
  3. Una demostración
  4. Una demostración A la estructura se le denomina isomorfismo o biyección, pero a partir de aquí nos referiremos a ella como equivalencia.

La tarea de equivalencias

De tarea les pedí que escribieran dos funciones ( y ) para los siguientes pares de tipos:

Tipo ATipo B
b -> a, c -> aEither b c -> a
c -> (a, b)(c -> a, c -> b)
c -> (b -> a)(b, c) -> a
Como pueden ver ahora, lo que en realidad les estaba pidiendo era que demostraran que era equivalente a () para cada caso particular.

Aquí podrían preguntarse: ¿No hacía falta también demostrar formalmente que y ? Sí, por supuesto. Pero en este ejercicio solo hacía falta que el código compilara. ¿Por qué? Porque al usar variables de tipo (a, b, c), Haskell nos obliga a programar funciones que sean biyectivas.

Sin embargo, si usáramos tipos concretos, podríamos escribir programas que compilan perfectamente pero que fallan matemáticamente. Por ejemplo, intentemos “demostrar” que :

f :: Bool -> Bool
f x = True
 
g :: Bool -> Bool
g x = False

Este código compila sin errores en Haskell. Pero si evaluamos , el resultado es False. La demostración de ha fallado.

El Límite de Haskell: Tipos Dependientes

Incluso si quisiéramos exigirle a Haskell las demostraciones matemáticas y , no podríamos escribirlas en el lenguaje. Para hacer esto, necesitamos un lenguaje más expresivo con un sistema de tipos dependientes, como LEAN o Rocq.

¿Qué tienen LEAN o Rocq que Haskell no tiene? Una de tantas cosas es la representación de la igualdad proposicional a nivel de tipos.

Sin embargo, como sugieren los nombres True y False de los constructores de Bool, la frontera entre “evaluar un programa” y “demostrar una proposición” a veces se difumina. Algunas proposiciones son decidibles, lo que significa que pueden ser verificadas computacionalmente como una simple función booleana. La función que evalúa si la proposición es verdadera o falsa se llama procedimiento de decisión, y nos devuelve la evidencia de su veracidad o falsedad.

Algunos ejemplos de igualdades decidibles incluyen la igualdad y desigualdad de números, la igualdad de cadenas de texto (String), y combinaciones de proposiciones que a su vez son decidibles.

Pero no todas las proposiciones son decidibles. Si lo fueran, las computadoras podrían demostrar cualquier verdad matemática simplemente ejecutando un procedimiento de decisión, ¡y los matemáticos se quedarían sin trabajo!

Más específicamente, en Haskell, las proposiciones decidibles sobre igualdad tienen una instancia de la Type Class Eq, donde el método (==) actúa como este procedimiento de decisión. Intentar usar una proposición (o comparar un tipo) que no es decidible como si fuera un simple Bool resulta en un fallo, pues el compilador no encuentra la instance de Eq correspondiente.

Por ejemplo, decidir si dos funciones hacen lo mismo (como \x -> x * 2 y \y -> 2 * x) no es decidible de forma general. Si intentamos forzar a Haskell a usar el procedimiento de decisión con ellas, obtendremos el siguiente error:

ghci> "OM" == "MO"
False
ghci> 1 == 1
True
ghci> let x = \x -> x * 2
ghci> let y = \y -> 2 * x
ghci> x == y
 
<interactive>:
 • No instance for ‘Eq (Integer -> Integer)’ arising from a use of ‘==’

Referencias

Graph View

Backlinks