Cálculo lambda não tipificado: Por que o call-by-value é estrito?

5

Atualmente estou lendo "Types and Programming Languages" de Benjamin C. Pierce. Antes de entrar realmente na teoria dos tipos, explica o cálculo lambda e as estratégias de avaliação.

Estou um pouco confuso com a explicação de chamada por nome vs chamada por valor neste contexto.

As duas estratégias são explicadas da seguinte maneira:

chamada por nome

Como ordem normal em que ele escolhe primeiro o redex mais externo, mas mais restritivo por não permitir reduções dentro de abstrações. Um exemplo:

  id (id (λz. id z))
→ id (λz. id z)
→ λz. id z

chamada por valor

Somente os redexes mais externos são reduzidos e um redex é reduzido somente quando seu lado direito já foi reduzido a um valor - um termo que termina a computação e não pode ser reduzido mais. Um exemplo:

  id (id (λz. id z))
→ id (λz. id z)
→ λz. id z

(identical to the call by name evaluation)

Ok, até aí tudo bem. Mas isso é seguido pelo seguinte parágrafo:

The call-by-value strategy is strict, in the sense that the arguments to functions are always evaluated, whether or not they are used by the body of the function. In contrast, non-strict (or lazy) strategies such as call-by-name and call-by-need evaluate only the arguments that are actually used.

Eu sei o que chamada por valor e chamada por nome significa praticamente, por ter usado (entre outros) C e Haskell, mas não vejo por que a estratégia de avaliação explicada acima leva a isso no cálculo lambda. Essa é uma regra adicional que sempre acompanha a chamada por valor ou segue a estratégia de redução descrita acima?

Especialmente desde que as etapas de redução nos exemplos são idênticas, não consigo ver a diferença entre as duas estratégias e adoraria se alguém pudesse me ajudar a ganhar alguma intuição.

    
por beta 27.05.2013 / 18:23
fonte

1 resposta

5

Sim, a estratégia de avaliação descrita conduz a uma semântica estrita, e os exemplos são espetacularmente mal escolhidos para esconder a diferença entre as duas semânticas. Eu acho que é mais ou menos assim:

id (id (λz. id z))  # strict means we evaluate the right hand side
→ id (λz. id z)     # RHS has been reduced (id (λz. id z)) → (λz. id z) by inner id 
→ λz. id z          # now we have called the outer id to obtain the final value

id (id (λz. id z))  # normal form means we call the outer id and pass RHS as a closure
→ id (λz. id z)     # outer id just returned its argument unevaluated → id (λz. id z) 
→ λz. id z          # now same thing is repeated with inner id

Assim, as etapas de derivação parecem sintaticamente as mesmas, mas coisas diferentes estão acontecendo. Sob o esquema de avaliação preguiçosa, id na verdade não força a avaliação de seu argumento: ele simplesmente retorna esse argumento em si. Portanto, não apenas id x e x geram o mesmo valor, mas na verdade são equivalentes: id x realmente gera x , e então x produz seu valor mais tarde quando realmente necessário. Da mesma forma, id (id (λz. id z)) simplesmente gera o lado direito não avaliado (id (λz. id z)) .

O que é confuso no exemplo é que ele é baseado no aninhamento da mesma função, que é apenas id , de modo que duas reduções diferentes geram id (λz. id z) . Em um deles, é apenas uma cópia da expressão id interna e, no outro, é o valor da expressão interna, sendo passado um argumento para o exterior id .

    
por 27.05.2013 / 19:40
fonte

Tags