Estratégia de redução - Reduction strategy

Na reescrita , uma estratégia de redução ou estratégia de reescrita é uma relação que especifica uma reescrita para cada objeto ou termo, compatível com uma dada relação de redução. Alguns autores usam o termo para se referir a uma estratégia de avaliação .

Definições

Formalmente, para um sistema de reescrita abstrato , uma estratégia de redução é uma relação binária on com , onde está o fechamento transitivo de (mas não o fechamento reflexivo). ${\ displaystyle (A, \ to)}$ ${\ displaystyle \ para _ {S}}$ ${\ displaystyle A}$ ${\ displaystyle \ to _ {S} \ subseteq {\ overset {+} {\ to}}}$ ${\ displaystyle {\ overset {+} {\ to}}}$ ${\ displaystyle \ to}$

Uma estratégia de redução de uma etapa é aquela em que . Caso contrário, é uma estratégia de muitas etapas . ${\ displaystyle \ to _ {S} \ subseteq \ to}$

Uma estratégia determinística é aquela em que existe uma função parcial , ou seja, para cada uma existe no máximo uma tal que . Caso contrário, é uma estratégia não determinística . ${\ displaystyle \ para _ {S}}$ ${\ displaystyle a \ in A}$ ${\ displaystyle b}$ ${\ displaystyle a \ to _ {S} b}$

Reescrita de mandato

Em um sistema de termo reescrever uma reescrita especifica de estratégia, de todas as subtermos redutíveis ( redexes ), que deve ser reduzido ( contratado ) dentro de um prazo.

As estratégias de uma etapa para a reescrita de termos incluem:

leftmost-innermost: em cada etapa, o redex mais à esquerda dos redexes mais internos é contraído, onde um redex mais interno é um redex que não contém nenhum redex
mais à esquerda-ultraperiféricas: em cada etapa, o mais à esquerda dos redexes mais externos é contraído, onde um redex mais externo é um redex não contido em nenhum redex
mais à direita-mais interno, mais à direita-mais externo: da mesma forma

As estratégias de muitas etapas incluem:

paralelo-interno: reduz todos os redexes internos simultaneamente. Isso é bem definido porque os redexes são disjuntos aos pares.
paralelo-externo: da mesma forma
Redução de Gross-Knuth, também chamada de substituição completa ou redução de Kleene: todos os redexes no termo são reduzidos simultaneamente

A redução paralela externa e de Gross-Knuth é hipernormalizante para todos os sistemas de reescrita de termos quase ortogonais, o que significa que essas estratégias acabarão por atingir uma forma normal se existir, mesmo ao realizar (finitamente muitas) reduções arbitrárias entre aplicações sucessivas da estratégia.

Stratego é uma linguagem de domínio específico projetada especificamente para estratégias de reescrita de termos de programação.

Cálculo lambda

No contexto do cálculo lambda , a redução de ordem normal refere-se à redução mais à esquerda no sentido dado acima . A redução mais à esquerda é às vezes usada para se referir à redução de ordem normal, pois com uma travessia de árvore de pré-ordem as noções coincidem, mas com a travessia de ordem mais típica as noções são distintas. Por exemplo, no termo com definido aqui , o redex textualmente mais à esquerda é enquanto o redex mais à esquerda é a expressão inteira. A redução de ordem normal é normalizadora, no sentido de que se um termo tem uma forma normal, então a redução de ordem normal acabará por alcançá-lo, daí o nome normal. Isso é conhecido como teorema de padronização. ${\ displaystyle (\ lambda xx \ Omega) (\ lambda yI)}$ ${\ displaystyle \ Omega, I}$ ${\ displaystyle \ Omega}$

A redução de pedido do aplicativo refere-se à redução mais à esquerda. Em contraste com o pedido normal, a redução do pedido de aplicativo não pode terminar, mesmo quando o termo tem uma forma normal. Por exemplo, usando a redução de pedido de aplicativo, a seguinte sequência de reduções é possível:

{\ displaystyle {\ begin {alinhados} & (\ mathbf {\ lambda} xz) ((\ lambda w.www) (\ lambda w.www)) \\\ rightarrow & (\ lambda xz) ((\ lambda w .www) (\ lambda w.www) (\ lambda w.www)) \\\ rightarrow & (\ lambda xz) ((\ lambda w.www) (\ lambda w.www) (\ lambda w.www) (\ lambda w.www)) \\\ rightarrow & (\ lambda xz) ((\ lambda w.www) (\ lambda w.www) (\ lambda w.www) (\ lambda w.www) (\ lambda w.www)) \\ & \ ldots \ end {alinhado}}}

Mas usando a redução de ordem normal, o mesmo ponto de partida é reduzido rapidamente para a forma normal:

{\ displaystyle (\ mathbf {\ lambda} xz) ((\ lambda w.www) (\ lambda w.www))}

{\ displaystyle \ rightarrow z}

A redução β total refere - se à estratégia não determinística de uma etapa que permite reduzir qualquer redex em cada etapa. A redução β paralela de Takahashi é a estratégia que reduz todos os redexes no termo simultaneamente.

Redução fraca

