Índice De Bruijn - De Bruijn index

Na lógica matemática , o índice De Bruijn é uma ferramenta inventada pelo matemático holandês Nicolaas Govert de Bruijn para representar termos do cálculo lambda sem nomear as variáveis ​​ligadas. Os termos escritos usando esses índices são invariantes em relação à conversão α , então a verificação para equivalência α é a mesma que para a igualdade sintática. Cada índice De Bruijn é um número natural que representa uma ocorrência de uma variável em um termo λ e denota o número de fichários que estão no escopo entre essa ocorrência e seu fichário correspondente. A seguir estão alguns exemplos:

• O termo λ x . λ y . x , às vezes chamado de combinador K , é escrito como λ λ 2 com índices de De Bruijn. O fichário para a ocorrência x é o segundo λ no escopo.
• O termo λ x . λ y . λ z . x z ( y z ) (o combinador S ), com índices de De Bruijn, é λ λ λ 3 1 (2 1).
• O termo λ z . (λ y . y (λ x . x )) (λ x . z x ) é λ (λ 1 (λ 1)) (λ 2 1). Veja a ilustração a seguir, onde os fichários são coloridos e as referências são mostradas com setas.

Os índices de De Bruijn são comumente usados ​​em sistemas de raciocínio de ordem superior , como provadores de teoremas automatizados e sistemas de programação lógica .

Definição formal

Formalmente, os termos λ ( M , N , ...) escritos usando índices De Bruijn têm a seguinte sintaxe (parênteses são permitidos livremente):

M , N , ... :: = n | M N | λ M

onde n - números naturais maiores que 0 - são as variáveis. Uma variável n é limitada se estiver no escopo de pelo menos n ligantes (λ); caso contrário, é grátis . O local de ligação para uma variável N é o n th ligante é no âmbito de, a partir do ligante mais interna.

A operação mais primitiva em termos λ é a substituição: substituir variáveis ​​livres em um termo por outros termos. Na redução β (λ M ) N , por exemplo, devemos

1. encontre as instâncias das variáveis n ₁ , n ₂ , ..., n _k em M que são limitadas pelo λ em λ M ,
2. decrementar as variáveis ​​livres de M para coincidir com a remoção do ligante λ externo, e
3. substitua n ₁ , n ₂ , ..., n _k por N , incrementando adequadamente as variáveis ​​livres que ocorrem em N cada vez, para corresponder ao número de ligantes λ, sob os quais a variável correspondente ocorre quando N substitui um dos n _eu .

Para ilustrar, considere a aplicação

(λ λ 4 2 (λ 1 3)) (λ 5 1)

que pode corresponder ao seguinte termo escrito na notação usual

(λ x . λ y . z x (λ u . u x )) (λ x . w x ).

Após o passo 1, obtém-se o termo λ 4 □ (λ 1 □), onde as variáveis ​​destinadas à substituição são substituídas por caixas. O passo 2 diminui as variáveis ​​livres, dando λ 3 □ (λ 1 □). Finalmente, no passo 3, substituímos as caixas pelo argumento, a saber λ 5 1; a primeira caixa está sob um fichário, então a substituímos por λ 6 1 (que é λ 5 1 com as variáveis ​​livres aumentadas em 1); o segundo está sob dois ligantes, então o substituímos por λ 7 1. O resultado final é λ 3 (λ 6 1) (λ 1 (λ 7 1)).

Formalmente, uma substituição é uma lista ilimitada de substituições de termos para as variáveis ​​livres, escrita M ₁ . M ₂ ..., onde M _i é a substituição da i ésima variável livre. A operação de aumento na etapa 3 às vezes é chamada de deslocamento e escrita ↑ ^k onde k é um número natural que indica a quantidade de aumento das variáveis; por exemplo, ↑ ⁰ é a substituição de identidade, deixando um termo inalterado.

A aplicação de uma substituição s a um termo M é escrita M [ s ]. A composição de duas substituições s ₁ e s ₂ é escrita s ₁ s ₂ e definida por

M [ s ₁ s ₂ ] = ( M [ s ₁ ]) [ s ₂ ].

As regras de aplicação são as seguintes:

${\ displaystyle {\ begin {alinhados} n [N_ {1} \ ldots N_ {n} \ ldots] = & N_ {n} \\ (M_ {1} \; M_ {2}) [s] = & (M_ {1} [s]) (M_ {2} [s]) \\ (\ lambda \; M) [s] = & \ lambda \; (M [1,1 [s ']. 2 [s']. 3 [s '] \ ldots]) \\ & {\ text {onde}} s' = s \ uparrow ^ {1} \ end {alinhado}}}$

As etapas descritas para a redução β acima são, portanto, expressas de forma mais concisa como:

(λ M ) N → _β M [ N .1.2.3 ...].

Alternativas aos índices De Bruijn

Ao usar a representação "nomeada" padrão de termos λ, onde as variáveis ​​são tratadas como rótulos ou strings, deve-se tratar explicitamente a conversão α ao definir qualquer operação nos termos. Na prática, isso é complicado, ineficiente e, muitas vezes, sujeito a erros. Portanto, levou à busca de diferentes representações de tais termos. Por outro lado, a representação nomeada de termos λ é mais difundida e pode ser mais imediatamente compreensível por outros porque as variáveis ​​podem receber nomes descritivos. Assim, mesmo que um sistema use índices De Bruijn internamente, ele apresentará uma interface de usuário com nomes.

Os índices de De Bruijn não são a única representação de termos λ que evita o problema da conversão α. Entre as representações nomeadas, as técnicas nominais de Pitts e Gabbay são uma abordagem, onde a representação de um termo λ é tratada como uma classe de equivalência de todos os termos regraváveis para ele usando permutações de variáveis. Essa abordagem é adotada pelo Nominal Datatype Package of Isabelle / HOL .

Outra alternativa comum é um apelo a representações de ordem superior onde o ligante λ é tratado como uma função verdadeira. Em tais representações, as questões de α-equivalência, substituição, etc. são identificadas com as mesmas operações em uma meta-lógica .

Ao raciocinar sobre as propriedades metateóricas de um sistema dedutivo em um assistente de prova , às vezes é desejável limitar-se a representações de primeira ordem e ter a capacidade de nomear ou renomear suposições. A abordagem localmente sem nome usa uma representação mista de variáveis ​​- índices de De Bruijn para variáveis ​​ligadas e nomes para variáveis ​​livres - que pode se beneficiar da forma α-canônica dos termos indexados de De Bruijn quando apropriado.

Convenção de variável de Barendregt

A convenção de variável de Barendregt é uma convenção comumente usada em provas e definições onde se assume que:

• as variáveis ​​associadas são distintas das variáveis ​​livres e
• todos os ligantes vinculam variáveis ​​que ainda não estão no escopo.

No contexto geral de uma definição indutiva, não é possível aplicar a conversão α conforme necessário para converter uma definição indutiva usando a convenção para uma onde a convenção não é usada, porque uma variável pode aparecer tanto em uma posição de ligação quanto em uma não -posição obrigatória na regra. O princípio de indução é válido se cada regra satisfizer as duas condições a seguir:

• a regra é equivariante no sentido da lógica nominal, ou seja, sua validade permanece inalterada com a renomeação de variáveis
• assumindo as premissas da regra, as variáveis ​​nas posições de ligação na regra são distintas e são livres na conclusão

Veja também

• A notação de De Bruijn para termos λ.
• Lógica combinatória , uma forma mais essencial de eliminar nomes de variáveis.

Referências