Bitácora · Lógica · Ensayo

Un corte equivocado rompe las dos piezas

Que una palabra partida por una coma sea un término no dice nada de las dos piezas. Que una de ellas sea término lo dice todo.

En el ensayo anterior un término de reticulado terna era algo que se reescribe: se le aplicaba una identidad y quedaba otro término con el mismo valor. La Guía 9 lo mira desde más abajo. Un término de tipo τ es una palabra, una tira de símbolos, y dos términos son iguales sólo si tienen los mismos símbolos en el mismo orden. Se arman por niveles. En el nivel cero, $T_{0}^{τ}$ , están las variables y los nombres de constante; las variables son palabras concretas, una $X$ seguida de numerales con el último en negrita: $X 1$ , $X 2$ , $X 3$ . Cada nivel nuevo agrega las palabras $f (t_{1}, \dots, t_{n})$ , con $f$ un nombre de función de aridad $n$ y $t_{1}, \dots, t_{n}$ del nivel anterior. El tipo de los reticulados terna no tiene constantes y tiene dos nombres de función binarios, $s$ e $i$ , y ahí el supremo de un supremo se escribe $s (s (X 1, X 2), X 3)$ : una palabra de catorce símbolos, de nivel 2.

Hacen falta dos ideas más. Una palabra $β$ es tramo inicial de $α$ si $α = β γ$ para alguna palabra $γ$ : es un pedazo de $α$ tomado desde el principio. Tramo final es lo mismo desde el final. Y la lectura única (Teorema 3 de la guía) dice que un término que no es variable ni constante se escribe de una sola manera como $f (t_{1}, \dots, t_{n})$ con los $t_{i}$ términos: hay un solo modo de partirlo en nombre y argumentos. La sostiene el mordisqueo (Lema 2): si un término es tramo inicial o final de otro término, son el mismo término. Las definiciones enteras están en Variables y términos de tipo τ y en Mordisqueo y lectura única de términos.

Este ensayo mira la letra chica: «con los $t_{i}$ términos». Que $f (α, β)$ sea un término, con $α$ y $β$ palabras cualesquiera, no dice que $α$ y $β$ lo sean. Pero si se sabe que una de las dos es término, la otra también. La distancia entre esas dos frases se puede contar: un corte por la coma equivocada no rompe una pieza, rompe las dos.

Lo medido

El universo de la simulación son todos los términos de reticulado terna que se arman con las variables $X 1$ , $X 2$ y $X 3$ aplicando $s$ o $i$ a pares de términos ya armados, en tres rondas, sin pasar de 30 símbolos. Son 26 802 términos compuestos, de nivel 1, 2 y 3, y todos tienen la forma $f (α, β)$ de muchas maneras: hay que elegir la coma. Probando cada coma de cada uno como separador salen 103 482 cortes, y se reparten así:

en 26 802 las dos piezas son términos: exactamente uno por término, el de la lectura única;
en 76 680 no es término ninguna de las dos;
en ninguno se rompe una sola.

El corte bueno, además, casi nunca es el primero que se ve. Sólo en 5 310 de los 26 802 la coma buena es la de más a la izquierda —los que tienen una variable como primer argumento—; en los otros 21 492, leer de izquierda a derecha y cortar en la primera coma es cortar mal. El reparto no cambia por eso: esté donde esté la coma buena, todas las otras rompen las dos piezas.

Por qué se rompen las dos

Es una cuenta de paréntesis. Dentro del paréntesis de afuera, la palabra $s (t_{1}, t_{2})$ tiene la coma que separa $t_{1}$ de $t_{2}$ y las comas de adentro de $t_{1}$ y de $t_{2}$ . Un término con comas es de la forma $g (\dots)$ y sus comas están entre sus propios paréntesis. Así que la coma principal es la única donde, contando desde después del primer «(», se cerraron tantos paréntesis como se abrieron. En cualquier otra hay $d \geq 1$ paréntesis abiertos y sin cerrar.

Cortar ahí deja a la izquierda una pieza con $d$ «(» de más. Y como la palabra entera tiene tantos «(» como «)», y el «(» y el «)» de afuera se compensan entre sí, la pieza de la derecha tiene $d$ «)» de más. Ninguna de las dos está balanceada, y una palabra desbalanceada no es término. El corte malo no puede elegir a quién romper: el desbalance de un lado es el del otro con el signo cambiado. Medido, los 76 680 cortes malos cumplen eso sin excepción: la izquierda abre $d$ de más y la derecha cierra exactamente los mismos $d$ de más.

En la simulación se ve en la línea de abajo de cada pieza: los dos contadores están descompensados en espejo. El motivo que da la lectura de afuera cambia —que la pieza no termina en «)», que los paréntesis no cierran, que un «)» cierra antes de tiempo—, pero todos son síntomas de lo mismo.

