Dos nombres para la misma función

La consigna, textual: «Sea $τ$ el tipo $(\emptyset, {F1, F2}, \emptyset, {(F1, 2), (F2, 2)})$ . Sea $t \in T^{τ}$ y sea $t^{'}$ el resultado de reemplazar cada ocurrencia de la palabra $F1$ en $t$ por la palabra $F2$ . (a) Pruebe que $t^{'} \in T^{τ}$ . (b) Pruebe que si $𝐀 = (A, i)$ es una estructura de tipo $τ$ tal que $i (F1) = i (F2)$ , entonces para cualquier asignación $\vec{a} \in A^{𝐍}$ se tiene que $t^{' 𝐀} [\vec{a}] = t^{𝐀} [\vec{a}]$ ». No viene de las guías. Va sin notación declaratoria, con asignaciones infinitas.

01 · Qué dice, con un ejemplo

El tipo no tiene constantes ni relaciones: sólo dos nombres de función binarios. Cada nombre es una palabra de dos símbolos, la letra F y un numeral normal: $F1$ no es «F sub 1», es la palabra que tiene una F y después un 1. Los términos son las variables y las palabras $F1 (t_{1}, t_{2})$ y $F2 (t_{1}, t_{2})$ .

En $t = F1 (X 1, F2 (X 2, F1 (X 1, X 3)))$ , de 23 símbolos, la palabra $F1$ ocurre a partir de 1 y a partir de 13. Reemplazar las dos da $t^{'} = F2 (X 1, F2 (X 2, F2 (X 1, X 3)))$ , que es término y tiene el mismo nivel, 3. Con $A = {0, 1, 2, 3, 4}$ , $i (F1)$ e $i (F2)$ los dos el máximo, y $\vec{a} = (1, 3, 2, 2, \dots)$ , los dos términos valen 3. Si en cambio $i (F2)$ es el mínimo, $t^{'}$ vale $\min (1, \min (3, \min (1, 2))) = 1$ , y $t$ , que también tiene un $F2$ , vale $\max (1, \min (3, \max (1, 2))) = 2$ .

El enunciado parece obvio, y la mitad que no lo es está escondida en «reemplazar cada ocurrencia de la palabra». El reemplazo es ciego: busca los dos símbolos F1 seguidos donde estén, sin saber nada de términos. Para que el resultado sea «cambiarle el nombre a cada nodo» hay que saber que la palabra $F1$ sólo aparece como nombre de función: que no hay un F1 armado con el final de una cosa y el principio de otra, ni escondido adentro de una variable o de $F2$ . En este tipo es cierto, y es lo primero que hay que probar.

02 · Las herramientas

Las variables (Guía 9, p. 1): son las palabras $X α$ donde $α$ es la escritura decimal de un natural con el último numeral en negrita y los demás en itálica. No tienen ni la letra F ni numerales normales.

Los niveles (Guía 9, p. 1). Acá $𝒞 = \emptyset$ , así que $T_{0}^{τ} = Var$ , y $T_{k + 1}^{τ} = T_{k}^{τ} \cup {f (t_{1}, t_{2}) : f \in {F1, F2} y t_{1}, t_{2} \in T_{k}^{τ}}$ . La palabra $f (t_{1}, t_{2})$ es la concatenación de $f$ , «(», $t_{1}$ , «,», $t_{2}$ y «)». La Regla de Inducción desde 0 se usa dos veces, una por inciso.

El valor de un término (Guía 10, p. 1): $x_{m}^{𝐀} [\vec{a}] = a_{m}$ , y $f (t_{1}, t_{2})^{𝐀} [\vec{a}] = i (f) (t_{1}^{𝐀} [\vec{a}], t_{2}^{𝐀} [\vec{a}])$ si $t_{1}, t_{2} \in T^{τ}$ . Y la lectura única de términos, que la lista deja usar sin enunciar: un término de este tipo es una variable o es $f (t_{1}, t_{2})$ con únicos $f$ , $t_{1}$ y $t_{2}$ .

El hecho de la palabra $F1$ . Es propio de este tipo y no está en ninguna guía, así que se enuncia y se prueba. Sea $t \in T^{τ}$ :

(i) $t$ termina en un numeral negrita o en «)».
(ii) Si $t \in Var$ , la palabra $F1$ no ocurre en $t$ .
(iii) Si $t = f (t_{1}, t_{2})$ , las ocurrencias de $F1$ en $t$ son la que empieza en la posición 1, cuando $f = F1$ , y las que suceden dentro de $t_{1}$ o de $t_{2}$ . Y toda ocurrencia de $F1$ en $t_{1}$ o en $t_{2}$ es una ocurrencia en $t$ .
(iv) Dos ocurrencias distintas de $F1$ nunca se superponen.

