Em [1], Mitchell Wand demonstrado que a adição de FEXPRs para o cálculo lambda puro trivializes a teoria de equivalência contextual, o que significa que dois termos são contextualmente equivalente sse eles são -congruent. Ao explorar o trabalho relacionado, ele foi "o nosso resultado estende uma velha observação de Albert Meyer [2] que e tornar equivalência contextual trivial". Mas, referindo-se a [2], o que pode ser encontrado é apenas a seguinte declaração de Meyer:eval
quote
A princípio, pensei que em linguagens com um recurso
quote
-eval
como LISP [3] não havia distinção de tipo entre objetos sintáticos e objetos executáveis. De fatoquote
-eval
parece suficientemente seguro no LISP porque, emboraquote
pareça sintaticamente um operador bona fi de, digamoscond
, ele realmente não se comporta como um (ele só tem comportamento no tempo de análise, não no tempo de execução, por exemplo, não se pode passarquote
como um parâmetro para um procedimento). Ainda assim, ainda não vi exemplos convincentes de onde o recursoquote
-eval
valeu a pena.
Independentemente de uma falha menor nesses comentários que possa induzir o leitor a inferir que isso cond
poderia ser passado como parâmetro para um procedimento. Se eu entendi direito, o que Meyer disse " quote
- eval
parece suficientemente seguro" significa que quote
- eval
pode não trivializar a teoria equacional, embora ele não tenha oferecido uma prova.
EDITAR:
Conforme sugerido por Martin, como todos os três documentos citados lidam com os idiomas da família LISP, vamos colocar a questão nessa mesma configuração. A equivalência contextual de uma língua com quote
- eval
, em particular o LISP, na Terra é trivial ou não?
[1] Mitchell Wand, a teoria de Fexprs é trivial . Lisp e Symbolic Computation 10 (3): 189-199 (1998).
[2] Albert Meyer, Puzzles no Workshop de Lógica de Programação sobre Desenvolvimento Formal de Software. 1984
[3] John McCarthy, Funções recursiva de expressões simbólicas e seu cálculo por Máquina, Parte I . Comunicações da ACM em abril de 1960.
Respostas:
Primeiro, isso depende inteiramente do que você considera seu conjunto de contextos. Se
(quote [])
for um contexto, a equivalência contextual é equivalência sintática.Tradicionalmente, os contextos de equivalência contextual são considerados contextos nos quais "expressões", em qualquer significado que tenha na linguagem, podem aparecer. Isso exclui contextos como
"[]"
, onde o contexto coloca seu argumento dentro de uma string literal. Esses tipos de contextos também foram descartados pelo IIRC por Quine quando ele originalmente descreveu a transparência referencial.Nesta perspectiva, acho que
(quote [])
também não é um contexto. Em vez disso, os contextos são os locais onde a avaliação da expressão poderia potencialmente acontecer, como no corpo de uma função ou no argumento de um aplicativo.Potencialmente, problematicamente, isso significa que em um programa Lisp com macros (ou um programa Racket ou Scheme) você não sabe quais são os contextos até executar o processo de expansão de macro potencialmente não-determinante, porque você nem sabe onde as expressões estamos. Se você acha que isso é um problema ou não, é principalmente uma questão filosófica, e não técnica.
fonte
(quote [])
, em vez de ilusões, como um contexto: descartar a idéia de tratar'datum
como açúcar sintático para(quote datum)
, então'[]
, como"[]"
não é mais um contexto. As macros de esquema foram obscurecidas dequote
qualquer maneira.'datum
e(quote datum)
muda alguma coisa?quote
é um construto de linguagem e um'datum
desejo para as(quote datum)
pessoas, é mais provável que as pessoas argumentem que(quote [])
é um contexto. Se removermosquote
da linguagem principal, mas oferecermos suporte à'datum
sintaxe literal , é provável que eles argumentem menos porque o similar"[]"
é bem conhecido por não ser um contexto."[]"
contexto, mas não no(quote [])
contexto. O que as pessoas podem argumentar não está aqui nem ali.quote
da sintaxe abstrata, mas apoiando a sintaxe literal (concreta) da citação (insignificante em espaço). Pelo que posso ver, os dois lados levam a "Não" à pergunta original.