Por qué alcanza con saber una

El Ejercicio 11, pág. 5, es la versión verdadera del 2(h):

Sea $τ$ un tipo. Si $f \in ℱ_{2}$ y $f (α, t), t \in T^{τ}$ , entonces $α \in T^{τ}$

La cuenta de arriba lo explica: si $t$ es término, está balanceado, así que el corte no puede ser uno malo, y el único corte bueno deja dos términos. La guía lo prueba con lo que ya tiene. Por la lectura única, $f (α, t) = g (s_{1}, s_{2})$ con $s_{1}, s_{2}$ términos, y $g = f$ porque los dos son lo que viene antes del primer «(». Sacando $f ($ de los dos lados queda

α, t) = s_{1}, s_{2})

y acá se compara por atrás, porque lo que se sabe término es $t$ : de $α$ no se sabe nada. Sin el «)» final, $t$ y $s_{2}$ son tramos finales de la misma palabra, así que uno es tramo final del otro, y el mordisqueo dice que son iguales. Cancelando $t$ y la coma, $α = s_{1}$ , que es término. Por adelante no se puede: para usar el mordisqueo sobre $α$ habría que saber que $α$ es término, que es justo lo que se quiere probar. Si el que se sabe término es el primero, $f (t, β)$ , se compara por adelante y sale igual.

El mordisqueo es lo que convierte «una pieza es término» en «el corte es el bueno». La cuenta de paréntesis llega a lo mismo, pero como prueba pide dos invariantes más, cada uno con su inducción: que toda coma de un término queda adentro de sus paréntesis, y que ningún tramo inicial de un término cierra más de lo que abre. El mordisqueo, en cambio, la guía lo da por aceptado: el Ejercicio 9 pide no probarlo.

Leído al revés, el cero de la lista es el Ejercicio 11: un corte que dejara $t$ término y $α$ no sería un contraejemplo. En los 103 482 no aparece ninguno. Eso no prueba nada —lo prueba el lema—, pero muestra que el 2(h) y el 11 no están separados por un caso raro: entre «las dos se rompen» y «las dos sirven» no hay nada en el medio.

Con fórmulas, por atrás cuesta más

El Ejercicio 13(a), pág. 11, es el 2(h) con fórmulas: «Si $α, β$ son palabras tales que $(α \land β) \in F^{τ}$ , entonces $α, β \in F^{τ}$ ». Es falso por lo mismo. En $(((X 1 \equiv X 2) \land (X 1 \equiv X 1)) \land (X 2 \equiv X 2))$ , tomando el primer $\land$ como separador, $α = ((X 1 \equiv X 2)$ tiene dos «(» y un «)». En la simulación está en el modo de fórmulas.

El conteo da igual. Sobre las 225 conjunciones que se arman con los átomos $(X 1 \equiv X 2)$ , $(X 1 \equiv 0)$ y $(0 \equiv X 2)$ usando $\neg$ y $\land$ en dos rondas, hasta 40 símbolos, cada $\land$ probado como separador da 495 cortes: 225 buenos, uno por fórmula; 270 que rompen las dos piezas, y ninguno que rompa una sola. El $\land$ equivocado está metido en algún paréntesis, igual que la coma, y el desbalance se reparte igual.

Lo que cambia es el precio de la prueba. La versión verdadera es el Ejercicio 19, pág. 12: «Si $(α \land β), β \in F^{τ}$ , entonces $α \in F^{τ}$ ». Se compara por atrás, como en el 11, y ahí el mordisqueo de fórmulas da menos. Una fórmula sí puede ser tramo final de otra: $(X 1 \equiv X 2)$ es tramo final de $\neg (X 1 \equiv X 2)$ . En 45 de las 225 conjunciones el segundo miembro termina en otra fórmula más corta, y en los términos eso no pasa nunca. Lo que la Proposición 6 garantiza es que lo que sobra adelante es una tira de $\neg$ y de cuantificadores con su variable, y hay que dar un paso más para descartarlo: si no es vacía, termina en $\neg$ o en el numeral negrita de una variable, y en la palabra lo que viene antes de $β$ es el $\land$ .

Por adelante, en cambio, todo sigue como con términos: una fórmula nunca es tramo inicial propio de otra (Ejercicio 16). Por eso la mitad fácil del bloque de fórmulas es la de adelante, y la difícil la de atrás; está entera en Una fórmula puede ser el final de otra, nunca el principio.

← Anterior Siguiente → Inicio