В [1] Митчелл Ванд продемонстрировал, что добавление fexprs к чистому лямбда-исчислению упрощает теорию контекстуальной эквивалентности, означая, что два термина контекстуально эквивалентны, если они -конгруэнтны. При изучении соответствующей работы, он пошел «наш результат расширяет старое наблюдение Альберт Мейер [2] , что и визуализации контекстная эквивалентности тривиальным». Но, ссылаясь на [2], можно найти только следующее утверждение Мейера:eval
quote
Я первая подумала , что в языках с
quote
-eval
функциями , такими как LISP [3] не было никакого типа различия между синтаксическими и исполняемыми объектами. На самом делеquote
-eval
кажется достаточно безопасным в LISP, потому что, хотяquote
синтаксически выглядит как добросовестный оператор, как, скажемcond
, он действительно не ведет себя как один (он работает только во время разбора, а не во время выполнения, например, никто не может пройтиquote
в качестве параметра к процедуре). Тем не менее, я до сих пор увидеть убедительные примеры , гдеquote
-eval
функция была стоящей.
Независимо от одного незначительного недостатка в этих комментариях, который может ввести читателя в заблуждение, сделать вывод, что cond
можно передать в качестве параметра в процедуру. Если я правильно понимаю, то, что Мейер сказал « quote
- eval
кажется достаточно безопасным», означает, что quote
- eval
может не тривиализировать эквациональную теорию, хотя он и не представил доказательств.
РЕДАКТИРОВАТЬ:
По предложению Мартина, поскольку все три упомянутые статьи касаются языков семейства LISP, давайте поставим вопрос под эту же настройку. Является ли контекстуальная эквивалентность языка с quote
- eval
в частности LISP, на земле тривиальной или нет?
[1] Митчелл Жезл, Теория Fexprs тривиальна . Лисп и Символьные вычисления 10 (3): 189-199 (1998).
[2] Альберт Мейер, семинар « Пазлы в программировании и логике» по разработке формального программного обеспечения. 1984
[3] Джон Маккарти, Рекурсивные функции символических выражений и их вычисление с помощью машины, часть I . Связь АСМ в апреле 1960 года.
Ответы:
Во-первых, это полностью зависит от того, что вы считаете своим набором контекстов. Если
(quote [])
есть контекст, то контекстуальная эквивалентность является синтаксической эквивалентностью.Традиционно контексты для контекстуальной эквивалентности считаются контекстами, в которых могут появляться «выражения» в любом значении, которое имеет в языке. Это исключает контексты, например
"[]"
, где контекст помещает свой аргумент в строковый литерал. Подобные контексты были, IIRC, исключены Куайном, когда он первоначально описал ссылочную прозрачность.С этой точки зрения, я думаю,
(quote [])
, также не является контекстом. Вместо этого контексты - это места, где потенциально может произойти оценка выражения, например, в теле функции или в аргументе приложения.Потенциально проблематично, это означает, что в программе на Лиспе с макросами (или в программе Racket или Scheme) вы не знаете, что такое контексты, пока не запустите потенциально не определяемый процесс расширения макроса, потому что вы даже не знаете, где выражения находятся. Считаете ли вы, что это проблема или нет, это в основном философский вопрос, а не технический.
источник
(quote [])
, а не выдавать желаемое за действительное, как контекст: отвергая идею лечения ,'datum
как синтаксический сахар для(quote datum)
, тогда'[]
как"[]"
больше не является контекстом. Схемы макросовquote
все равно затенились .'datum
и что-то(quote datum)
меняют?quote
это языковая конструкция и'datum
десугары(quote datum)
, люди, скорее всего, будут утверждать, что(quote [])
это контекст. Если убратьquote
из базового языка, но поддерживают буквальный'datum
синтаксис, то они будут менее склонны рассуждать так , потому что подобное"[]"
будет хорошо известно , что не является контекстом."[]"
контексте, но не в(quote [])
контексте. То, что могут спорить «люди», не здесь и не там.quote
из абстрактного синтаксиса, но поддержав (конкретный) буквальный синтаксис (незначительный пробел) цитаты. Из того, что я вижу, оба пути ведут к «Нет» на исходный вопрос.