A redução de ordem normal e de aplicativo são fortes porque permitem a redução sob abstrações lambda. Em contraste, a redução fraca não reduz sob uma abstração lambda. A redução de chamada por nome é a estratégia de redução fraca que reduz o redex externo mais à esquerda fora de uma abstração lambda, enquanto a redução de chamada por valor é a estratégia de redução fraca que reduz o redex interno mais à esquerda não dentro de uma abstração lambda. Essas estratégias foram elaboradas para refletir as estratégias de avaliação chamada por nome e chamada por valor . Na verdade, a redução de pedido de aplicativo também foi originalmente introduzida para modelar a técnica de passagem de parâmetro chamada por valor encontrada no Algol 60 e em linguagens de programação modernas. Quando combinada com a ideia de redução fraca, a redução chamada por valor resultante é de fato uma aproximação fiel.

Infelizmente, a redução fraca não é confluente e as equações de redução tradicionais do cálculo lambda são inúteis, porque sugerem relações que violam o regime de avaliação fraca. No entanto, é possível estender o sistema para ser confluente, permitindo uma forma restrita de redução sob uma abstração, em particular quando o redex não envolve a variável limitada pela abstração. Por exemplo, λ x . (Λ y . X ) z está na forma normal para uma estratégia de redução fraca porque o redex (λ y . X ) z está contido em uma abstração lambda. Mas o termo λ x . (Λ y . Y ) z ainda pode ser reduzido sob a estratégia de redução fraca estendida, porque o redex (λ y . Y ) z não se refere a x .

Redução ótima

A redução ótima é motivada pela existência de termos lambda onde não existe uma sequência de reduções que os reduza sem duplicar o trabalho. Por exemplo, considere

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

É composto de três termos semelhantes, x = ((λg. ...) (λh.y)) e y = ((λf. ...) (λw.z)) , e, finalmente z = λw. (H (w (λy.y))) . Existem apenas duas reduções β possíveis a serem feitas aqui, em xe em y. Reduzir o termo x externo primeiro resulta na duplicação do termo y interno, e cada cópia terá que ser reduzida, mas reduzir o termo y interno primeiro duplicará seu argumento z, o que fará com que o trabalho seja duplicado quando os valores de he w são tornados conhecidos.

A redução ótima não é uma estratégia de redução para o cálculo lambda em um sentido estrito porque realizar a redução β perde a informação sobre os redexes substituídos que estão sendo compartilhados. Em vez disso, é definido para o cálculo lambda rotulado , um cálculo lambda anotado que captura uma noção precisa do trabalho que deve ser compartilhado.

Os rótulos consistem em um conjunto infinito contável de rótulos atômicos e concatenações , sobreposições e sublinhados de rótulos. Um termo rotulado é um termo de cálculo lambda em que cada subtermo possui um rótulo. A rotulagem inicial padrão de um termo lambda dá a cada subtermo um rótulo atômico exclusivo. A redução β rotulada é dada por: ${\ displaystyle ab}$ ${\ displaystyle {\ overline {a}}}$ ${\ displaystyle {\ underline {a}}}$

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

onde concatena rótulos,, e a substituição é definida da seguinte maneira (usando a convenção de Barendregt ): ${\ displaystyle \ cdot}$ ${\ displaystyle \ beta \ cdot T ^ {\ alpha} = T ^ {\ beta \ alpha}}$ ${\ displaystyle M [x \ mapsto N]}$

{\ displaystyle {\ begin {alinhados} x ^ {\ alpha} [x \ mapsto N] & = \ alpha \ cdot N & \ quad (\ lambda yM) ^ {\ alpha} [x \ mapsto N] & = (\ lambda yM [x \ mapsto N]) ^ {\ alpha} \\ y ^ {\ alpha} [x \ mapsto N] & = y ^ {\ alpha} & \ quad (MN) ^ {\ alpha} [x \ mapas para P] & = (M [x \ mapas para P] N [x \ mapas para P]) ^ {\ alpha} \ end {alinhados}}}

O sistema pode ser comprovado como confluente. A redução ótima é então definida como a ordem normal ou a redução mais externa à esquerda usando a redução por famílias, ou seja, a redução paralela de todos os redexes com o mesmo rótulo de parte de função.

Um algoritmo prático para redução ótima foi descrito pela primeira vez em 1989, mais de uma década após a redução ótima ter sido definida pela primeira vez em 1974. A Máquina Ótima de Ordem Superior de Bolonha (BOHM) é um protótipo de implementação de uma extensão da técnica para redes de interação . Lambdascope é uma implementação mais recente de redução ótima, também usando redes de interação.

Redução de chamadas por necessidade

A redução de chamada por necessidade pode ser definida de forma semelhante à redução ótima como redução mais à esquerda mais externa fraca usando a redução paralela de redexes com o mesmo rótulo, para um cálculo lambda rotulado ligeiramente diferente. Uma definição alternativa altera a regra beta para encontrar o cálculo "exigido". Isso requer estender a regra beta para permitir a redução de termos que não são sintaticamente adjacentes, portanto, essa definição é semelhante à definição rotulada, pois ambas são estratégias de redução para variações do cálculo lambda. Tal como acontece com chamada por nome e chamada por valor, a redução chamada por necessidade foi concebida para imitar o comportamento da estratégia de avaliação conhecida como "chamada por necessidade" ou avaliação preguiçosa .

Languages

In other projects

Estratégia de redução - Reduction strategy

Conteúdo

Definições

Reescrita de mandato

Cálculo lambda

Redução fraca

Redução ótima

Redução de chamadas por necessidade

Veja também

Notas

Referências

links externos