Что такое бета-эквивалентность?

В сценарии, который я сейчас читаю по лямбда-исчислению, бета-эквивалентность определяется следующим образом:

-эквивалентность является наименьшей эквивалентности , который содержит . $\beta$ $\equiv_\beta$ $\rightarrow_\beta$

Я понятия не имею, что это значит. Может кто-нибудь объяснить это более простыми словами? Может быть с примером?

Мне это нужно для леммы, вытекающей из теоремы Черча-Рассера:

Если M N, то есть L с M L и N L. $\equiv_\beta$ $\twoheadrightarrow_\beta$ $\twoheadrightarrow_\beta$

logic terminology lambda-calculus type-theory magnattic
источник

Извините, если язык не идеален, я перевёл цитаты с немецкого.

Magnattic

Ответы:

$\to_\beta$ - это одношаговое отношение между членами в $\lambda$ калькуляторе. Это отношение не является ни рефлексивным, ни симметричным, ни транзитивным. Отношение эквивалентности $\equiv_\beta$ является рефлексивным, симметричным, транзитивным замыканием $\to_\beta$ . Это означает

Если $M\to_\beta M'$ то $M\equiv_\beta M'$ .
Для всех терминов $M$ , $M\equiv_\beta M$ имеет.
Если $M\equiv_\beta M'$ 'то $M'\equiv_\beta M$ .
Если $M\equiv_\beta M'$ и $M'\equiv_\beta M''$ , то $M\equiv_\beta M''$ .
$\equiv_\beta$ - наименьшее отношение, удовлетворяющее условиям 1-4.

Более конструктивно: сначала примените правила 1 и 2, затем повторяйте правила $3$ и $4$ снова и снова, пока они не добавят новые элементы в отношение.

Дэйв Кларк
источник

Хорошо, спасибо, я думаю, что понял. Мое первое предположение состояло в том, что означает, что M можно каким-то образом уменьшить до N, но это не обязательно должно выполняться, поскольку они, очевидно, также эквивалентны, если их можно привести к одному и тому же члену. Думаю, из-за вашей точки 3 это можно построить. Спасибо, это очень помогло.

M \equiv_{β} N

$M \equiv_\beta N$

Magnattic

Не является ли отношение бесконечно большим? Разве я не всегда могу найти термин L для термина M, чтобы ?

L \to_{β} M

$L \rightarrow_\beta M$

Magnattic

Это так, но это не должно быть проблематичным. Почему вы ищете такой ?

L

$L$

Дейв Кларк

Я не знаю. Я просто спорил со своим партнером, если он всегда будет бесконечно большим. Спасибо за объяснение. :)

Magnattic

Это действительно элементарная теория множеств. Вы знаете, что такое рефлексивное отношение, что такое симметричное отношение и что такое транзитивное отношение, верно? Отношение эквивалентности - это такое, которое удовлетворяет всем трем из этих свойств.

Вы, наверное, слышали о «транзитивном замыкании» отношения ? Ну, это не что иное, как минимум транзитивное отношение , которое включает . Вот что означает термин «закрытие». Точно так же вы можете говорить о «симметричном замыкании» отношения , «рефлексивном замыкании» отношения и «замыкании эквивалентности» отношения точно таким же образом. $R$ $R$ $R$ $R$ $R$

Подумав немного, вы можете убедить себя, что транзитивное замыкание есть . Симметричное замыкание есть . Рефлексивным замыканием является (где - отношение идентичности). $R$ $R \cup R^2 \cup R^3 \cup \ldots$ $R \cup R^{-1}$ $R \cup I$ $I$

Мы используем обозначение для . Это рефлексивное транзитивное замыкание в . Теперь заметим, что если симметричен, то каждое из соотношений , , , , ... симметрично. Следовательно, также будет симметричным. $R^*$ $I \cup R \cup R^2 \cup \ldots$ $R$ $R$ $I$ $R$ $R^2$ $R^3$ $R^*$

Таким образом, замыкание эквивалентности является транзитивным замыканием его симметричного замыкания, т. Е. . Это представляет последовательность шагов, некоторые из которых являются шагами вперед ( ) и шагами назад ( ). $R$ $(R \cup R^{-1})^*$ $R$ $R^{-1}$

Говорят, что отношение обладает свойством Черча-Россера, если замыкание эквивалентности совпадает с составным отношением . Это представляет собой последовательность шагов, в которой все шаги вперед идут первыми, а затем все шаги назад. Таким образом, свойство Черча-Россера говорит, что любое чередование шагов вперед и назад можно эквивалентно выполнить, выполнив шаги вперед вперед и шаги назад позже. $R$ $R^* (R^{-1})^*$

Удай Редди
источник

Если вы добавите одно последнее предложение, относящееся к вопросу, это будет хорошим ответом.

Рафаэль

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

Марко Фаустинелли