A equivalência contextual de um idioma com `quote`-`eval` é trivial ou não?

13

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:αevalquote

A princípio, pensei que em linguagens com um recurso quote- evalcomo LISP [3] não havia distinção de tipo entre objetos sintáticos e objetos executáveis. De fato quote- evalparece suficientemente seguro no LISP porque, embora quotepareça sintaticamente um operador bona fi de, digamos cond, 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 passar quotecomo um parâmetro para um procedimento). Ainda assim, ainda não vi exemplos convincentes de onde o recurso quote- evalvaleu a pena.

Independentemente de uma falha menor nesses comentários que possa induzir o leitor a inferir que isso condpoderia ser passado como parâmetro para um procedimento. Se eu entendi direito, o que Meyer disse " quote- evalparece suficientemente seguro" significa que quote- evalpode 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.

dia
fonte
1
Eu sugeriria considerar se você poderia tornar a pergunta mais específica: existem diferentes maneiras de implementar eval / quote como construções e várias opções para projetar equivalências contextuais para esses cálculos. Uma publicação recente e interessante é Reasoning About Multi-Stage Programs de Inoue, Taha.
Martin Berger
1
A principal distinção é entre CTMP (metaprogramação em tempo de compilação, como exemplificado por Template Haskell, Lisp / Scheme / Racket e Converge , e RTMP (metaprogramação em tempo de execução, como avaliação de Javascript ou MetaOCaml). . Aqui é um talk visão geral eu dei alguns meses atrás sobre este assunto, bastante superficial Temo Quanto equivalências contextuais, pouco trabalho tem sido feito, principalmente possuir ao estado fluido de apoio meta-programação de programação..
Martin Berger
1
@ plmday: BTW, a linguagem de programação idealizada que Wand formaliza em The Theory of Fexprs Is Trivial é bem diferente da metaprogramação de Lisp. O primeiro é RTMP, o segundo (dependendo de implementações concretas) não é.
Martin Berger
1
@MartinBerger: Você pode postar sua palestra em pdf?
Dave Clarke
1
@ Dave Clarke, claro, aqui está! Feedback bem-vindo.
Martin Berger

Respostas:

2

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.

Sam Tobin-Hochstadt
fonte
Eu acho que há uma maneira de excluir (quote []), em vez de ilusões, como um contexto: descartar a idéia de tratar 'datumcomo açúcar sintático para (quote datum), então '[], como "[]"não é mais um contexto. As macros de esquema foram obscurecidas de quotequalquer maneira.
dia
Eu não entendo o seu comentário, @day. Por que o relacionamento entre 'datume (quote datum)muda alguma coisa?
Sam Tobin-Hochstadt 23/03
Se quoteé um construto de linguagem e um 'datumdesejo para as (quote datum)pessoas, é mais provável que as pessoas argumentem que (quote [])é um contexto. Se removermos quoteda linguagem principal, mas oferecermos suporte à 'datumsintaxe literal , é provável que eles argumentem menos porque o similar "[]"é bem conhecido por não ser um contexto.
dia
@ dia, isso é um mal-entendido. Não existe uma definição correta de "contexto". É que contextos diferentes suportam noções diferentes de equivalência contextual. Por exemplo, o espaço em branco é semanticamente significativo no "[]"contexto, mas não no (quote [])contexto. O que as pessoas podem argumentar não está aqui nem ali.
Sam Tobin-Hochstadt 23/03
Concordo que não existe uma definição correta de contexto. Mas há uma definição tradicional baseada na sintaxe abstrata, aquela que Wand usa em seu artigo e Meyer usa em seu artigo, para questionar o status da equivalência contextual de Lisp. O que você sugeriu é substituir a definição tradicional de contexto pelo contexto de avaliação. O que sugeri é manter a definição tradicional de contexto, removendo quoteda 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.
dia