De (iii) y (iv) sale lo que se usa en las dos inducciones: si $t = f (t_{1}, t_{2})$ , entonces $t^{'} = F2 (t_{1}^{'}, t_{2}^{'})$ , donde $t_{1}^{'}$ y $t_{2}^{'}$ son los resultados de reemplazar cada ocurrencia de $F1$ en $t_{1}$ y en $t_{2}$ por $F2$ . Sea $f$ el que sea, la cabeza de $t^{'}$ es $F2$ : si era $F1$ , la ocurrencia de la posición 1 se reemplazó, y si era $F2$ , ya estaba.

03 · La mariposa: dos inducciones con el mismo paso

Las dos metas piden mirar $t^{'}$ por dentro: para que sea término, hay que ver que es de la forma $F2 (t_{1}^{'}, t_{2}^{'})$ con piezas que ya son términos; para calcular su valor, la cláusula del valor necesita esa misma forma. Las dos se apoyan en la descomposición $t^{'} = F2 (t_{1}^{'}, t_{2}^{'})$ , y las dos se prueban por inducción en el nivel de $t$ , porque el nivel baja de $t$ a $t_{1}$ y $t_{2}$ .

En (a), conviene pedir más. El ${Enu}_{k}$ natural sería «si $t \in T_{k}^{τ}$ , entonces $t^{'} \in T^{τ}$ ». Anda, pero en el paso da $t_{1}^{'} \in T_{m_{1}}^{τ}$ y $t_{2}^{'} \in T_{m_{2}}^{τ}$ con niveles distintos, y hay que subir los dos al máximo. Pidiendo $t^{'} \in T_{k}^{τ}$ , el mismo nivel que $t$ , el paso es inmediato: $t_{1}^{'}, t_{2}^{'} \in T_{k}^{τ}$ y entonces $F2 (t_{1}^{'}, t_{2}^{'}) \in T_{k + 1}^{τ}$ . Es verdad porque el reemplazo cambia un nombre por otro de la misma aridad y no toca la forma del árbol.

En (b), la hipótesis trabaja en un solo lugar: en la cabeza, cuando $f = F1$ . La cuenta es $t^{' 𝐀} [\vec{a}] = i (F2) (t_{1}^{' 𝐀} [\vec{a}], t_{2}^{' 𝐀} [\vec{a}])$ , la hipótesis inductiva cambia los argumentos por los de $t$ , y $i (F2) = i (F1)$ cambia la cabeza. Si $f = F2$ no hace falta. Y (b) usa (a) dos veces: para que $t^{' 𝐀} [\vec{a}]$ tenga sentido, y para aplicar la cláusula a $F2 (t_{1}^{'}, t_{2}^{'})$ , que pide $t_{1}^{'}, t_{2}^{'} \in T^{τ}$ .

El ${Enu}_{k}$ de (b) lleva adentro la estructura y la asignación. Como en el Ejercicio 7, ninguna cláusula del valor de un término cambia la asignación, así que se podrían fijar afuera; adentro es el molde de la lista y no cuesta nada.

Con $i (F2) = i (F1)$ el conteo da las 125 asignaciones de $(a_{1}, a_{2}, a_{3})$ en ${0, \dots, 4}^{3}$ , para cualquier término de esas tres variables. Con el mínimo, el primer término se iguala en 25 de las 125 y el tercero, $F1 (F1 (X 1, X 2), X 3)$ , en 5: la hipótesis no es necesaria para que dos valores coincidan alguna vez, es lo que hace que coincidan siempre.

04 · El escarabajo: la prueba escrita

Prueba del hecho de la palabra $F1$ .

