Aquí está el contexto ( Estructura e interpretación de programas de computadora , sección 1.1.8, bajo el título "Nombres locales"):
Un parámetro formal de un procedimiento tiene un papel muy especial en la definición del procedimiento, ya que no importa qué nombre tenga el parámetro formal. Tal nombre se llama variable enlazada , y decimos que la definición del procedimiento une sus parámetros formales. El significado de una definición de procedimiento no cambia si una variable enlazada cambia constantemente de nombre a lo largo de la definición.
Al final de esa última línea, hay una nota al pie (26), que dice:
El concepto de cambio de nombre consistente es realmente sutil y difícil de definir formalmente. Los lógicos famosos han cometido errores vergonzosos aquí.
¿A qué o a quién se refiere el texto? ¿Por qué sería difícil definir un "cambio de nombre consistente", qué lógicos han cometido errores al tratar de definir esto, y cuáles fueron esos errores?
Respuestas:
Esta es una respuesta parcial: no tengo idea de a qué errores o personas se refiere SICP. Solo puedo proporcionar algunos consejos sobre "por qué" el cambio de nombre variable puede ser difícil de manejar con precisión.
En primer lugar, parece trivial de definir. Por ejemplo, podemos cambiar el nombre de las variables enlazadas en sumas indexadas
dondee es cualquier expresión, y e{y/x} denota el reemplazo sintáctico de cada x con y . Trivial, ¿verdad?
Bueno, si aplicamos ciegamente la regla anterior, obtenemos
Eso no es bueno. Necesitamos agregar el requisito "y no ocurre en e ", u obtenemos un choque de nombres.
Ahora, considere este cambio de nombre correcto
si queremos cambiar el nombre dex a y , según la regla anterior, podemos hacerlo en el lado derecho, pero no en el lado izquierdo. Eso es inconveniente, ya que los dos difieren solo por un cambio de nombre, por lo que deben manejarse de la misma manera.
Un enfoque típico aquí es recurrir a la redefinición dee{y/x} como "sustitución para evitar la captura", y relajar el requisito " y no ocurre en e " y usar en su lugar " y no ocurre libre en e ".
Luego definimos ocurrencias libres:
Finalmente, captura evitando la sustitución:
El último caso es doloroso. Six=y , la sustitución es no operativa, ya que queremos que afecte solo a las variables libres, y x está vinculada. Entonces el resultado es solo ∑xe .
Siy≠x , nos gustaría decir que (∑xe){t/y}=∑x(e{t/y}) . Sin embargo, esto está mal, en general, ya que si x ocurre libre en t obtenemos una captura.
Espero haberlo hecho bien. (Mi primer intento fue incorrecto, por cierto)
Ahora, imagine tener que lidiar con esta intrincada definición cada vez que queremos probar algo en la teoría PL. Podríamos, pero no queremos. Es aburrido, tedioso, propenso a errores, abarrota la prueba y no proporciona información al lector. Por esta razón, muchos autores de PL simplemente omiten los detalles diciendo (¡o incluso dando por sentado!) Que los términos deben tomarse "hasta el cambio de nombre de la variable", que todas las variables enlazadas se suponen distintas de lo que sea necesario, que asumimos la "convención de Barendregt", o algo por el mismo efecto.
Para ser brutalmente honesto, esto es trampa en pruebas. También podríamos agregar "wink wink, nudge nudge, say no more!" En el mismo espíritu. Esencialmente pedimos piedad y le decimos al lector: "mira, esto es aburrido, no quiero hacerlo, no quieres leerlo; ambos sabemos que, con un gran esfuerzo, podríamos reescribir esta prueba para incluir todos los detalles ".
Técnicamente, es posible explotar este atajo para probar una declaración falsa. Sin embargo, el revisor de pruebas experimentado sabe qué es "moralmente bueno" y que podría perfeccionarse (con gran esfuerzo) y qué es sospechoso. Este último podría incluir algo que depende de la elección real de los nombres enlazados (por lo que realmente no estamos trabajando "hasta" como se prometió). En esos casos, la revisión solicitará más detalles, para que pueda convencerse.
fuente