В чем разница между стратегиями сокращения и оценочными стратегиями?

Из статьи по стратегии оценки в Википедии:

Понятие стратегии сокращения в лямбда-исчислении сходно, но различно.

Из статьи о стратегии сокращения в Википедии:

Это похоже на понятие стратегии оценки в информатике, но немного отличается от него.

Какое тонкое различие между стратегиями оценки и стратегиями сокращения, на которые намекают эти две статьи? Это просто две одинаковые концепции из разных областей?

Стратегия сокращения - это функция в Lambda, которая выбирает одно переопределение (приводимое выражение) из всех возможных переопределений - в зависимости от того, что вы определяете как переопределение.

Неформально стратегия оценки - это порядок, в котором язык оценивает свои аргументы. Стратегия передачи параметров - это то, что язык передает функции.

Чтобы понять связь между ними, изучите статью Плоткина «Звонок по имени», «Звонок по значению» и лямбда-исчисление. Он четко объясняет, что вы хотите выбрать разные АКСИОМЫ в зависимости от того, какой порядок оценки вы хотите. Для Cb-name вам нужна старая бета-аксиома, а для cb-value - аксиома бета-значения. Если вы сделаете это, все мета-теоремы сработают одинаково для обоих вариантов. Позже я показал (со многими сотрудниками), что эта идея обобщает все, что изучал мир ЛП.

Это все техническое, а не какое-то стихотворение, которое можно интерпретировать. Просто прочитайте об этом.

- Матиас Феллайзен

PS Я скажу, что я думаю, что людям будет легче понять статью Плоткина из первой части нашей книги Redex. Но да, это в 3 раза длиннее.

Статья в википедии «Стратегия сокращения» целиком извлечена из конкретного редактирования, сделанного анонимным IP в статье «Стратегия оценки».

Представление, которое оно представляет, не является консенсусным, в том смысле, что я подозреваю, что относительно немногие люди на местах спонтанно дадут этот ответ, если вы спросите их: «Различите ли вы названия« стратегия сокращения »и« стратегия оценки »?». Я слышал это только от Матиаса Феллайзена, который непреклонен в отношении важности этого различия, и я полагаю, что эту точку зрения разделяют другие, у которых была возможность уделить время для подробного обсуждения этих вопросов с ним.

Мое текущее понимание этого вопроса (но я еще не изучил технические детали в полной мере) о следующем: речь идет о том, используете ли вы семантику «большой шаг» против «малого шага» - это различие стандартно и понятно всеми в поле. Семантика малых шагов определяет один атомарный шаг редукции, и результат в целом все еще сводим. Семантика большого шага определяет один «большой» шаг сокращения, который проходит весь путь от начальной программы до ее значения (или некоторого более богатого типа «ответа», если у вашего языка есть другие наблюдаемые эффекты, чем возвращение значения, например, ввод / вывод или изменчивое состояние).

Если вы определяете отношение большого шага и малого шага, вы можете проверить, что семантика большого шага включена в транзитивное замыкание отношения малого шага, и что отношение малого шага не сводится к другим застрявшим терминам, чем те, которые достигаются отношением большого шага, или расходятся, если определено уменьшение большого шага. Это ожидаемая связь между обоими.

Я думаю, что формулировка статьи может быть более или менее описана в современных терминах как «стратегия оценки - это отношение большого шага», «стратегия сокращения - это отношение малого шага». Обратите внимание, что обсуждение в статье «Стратегия сокращения» в основном касается статей и исследований (и, что более важно, красноречивых точек зрения, сформированных во время их чтения и письма) в период с 1973 по 1991 год, в то время, когда эти понятия только родились, и вероятно, не так хорошо, как они понимают сегодня. (семантика большого шага была подчеркнута Каном в 1987 году, и одна из наиболее важных работ по семантике малого шага - Райт и Феллайзен, 1992)

Для более самоуверенной стороны того, почему Фелляйзен настаивает на важности этого различия (то есть, почему это может быть чем-то большим, чем просто «маленький шаг против большого шага, ме»), мое текущее понимание следующее: Смысл в том, что семантика малого шага должна рассматриваться как деталь реализации. семантика, согласно этому аргументу, является абстрактной функцией, которая отображает каждую программу в ее значение / ответ, а остальные являются устройствами реализации, предназначенными для ее аппроксимации (или обоснования эквивалентности, вызванной этой семантикой). Когда мы сегодня говорим «большой шаг», мы думаем о системе правил вывода синтаксической природы, но обсуждаемая выше «стратегия сокращения» на самом деле является ее абстракцией как отображением. (Я не думаю, что это дает больше выразительности или силы понятию на практике, но делает его более абстрактным.)

Поэтому я думаю, что то, что говорится на этой странице википедии и Матиасе Феллайзене, выглядит примерно так: «Определите свою оценку так, как вам нравится, но в конечном итоге важно то, как ваши программы отображаются в соответствии с их значениями / ответы / поведение, и это то, что следует называть «операционной семантикой» и обосновывать ».

Обратите внимание, что эта позиция идет вразрез с нынешним различием (которое я считаю довольно согласованным, но это может быть культурный уклон с моей стороны) между «операционной семантикой» и «денотационной семантикой», где первая считается более синтаксической по своей природе (определяется как отношение редукции), и последний типично характеризуется тем фактом, что вычислительно эквивалентные программы имеют точно такое же обозначение (поэтому обозначение не учитывает фактический механизм вычислений). Согласно этому последнему мнению, то, что предлагается в качестве «стратегии оценки» или «операционной семантики» в статьях и в моем объяснении выше, скорее будет рассматриваться как денотационная семантика, но, по общему признанию, более конкретной природы, чем большинство: ценности / ответы / поведения ближе к синтаксическим объектам, чем многие семантические области.

Ссылки: чтобы понять эту точку зрения, вероятно, было бы полезно вернуться к ее провозглашенному источнику, который является статьей Гордона Плоткина в 1973 году. Возможно, вам также повезет, попробовав одну из последних статей, цитируемых в Википедии; Например, я обнаружил, что «Передача параметров и лямбда-исчисление» Крэнка и Феллайзена, 1991 год, на первых нескольких страницах очень четко обозначили их позицию по данному вопросу.