(i) Por lectura única, $t$ es una variable, cuyo último símbolo es un numeral negrita, o $t = f (t_{1}, t_{2})$ , cuyo último símbolo es «)». No hay otra posibilidad porque $𝒞 = \emptyset$ .
(ii) Una variable tiene sólo la $X$ y numerales itálicos y negritas. Toda ocurrencia de $F1$ empieza con el símbolo F, que no está en $t$ .
(iii) Sea $t = f (t_{1}, t_{2})$ . Sus símbolos son, en orden: F, el numeral normal de $f$ , «(», los de $t_{1}$ , «,», los de $t_{2}$ y «)». Una ocurrencia de $F1$ empieza en una posición donde hay una F. En la posición 1 hay una F, y la ocurrencia a partir de 1 existe exactamente cuando el símbolo 2 es el 1 normal, o sea cuando $f = F1$ . En la posición 2, en el «(», en la coma y en el «)» final no hay una F. Si la ocurrencia empieza dentro de $t_{1}$ y no está contenida en $t_{1}$ , tiene que empezar en el último símbolo de $t_{1}$ , porque $F1$ tiene dos símbolos; ese símbolo sería una F, y por (i) no lo es. Luego está contenida en $t_{1}$ . Lo mismo dentro de $t_{2}$ . La vuelta es inmediata: si $F1$ ocurre en $t_{1}$ , ocurre en $t$ en la posición corrida.
(iv) Dos ocurrencias que se superponen y son distintas empiezan en posiciones $p$ y $p + 1$ , y entonces el símbolo $p + 1$ es a la vez el 1 de la primera y la F de la segunda. Absurdo. Por eso tiene sentido reemplazar cada ocurrencia simultáneamente.

