O que é equivalência beta?

No script que estou lendo atualmente no cálculo lambda, a equivalência beta é definida como esta:

O $\beta$ -equivalence $\equiv_\beta$ é o menor equivalência que contém $\rightarrow_\beta$ .

Eu não tenho idéia o que isso significa. Alguém pode explicar isso em termos mais simples? Talvez com um exemplo?

Preciso dele para um lema que segue o teorema de Church-Russer, dizendo

$\equiv_\beta$ $\twoheadrightarrow_\beta$ $\twoheadrightarrow_\beta$

logic terminology lambda-calculus type-theory magnattic
fonte

Desculpe se o idioma não é perfeito, traduzi as aspas do alemão.

magnattic

Respostas:

$\to_\beta$ é a relação de uma etapa entre os termos no -calculus. Essa relação não é reflexiva, simétrica ou transitiva. A relação de equivalência é o fechamento reflexivo, simétrico e transitivo de . Isso significa $\lambda$ $\equiv_\beta$ $\to_\beta$

Se então . $M\to_\beta M'$ $M\equiv_\beta M'$
Para todos os termos , é válido. $M$ $M\equiv_\beta M$
Se'em seguida, . $M\equiv_\beta M'$ $M'\equiv_\beta M$
Se e , então . $M\equiv_\beta M'$ $M'\equiv_\beta M''$ $M\equiv_\beta M''$
$\equiv_\beta$ é a menor relação que satisfaz as condições 1-4.

Mais construtivamente, primeiro aplique as regras 1 e 2, depois repita as regras e repetidamente até que não adicionem novos elementos à relação. $3$ $4$

Dave Clarke
fonte

Ok obrigado, acho que entendi. Minha primeira suposição foi que significa que M pode, de alguma forma, ser reduzido a N, mas isso não precisa necessariamente ser válido, porque eles obviamente também são equivalentes se puderem ser reduzidos ao mesmo termo. Por causa do seu ponto 3, isso pode ser construído então, eu acho. Obrigado, isso ajudou muito.

M \equiv_{β} N

$M \equiv_\beta N$

magnattic

A relação não é infinitamente grande? Nem sempre consigo encontrar um Termo L para um Termo M, de modo que ?

L \to_{β} M

$L \rightarrow_\beta M$

magnattic

É, mas isso não deve ser problemático. Por que você está procurando um ?

L

$L$

Dave Clarke

Eu não sei. Eu estava apenas discutindo com meu parceiro se sempre seria infinitamente grande. Obrigado por explicar. :)

magnattic

É realmente a teoria dos conjuntos elementares. Você sabe o que é uma relação reflexiva, o que é uma relação simétrica e o que é uma relação transitiva, certo? Uma relação de equivalência é aquela que satisfaz todas as três dessas propriedades.

Você provavelmente já ouviu falar do "fechamento transitivo" de uma relação ? Bem, não é nada, mas a relação menos transitivo que inclui . É isso que significa o termo "encerramento". Da mesma forma, você pode falar sobre o "fechamento simétrico" de uma relação , o "fechamento reflexivo" de uma relação e o "fechamento de equivalência" de uma relação exatamente da mesma maneira. $R$ $R$ $R$ $R$ $R$

Com alguma reflexão, você pode se convencer de que o fechamento transitivo de é . O fechamento simétrico é . O fechamento reflexivo é (onde é a relação de identidade). $R$ $R \cup R^2 \cup R^3 \cup \ldots$ $R \cup R^{-1}$ $R \cup I$ $I$

Usamos a notação para . Este é o fechamento transitivo reflexiva de . Agora observe que se é simétrico, cada uma das relações , , , , ... é simétrica. Portanto, também será simétrico. $R^*$ $I \cup R \cup R^2 \cup \ldots$ $R$ $R$ $I$ $R$ $R^2$ $R^3$ $R^*$

Portanto, o fechamento de equivalência de é o fechamento transitivo de seu fechamento simétrico, ou seja, . Isso representa uma sequência de etapas, algumas das quais são etapas avançadas ( ) e algumas etapas anteriores ( ). $R$ $(R \cup R^{-1})^*$ $R$ $R^{-1}$

Diz-se que a relação possui a propriedade Church-Rosser se o fechamento da equivalência for o mesmo que a relação composta . Isso representa uma sequência de etapas nas quais todas as etapas avançadas vêm primeiro, seguidas por todas as etapas anteriores. Portanto, a propriedade Church-Rosser diz que qualquer intercalação de etapas para a frente e para trás pode ser realizada de maneira equivalente executando-se as etapas para a frente primeiro e para trás depois. $R$ $R^* (R^{-1})^*$

Uday Reddy
fonte

Se você adicionou uma frase final para se relacionar com a pergunta, essa seria uma boa resposta.

Raphael

É tudo tão elementar que chega ao fim e se pergunta "onde está a resposta, na verdade?"

Marco Faustinelli