Стратегия сокращения

В переписывании стратегия сокращения или стратегия переписывания — это отношение, определяющее перезапись для каждого объекта или термина, совместимое с данным отношением сокращения. Некоторые авторы используют этот термин для обозначения стратегии оценки .

Определения

Формально для абстрактной системы переписывания $(A,\to )$, стратегия сокращения $\to _{S}$ является бинарным отношением на $A$ с $\to _{S}\subseteq {\overset {+}{\to }}$ , где ${\overset {+}{\to }}$ является транзитивным замыканием $\to$ (но не рефлексивное закрытие). Кроме того, нормальные формы стратегии должны быть такими же, как нормальные формы исходной системы переписывания, т. е. для всех $a$, существует $b$ с $a\to b$ если только $\exists b'.a\to _{S}b'$.

Стратегия одношагового сокращения – это стратегия, при которой $\to _{S}\subseteq \to$. В противном случае это многошаговая стратегия.

стратегия Детерминированная – это стратегия, в которой $\to _{S}$ является частичной функцией , т.е. для каждого $a\in A$ есть максимум один $b$ такой, что $a\to _{S}b$. В противном случае это недетерминированная стратегия.

Переписывание термина

В системе переписывания терминов стратегия переписывания определяет из всех сокращаемых подтерминов ( редексов ), какой из них следует сократить ( сжать ) в пределах термина.

Одноэтапные стратегии переписывания терминов включают в себя:

• Самый левый-внутренний: на каждом шаге сжимается самый левый из самых внутренних редексов, причем самым внутренним редексом является редекс, не содержащий каких-либо редексов.
• Крайний левый-внешний: на каждом шаге сжимается самый левый из крайних редексов, где крайний редекс — это редекс, не содержащийся ни в одном редексе
• Крайний правый внутренний, Крайний правый крайний: аналогично

Многошаговые стратегии включают в себя:

• параллельный-внутренний: одновременно сокращает все самые внутренние редексы. Это четко определено, поскольку редексы попарно не пересекаются.
• параллельно-внешний: аналогично
• Редукция Гросса-Кнута, также называется полной заменой или редукцией Клини: все редексы в терме одновременно сокращаются

Параллельная внешняя редукция и редукция Гросса-Кнута гипернормализуют для всех почти ортогональных систем переписывания терминов, а это означает, что эти стратегии в конечном итоге достигнут нормальной формы, если она существует, даже при выполнении (конечного множества) произвольных редукций между последовательными применениями стратегии.

Stratego — это предметно-ориентированный язык, разработанный специально для стратегий переписывания терминов программирования.

Лямбда-исчисление

См. Также: Лямбда-исчисление § Стратегии сокращения

В контексте исчисления лямбда - сокращение нормального порядка относится к крайнему левому сокращению в смысле, указанном выше . Приведение к нормальному порядку является нормализацией в том смысле, что если терм имеет нормальную форму, то приведение к нормальному порядку в конечном итоге достигнет ее, отсюда и название «нормальный». Это известно как теорема стандартизации.

Крайнее левое сокращение иногда используется для обозначения нормального уменьшения порядка, поскольку при обходе предварительного порядка понятия совпадают, и аналогичным образом крайний левый редекс - это редекс с самым левым начальным символом, когда лямбда-термин рассматривается как строка символов. Когда «крайний левый» определяется с помощью обхода по порядку, понятия различны. Например, в термине $(\lambda x.x\Omega )(\lambda y.I)$ с $\Omega ,I$ определено здесь , самый левый редекс упорядоченного обхода равен $\Omega$ в то время как крайний левый редекс представляет собой все выражение.

Аппликативное снижение порядка относится к самому левому и самому внутреннему сокращению. В отличие от нормального порядка редукция аппликативного порядка может не прекращаться, даже если термин имеет нормальную форму. Например, с помощью аппликативного приведения порядка возможна следующая последовательность приведений:

$${\begin{aligned}&(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\&\ldots \end{aligned}}$$

Но при использовании приведения к нормальному порядку та же самая отправная точка быстро приводится к нормальной форме:

$$(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))$$

$$\rightarrow z$$

Полная β-редукция относится к недетерминированной одношаговой стратегии, которая позволяет уменьшать любой редекс на каждом этапе. Такахаши Параллельная β-редукция — это стратегия, которая уменьшает все редексы в термине одновременно.

Слабое сокращение

