En [1], Mitchell Wand demostró que agregar fexprs al cálculo lambda puro trivializa la teoría de la equivalencia contextual, lo que significa que dos términos son contextualmente equivalentes si son congruentes. Al explorar el trabajo relacionado, dijo: "nuestro resultado extiende una vieja observación de Albert Meyer [2] y hace que la equivalencia contextual sea trivial". Pero en referencia a [2], lo que se puede encontrar es solo la siguiente declaración de Meyer:eval
quote
Primero pensé que en los lenguajes con una característica
quote
-eval
como LISP [3] no había distinción de tipo entre objetos sintácticos y ejecutables. De hechoquote
,eval
parece lo suficientemente seguro en LISP porque, aunquequote
sintácticamente parece un operador de buena fe, como por ejemplocond
, realmente no se comporta como uno (solo tiene comportamiento en tiempo de análisis, no en tiempo de ejecución, por ejemplo, uno no puede pasarquote
como parámetro de un procedimiento). Aún así, todavía tengo que ver convencer ejemplos en los quequote
-eval
característica es que vale la pena.
Independientemente de una falla menor en estos comentarios que puede inducir a error al lector a inferir que cond
podría pasarse como parámetro de un procedimiento. Si he entendido bien, lo que dijo Meyer " quote
- eval
parece lo suficientemente seguro" significa que quote
- eval
no puede trivializar la teoría ecuacional, aunque él no ofrecen una prueba.
EDITAR:
Según lo sugerido por Martin, dado que los tres documentos citaron el trato con los idiomas familiares de LISP, coloquemos la pregunta en esta misma configuración. ¿Es la equivalencia contextual de un lenguaje con quote
- eval
, en particular LISP, en la tierra trivial o no?
[1] Mitchell Wand, The Theory of Fexprs Is Trivial . Lisp y Symbolic Computation 10 (3): 189-199 (1998).
[2] Albert Meyer, Taller de lógica de programación en desarrollo de software formal. 1984
[3] John McCarthy, funciones recursivas de expresiones simbólicas y su cómputo por máquina, Parte I . Comunicaciones de la ACM en abril de 1960.
Respuestas:
Primero, esto depende completamente de lo que consideres como tu conjunto de contextos. Si
(quote [])
es un contexto, entonces la equivalencia contextual es equivalencia sintáctica.Tradicionalmente, los contextos de equivalencia contextual se consideran contextos en los que pueden aparecer "expresiones", en cualquier significado que tenga en el lenguaje. Esto excluye contextos como
"[]"
, donde el contexto coloca su argumento dentro de un literal de cadena. Este tipo de contextos también fueron descartados por Quine cuando el IIRC describió originalmente la transparencia referencial.Desde esta perspectiva, creo que
(quote [])
tampoco es un contexto. En cambio, los contextos son los lugares donde la evaluación de expresiones podría suceder potencialmente, como en el cuerpo de una función o en el argumento de una aplicación.Potencialmente problemático, esto significa que en un programa Lisp con macros (o un programa Racket o Scheme) no sabes cuáles son los contextos hasta que ejecutas el proceso de expansión de macro potencialmente no determinante, porque ni siquiera sabes dónde están las expresiones son. Si crees que esto es un problema o no, es principalmente una cuestión filosófica más que técnica.
fuente
(quote [])
, en lugar de ilusiones, como contexto: descartar la idea de tratar'datum
como azúcar sintáctica para(quote datum)
, entonces'[]
, como"[]"
ya no es un contexto. Las macros del esquema se han oscurecido dequote
todos modos.'datum
y(quote datum)
cambia algo?quote
trata de una construcción del lenguaje y se'datum
desugará(quote datum)
, es más probable que las personas argumenten que(quote [])
es un contexto. Si eliminamosquote
del lenguaje central, pero admitimos la'datum
sintaxis literal , entonces es menos probable que lo argumenten porque"[]"
se sabe que lo similar no es un contexto."[]"
contexto, pero no en el(quote [])
contexto. Lo que la "gente" podría discutir no es ni aquí ni allá.quote
de la sintaxis abstracta, pero apoyando la sintaxis literal (concreta) de la cita (insignificante en el espacio). Por lo que puedo ver, ambas formas conducen a "No" a la pregunta original.