La descomposición. Si $t = f (t_{1}, t_{2})$ , por (iii) las ocurrencias de $F1$ en $t$ son la de la cabeza, si $f = F1$ , y las de $t_{1}$ y $t_{2}$ . Reemplazar cada una por $F2$ deja la cabeza en $F2$ , los paréntesis y la coma donde estaban, y adentro de cada argumento hace lo mismo que reemplazar cada ocurrencia de $F1$ en $t_{1}$ y en $t_{2}$ . Luego $t^{'} = F2 (t_{1}^{'}, t_{2}^{'})$ .

(a) Prueba. Usaremos la Regla de Inducción desde 0. Para cada $k \in ω$ sea ${Enu}_{k}$ el enunciado:

${Enu}_{k}$ : Si $t \in T_{k}^{τ}$ y $t^{'}$ es el resultado de reemplazar cada ocurrencia de la palabra $F1$ en $t$ por la palabra $F2$ , entonces $t^{'} \in T_{k}^{τ}$ .

Prueba de que ${Enu}_{0}$ es verdadero. Sea $t \in T_{0}^{τ} = Var \cup 𝒞 = Var$ . Por (ii) no hay ocurrencias de $F1$ en $t$ , así que $t^{'} = t \in T_{0}^{τ}$ .
Prueba de que ${Enu}_{k}$ implica ${Enu}_{k + 1}$ . Supongamos que vale Enuk y sea t∈Tk+1τ. Por definición de Tk+1τ hay dos casos.
- Caso $t \in T_{k}^{τ}$ . Por ${Enu}_{k}$ , $t^{'} \in T_{k}^{τ} \subseteq T_{k + 1}^{τ}$ .
- Caso $t = f (t_{1}, t_{2})$ , con $f \in {F1, F2}$ y $t_{1}, t_{2} \in T_{k}^{τ}$ . Por la descomposición, $t^{'} = F2 (t_{1}^{'}, t_{2}^{'})$ , donde $t_{j}^{'}$ es el resultado de reemplazar cada ocurrencia de $F1$ en $t_{j}$ por $F2$ . Como $t_{j} \in T_{k}^{τ}$ , por ${Enu}_{k}$ es $t_{j}^{'} \in T_{k}^{τ}$ , para $j = 1, 2$ . Como $F2 \in ℱ_{2}$ , por definición de $T_{k + 1}^{τ}$ resulta $t^{'} \in T_{k + 1}^{τ}$ .

Por la Regla de Inducción desde 0, ${Enu}_{k}$ vale para todo $k \in ω$ . Dado $t \in T^{τ}$ , hay $k$ con $t \in T_{k}^{τ}$ , y entonces $t^{'} \in T_{k}^{τ} \subseteq T^{τ}$ . ∎

(b) Prueba. Usaremos la Regla de Inducción desde 0. Para cada $k \in ω$ sea ${Enu}_{k}$ el enunciado:

${Enu}_{k}$ : Si $t \in T_{k}^{τ}$ y $t^{'}$ es el resultado de reemplazar cada ocurrencia de la palabra $F1$ en $t$ por la palabra $F2$ , entonces para cualquier estructura $𝐀 = (A, i)$ de tipo $τ$ tal que $i (F1) = i (F2)$ y cualquier asignación $\vec{a} \in A^{𝐍}$ , se tiene que $t^{' 𝐀} [\vec{a}] = t^{𝐀} [\vec{a}]$ .

Por (a), $t^{'} \in T^{τ}$ , así que $t^{' 𝐀} [\vec{a}]$ está definido.

Prueba de que ${Enu}_{0}$ es verdadero. Sea $t \in T_{0}^{τ} = Var$ . Por (ii), $t^{'} = t$ , y $t^{' 𝐀} [\vec{a}] = t^{𝐀} [\vec{a}]$ para cualesquiera $𝐀$ y $\vec{a}$ .
Prueba de que ${Enu}_{k}$ implica ${Enu}_{k + 1}$ . Supongamos que vale Enuk. Sean t∈Tk+1τ, 𝐀=(A,i) de tipo τ con i(F1)=i(F2) y a→∈A𝐍.
- Caso $t \in T_{k}^{τ}$ . Por ${Enu}_{k}$ , $t^{' 𝐀} [\vec{a}] = t^{𝐀} [\vec{a}]$ .
- Caso $t = f (t_{1}, t_{2})$ , con $f \in {F1, F2}$ y $t_{1}, t_{2} \in T_{k}^{τ}$ . Por la descomposición, $t^{'} = F2 (t_{1}^{'}, t_{2}^{'})$ , y por (a), $t_{1}^{'}, t_{2}^{'} \in T^{τ}$ . Por ${Enu}_{k}$ , aplicado a $t_{1}$ y a $t_{2}$ con las mismas $𝐀$ y $\vec{a}$ , $t_{j}^{' 𝐀} [\vec{a}] = t_{j}^{𝐀} [\vec{a}]$ para $j = 1, 2$ . Además $i (F2) = i (f)$ : si $f = F2$ es trivial, y si $f = F1$ es la hipótesis. Por la cláusula (3) de la definición de valor, $t^{' 𝐀} [\vec{a}] = i (F2) (t_{1}^{' 𝐀} [\vec{a}], t_{2}^{' 𝐀} [\vec{a}]) = i (F2) (t_{1}^{𝐀} [\vec{a}], t_{2}^{𝐀} [\vec{a}]) = i (f) (t_{1}^{𝐀} [\vec{a}], t_{2}^{𝐀} [\vec{a}]) = t^{𝐀} [\vec{a}]$

Por la Regla de Inducción desde 0, ${Enu}_{k}$ vale para todo $k \in ω$ , y como todo $t \in T^{τ}$ está en algún $T_{k}^{τ}$ , vale (b). ∎

05 · Lo que hace perder puntos y lo que se lleva

Lo que hace perder puntos. Escribir « $t^{'} = F2 (t_{1}^{'}, t_{2}^{'})$ » sin justificar dónde ocurre la palabra $F1$ : es la única parte del ejercicio que no es una cuenta, y la consigna habla de palabras, no de nodos. Olvidar el caso $f = F2$ , donde la cabeza no cambia y la hipótesis no se usa. En (b), calcular $t^{' 𝐀} [\vec{a}]$ sin citar (a). Y escribir un solo ${Enu}_{k}$ para los dos incisos sin decir cuál se prueba primero: (b) necesita (a) ya probado.

Lo que se lleva. El hecho (iii) es, para un nombre, lo que el Lema 4 de la Guía 9 dice de los subtérminos: una ocurrencia que empieza adentro de un argumento no se sale de él. Con subtérminos es la pieza central del Ejercicio 7: allí se reemplazan ocurrencias de un término que vale lo mismo, acá un nombre que se interpreta igual, y el paso de la inducción es el mismo. La versión con relaciones y fórmulas es el Ejercicio 26, ya dentro de la notación declaratoria.

Para tener a mano

La palabra $F1$ sólo ocurre como cabeza: las variables no tienen la letra F, y un término nunca termina en F, así que una ocurrencia que empieza en un argumento no se sale de él.
Si $t = f (t_{1}, t_{2})$ , entonces $t^{'} = F2 (t_{1}^{'}, t_{2}^{'})$ , sea $f$ el que sea.
(a) con ${Enu}_{k}$ : si $t \in T_{k}^{τ}$ , entonces $t^{'} \in T_{k}^{τ}$ . Pedir el mismo nivel ahorra subir dos niveles al máximo.
(b) con ${Enu}_{k}$ cuantificando $𝐀$ con $i (F1) = i (F2)$ y $\vec{a}$ ; la hipótesis se usa sólo en la cabeza, cuando $f = F1$ ; (a) se cita para que $t^{' 𝐀} [\vec{a}]$ tenga sentido.