Нормальное и аппликативное приведение порядка сильны тем, что позволяют приводить к лямбда-абстракциям. Напротив, слабая редукция не приводит к лямбда-абстракции. Сокращение вызова по имени — это слабая стратегия сокращения, которая уменьшает самый левый внешний редекс не внутри лямбда-абстракции, тогда как сокращение вызова по значению — это слабая стратегия сокращения, которая уменьшает самый левый внутренний редекс не внутри лямбда-абстракции. вызова по имени и вызова по значению Эти стратегии были разработаны для отражения стратегий оценки . Фактически, аппликативное понижение порядка также было первоначально введено для моделирования метода передачи параметров по значению, используемого в Algol 60 и современных языках программирования. В сочетании с идеей слабой редукции результирующая редукция вызова по значению действительно является точным приближением.

К сожалению, слабая редукция не является сливной. а традиционные уравнения приведения лямбда-исчисления бесполезны, поскольку они предполагают отношения, нарушающие режим слабой оценки. Однако можно расширить систему до конфлюэнтности, разрешив ограниченную форму редукции в рамках абстракции, в частности, когда редекс не включает переменную, связанную абстракцией. Например, λ x .(λ y . x ) z находится в нормальной форме для стратегии слабой редукции, поскольку редекс (λ y . x ) z содержится в лямбда-абстракции. Но термин λ x .(λ y . y ) z все еще можно уменьшить с помощью расширенной стратегии слабой редукции, поскольку редекс (λ y . y ) z не относится к х .

Оптимальное сокращение

Оптимальное сокращение мотивировано существованием лямбда-членов там, где не существует последовательности сокращений, которая уменьшает их без дублирования работы. Например, рассмотрим

((λg.(g(g(λx.x))))
 (λh.((λf.(f(f(λz.z))))
      (λw.(h(w(λy.y)))))))

Он состоит из трех вложенных терминов, x=((λg. ... ) (λh.y)) , y=((λf. ...) (λw.z)) , и z=λw.(h(w(λy.y))) . Здесь можно сделать только две возможные β-редукции: по x и по y. Уменьшение внешнего термина x сначала приводит к дублированию внутреннего термина y, и каждая копия должна быть уменьшена, но уменьшение сначала внутреннего термина y приведет к дублированию его аргумента z, что приведет к дублированию работы, когда значения h и мы стали известны.

Оптимальное сокращение не является стратегией сокращения для лямбда-исчисления в узком смысле, поскольку при выполнении β-редукции теряется информация об общих замененных редексах. Вместо этого он определен для помеченного лямбда-исчисления , аннотированного лямбда-исчисления, которое отражает точное представление о работе, которой следует поделиться.

Метки состоят из счетного бесконечного набора атомарных меток и конкатенаций. $ab$, зачеркивания ${\overline {a}}$ и подчеркивания ${\underline {a}}$ этикеток. Помеченный термин — это термин лямбда-исчисления, в котором каждый подтерм имеет метку. Стандартная начальная маркировка лямбда-терма дает каждому подтерму уникальную атомарную метку. Меченое β-восстановление определяется:

$$((\lambda x.M)^{\alpha }N)^{\beta }\to \beta {\overline {\alpha }}\cdot M[x\mapsto {\underline {\alpha }}\cdot N]$$

где $\cdot$ объединяет метки, $\beta \cdot T^{\alpha }=T^{\beta \alpha }$и замена $M[x\mapsto N]$ определяется следующим образом (с использованием соглашения Барендрегта ):

$${\begin{aligned}x^{\alpha }[x\mapsto N]&=\alpha \cdot N&\quad (\lambda y.M)^{\alpha }[x\mapsto N]&=(\lambda y.M[x\mapsto N])^{\alpha }\\y^{\alpha }[x\mapsto N]&=y^{\alpha }&\quad (MN)^{\alpha }[x\mapsto P]&=(M[x\mapsto P]N[x\mapsto P])^{\alpha }\end{aligned}}$$

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

Практический алгоритм оптимального сокращения был впервые описан в 1989 году. спустя более десяти лет после того, как оптимальное сокращение было впервые определено в 1974 году. Болонская оптимальная машина высшего порядка (BOHM) — это прототип реализации расширения метода на сети взаимодействия . Lambdascope — это более поздняя реализация оптимального сокращения, также использующая сети взаимодействия.

Звонок по сокращению потребности

Сокращение вызова по необходимости можно определить аналогично оптимальному сокращению как слабое крайнее левое сокращение с использованием параллельного сокращения редексов с одной и той же меткой для немного другого помеченного лямбда-исчисления. Альтернативное определение заменяет бета-правило на операцию, которая находит следующее «необходимое» вычисление, оценивает его и заменяет результат во все места. Это требует расширения бета-правила, чтобы позволить сокращать термины, которые не являются синтаксически смежными. Как и в случае с вызовом по имени и вызовом по значению, сокращение количества вызовов по необходимости было разработано для имитации поведения стратегии оценки, известной как «вызов по необходимости» или ленивая оценка .

См. также

• Система сокращения
• Семантика сокращения
• Thunk

Внешние ссылки

• Рабочая среда сокращения лямбда-исчисления