Redex e estratégias de redução

5

Estou estudando Tipos e linguagens de programação e tenho dificuldade em entender meus conceitos do quinto capítulo, O cálculo lambda não tipado .

Especificamente, redex , redução e as várias estratégias de avaliação estão fazendo a minha cabeça. O seguinte é o que eu entendo colocar em minhas próprias palavras, em uma tentativa de explicar coisas para mim e obter mais pessoas com conhecimento para corrigir meus erros / imprecisões. Estou honestamente inseguro quanto a saber se este é um formato aceitável para o stackexchange, e estou aberto a sugestões para tornar isso um melhor ajuste.

Note que outros tentaram responder a uma pergunta muito semelhante, mas ainda me deixaram confuso:

Redex

Se meu entendimento estiver correto, um redex é uma expressão redutível, isto é, a aplicação de um termo lambda para uma abstração lambda.

Ou, mais concretamente, um redex sempre tem o formato (λx.s)t .

Redução do Redex

A redução de (λx.s)t é feita substituindo todas as ocorrências livres de x em s por t . Por exemplo:

(λx.x + 2) 1
→ 1 + 2
→ 3

O processo de reduzir uma expressão lambda à sua forma normal é impulsionado por uma estratégia de avaliação: um algoritmo para escolher qual redex reduzir primeiro. Para descrevê-los, precisamos de mais vocabulário.

Qualificações do Redex

à esquerda e à direita

  • o redex mais à esquerda é aquele cuja abstração é textualmente à esquerda de todos os outros redexes.
  • o redex mais à direita é aquele cuja abstração é textualmente à direita de todos os outros redexes.

Então, por exemplo, em (λx.x + 2) (λy.y + 1) , temos:

  • redex mais à esquerda: λx.x + 2
  • redex mais à direita: λy.y + 1

Só pode haver um redex à esquerda e mais à direita em uma determinada expressão. Estou assumindo que em uma expressão composta de um único redex, esse redex é o mais à esquerda e o mais à direita.

Mais íntimos e mais externos

  • um redex mais interno é aquele que não contém nenhum outro redex.
  • um redex mais externo é aquele que não está contido em nenhum outro redex.

Então, por exemplo, em (λx.(λy.y + 1) x) 2 , temos:

  • mais interno: λy.y + 1 , pois não contém outro redex.
  • mais externo: λx.[...] , pois não está contido em nenhum outro redex.

Estou assumindo que em uma expressão composta de um único redex, esse redex é tanto externo quanto interno.

Estratégias de avaliação

Tendo definido isso, podemos falar sobre as duas estratégias de avaliação com as quais estou lutando: chamar pelo nome e chamar pelo valor .

Ligar por nome

Em chamada por nome , o redex mais externo mais à esquerda é sempre escolhido para redução. Além disso, nenhuma redução pode ocorrer dentro de uma abstração de lambda. O exemplo dado por Tipos e Linguagens de Programação é:

id (id (λz. id z)) # the leftmost, outermost redex is the very first id
→ id (λz. id z)    # the leftmost, outermost redex is still the first id
→ λz. id z         # there is no outermost redex remaining, we're done.

Eu não entendo a necessidade de a definição da estratégia incluir nenhuma redução pode ocorrer dentro de uma abstração de lambda : isso não está implícito no fato de que somente os redexes mais externos são elegíveis para redução?

Chamada por valor

Em chamada por valor , o redex mais externo à direita é sempre escolhido para redução. O exemplo dado por Tipos e Linguagens de Programação é:

id (id (λz. id z)) # the rightmost, outermost redex is the second id
→ id (λz. id z)    # the rightmost, outermost redex is the first id
                   # (it's textualy on the left, but there is no redex to its right)
→ λz. id z         # the only remaining redex is not outermost (it's contained within
                   # an abstraction) and cannot be reduced.
    
por Nicolas Rinaudo 12.02.2014 / 13:23
fonte

2 respostas

4

Em chamada por nome:

I do not understand the need for the definition of the strategy to include no reduction can occur within a lambda abstraction: is that not implied by the fact that only outermost redexes are eligible for reduction?

Não. De acordo com sua definição de outermost, um redex é mais externo se não estiver contido dentro de qualquer outro redex. No código a seguir, id z é o redex mais externo, não λz. id z (que é uma abstração, não um redex).

id (id (λz. id z)) # the leftmost, outermost redex is the very first id
→ id (λz. id z)    # the leftmost, outermost redex is still the first id
→ λz. id z         # there is no outermost redex remaining, we're done.

Observe que na descrição de chamada por valor em TAPL, há uma palavra ausente na definição de valor:

p 57, definition of call-by-value

"a term that is finished computing..." should be "a CLOSED term that is finished computing..."

Esta é provavelmente a razão da sua confusão.

Editado para adicionar: Acontece que a descrição do autor da chamada por valor é inconsistente com a semântica operacional dada no livro para o cálculo lambda não tipado sob avaliação de valor por chamada. De acordo com a descrição de chamada por valor, na página 57, λx. id id seria avaliado como λx. id , pois id é um valor. (um termo fechado que não pode ser reduzido) e id id é o redex mais externo. No entanto, a semântica operacional (na página 72) não possui uma regra que possa reduzir esse termo dessa maneira. Além disso, na mesma página em que o autor escreve: "A avaliação de (chamada a valor) para quando atinge um lambda, os valores podem ser termos-lambda arbitrários" sugerindo que não são permitidas reduções dentro de abstrações.

Na descrição de chamada por nome, o autor menciona que nenhuma redução é permitida dentro de abstrações, mas deixa de fazê-lo na descrição de chamada por valor.

Segunda edição: Acredito que a correção que adiciona a palavra "FECHADO" à definição de chamada por valor mencionada acima cause uma inconsistência com a semântica operacional. Por exemplo, id (λx. x y) reduz para λx. x y de acordo com a semântica operacional fornecida. (Como os valores são abstrações arbitrárias de lambda e a regra 'E-AppAbs' se aplica aqui) No entanto, λx. x y não é um termo fechado, pois a ocorrência de y não está vinculada.

As erratas do livro estão disponíveis em: link

    
por 06.05.2015 / 19:18
fonte
-1

Você disse que o redex mais externo de (λx. (λy.y + 1) x) 2 é λx [...] mas redex é da forma (λx.s) t. λx [...] não é dessa forma, mas a expressão inteira (λx. (λy.y + 1) x) 2 é. Portanto, a expressão inteira é o redex mais externo.

    
por 01.01.2018 / 19:14
fonte

Tags