Является ли контекстуальная эквивалентность языка с `quote`-`eval` тривиальной или нет?

13

В [1] Митчелл Ванд продемонстрировал, что добавление fexprs к чистому лямбда-исчислению упрощает теорию контекстуальной эквивалентности, означая, что два термина контекстуально эквивалентны, если они -конгруэнтны. При изучении соответствующей работы, он пошел «наш результат расширяет старое наблюдение Альберт Мейер [2] , что и визуализации контекстная эквивалентности тривиальным». Но, ссылаясь на [2], можно найти только следующее утверждение Мейера:αevalquote

Я первая подумала , что в языках с 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 года.

день
источник
1
Я бы посоветовал подумать, не могли бы вы сделать вопрос более конкретным: существуют разные способы реализации eval / quote-подобных конструкций, а также различные варианты создания контекстных эквивалентностей для таких исчислений. Интересная недавняя публикация - « Рассуждение о многоступенчатых программах » Иноуэ, Таха.
Мартин Бергер
1
Ключевое различие между CTMP (метапрограммирование времени компиляции, примером которого является Template Haskell, Lisp / Scheme / Racket и Converge , и RTMP (метапрограммирование времени выполнения, такое как eval Javascript или MetaOCaml). Другим параметром является типизация . Вот краткий обзор разговора я дал несколько месяцев назад на эту тему, совсем неглубоко , боюсь Что касается контекстные эквивалентностей, мало работы было сделано, в основном , владеющим в жидком состоянии программирования поддержку мета-программирования..
Мартин Бергер
1
@ plmday: Кстати, идеализированный язык программирования, который Wand формализует в The Feexprs The Trivial , весьма отличается от метапрограммирования Lisp. Первый - RTMP, последний (в зависимости от конкретных реализаций) - нет.
Мартин Бергер
1
@MartinBerger: Вы можете опубликовать свой доклад в формате PDF?
Дейв Кларк,
1
@ Дейв Кларк, конечно, вот оно! Обратная связь приветствуется.
Мартин Бергер

Ответы:

2

Во-первых, это полностью зависит от того, что вы считаете своим набором контекстов. Если (quote [])есть контекст, то контекстуальная эквивалентность является синтаксической эквивалентностью.

Традиционно контексты для контекстуальной эквивалентности считаются контекстами, в которых могут появляться «выражения» в любом значении, которое имеет в языке. Это исключает контексты, например "[]", где контекст помещает свой аргумент в строковый литерал. Подобные контексты были, IIRC, исключены Куайном, когда он первоначально описал ссылочную прозрачность.

С этой точки зрения, я думаю, (quote []) , также не является контекстом. Вместо этого контексты - это места, где потенциально может произойти оценка выражения, например, в теле функции или в аргументе приложения.

Потенциально проблематично, это означает, что в программе на Лиспе с макросами (или в программе Racket или Scheme) вы не знаете, что такое контексты, пока не запустите потенциально не определяемый процесс расширения макроса, потому что вы даже не знаете, где выражения находятся. Считаете ли вы, что это проблема или нет, это в основном философский вопрос, а не технический.

Сэм Тобин-Хохштадт
источник
Я не думаю , есть один способ , чтобы исключить (quote []), а не выдавать желаемое за действительное, как контекст: отвергая идею лечения , 'datumкак синтаксический сахар для (quote datum), тогда '[]как "[]"больше не является контекстом. Схемы макросов quoteвсе равно затенились .
день
Я не понимаю ваш комментарий, @day. Почему отношения 'datumи что-то (quote datum)меняют?
Сэм Тобин-Хохштадт
Если quoteэто языковая конструкция и 'datumдесугары (quote datum), люди, скорее всего, будут утверждать, что (quote [])это контекст. Если убрать quoteиз базового языка, но поддерживают буквальный 'datumсинтаксис, то они будут менее склонны рассуждать так , потому что подобное "[]"будет хорошо известно , что не является контекстом.
день
@день, это недоразумение. Там нет единого правильного определения «контекста». Просто разные контексты поддерживают разные понятия контекстуальной эквивалентности. Например, пробелы семантически значимы в "[]"контексте, но не в (quote [])контексте. То, что могут спорить «люди», не здесь и не там.
Сэм Тобин-Хохштадт
Я согласен, что не существует единого правильного определения контекста. Но есть одно традиционное определение, основанное на абстрактном синтаксисе, которое Ванд использует в своей статье, а Мейер использует в своей статье, чтобы поставить под сомнение статус контекстуальной эквивалентности Лисп. Вы предложили заменить традиционное определение контекста оценочным контекстом. Я предложил сохранить традиционное определение контекста, исключив quoteиз абстрактного синтаксиса, но поддержав (конкретный) буквальный синтаксис (незначительный пробел) цитаты. Из того, что я вижу, оба пути ведут к «Нет» на исходный вопрос.
день