Regra de redução para IF?

7

Estou trabalhando com "A Implementação de Linguagens de Programação Funcional", de Simon Peyton Jones, e na página 20 eu vejo:

SE VERDADEIRO ((λp.p) 3) ↔ SE VERDADEIRO 3 (por β vermelho) (1)
                   ↔ (λx.IF VERDADEIRO 3 x) (por η vermelho) (2)
                   ↔ (λx.3) (3)

Os passos 1 a 2 são explicados como conversão η. Mas de 2 a 3 diz "O passo final é a regra de redução para o FI". Não sei ao certo qual é essa regra de redução.

logic programming-languages lambda-calculus term-rewriting operational-semantics galaxybeing
fonte

Respostas:

10

A regra de redução que você solicita é a regra usual para declarações IF. Consiste em duas regras de computação e uma regra de contexto:

  • IF TRUE a b → a

  • IF FALSE a b → b

  • a→a′IF a b c→IF a′ b c

Em ambos os call-by-value (estrito) e configurações (preguiçoso) chamada-a-necessidade, tanto e podem ser expressões arbitrárias. Eles não precisam ser valores.ab

Regras desse tipo, que reduzem funções específicas (aqui IF), geralmente são chamadas de regras delta.

Agora, o motivo (2) acima é necessário para que as regras de redução para possam ser aplicadas. requer 3 argumentos, mas no termo original ele possui apenas dois, portanto não pode ser reduzido. ( está sendo parcialmente aplicado, como qualquer função do Haskell. Isso significa que apenas parte de seus argumentos precisa ser fornecida.) O uso de -expansion fornece o argumento adicional, sem alterar a semântica.IFIFIFη

Dave Clarke
fonte
11
Gostaria de acrescentar IF a b c -> IF a' b c with a-> a'
Fabio F.
Sim, mas a conversão η não deve adicionar condições? Parece que passar de IF TRUE 3 para λx.IF TRUE 3 x (desculpe minha omissão de x na postagem original) - se usado na próxima etapa como em conformidade com a redução de IF - não é exatamente honesto, porque adicionamos o x apenas para ser a metade MAIS quasi. Por exemplo, e se o problema fosse SE FALSO 3 ? Poderíamos tê-lo convertido em λx.IF FALSE 3 x ? Então o passo 3 teria sido λx.x , o que não parece certo ... Estranho, isso. O ponto era provar que SE VERDADEIRO ((λp.p) 3) é equivalente a (λx.3) Isso me deixa confuso.
galaxybeing
@ galaxybeing: adicionei um comentário sobre por que você usa -expansion. Por fim, é para que o IF tenha dois argumentos e, portanto, suas regras de redução possam ser aplicadas. η
Dave Clarke
@galaxybeing IF FALSE 3 é equivalente a \x -> IF FALSE 3 x(supondo que a aplicação parcial de IFseja permitida). IF FALSE 3precisa de mais um argumento para ser reduzido a um valor; aplicá-lo aos xrendimentos IF FALSE 3 x, o que reduz a simplesmente x. Portanto, IF FALSE 3é de fato equivalente a \x -> x, desde que estejamos usando o cálculo lambda sem tipo; se você tentar fazer isso no Haskell (definindo uma função if' :: Bool -> a -> apara que possa aplicá-la parcialmente), você obterá a idfunção especializada para qualquer tipo que Haskell deduza para o 3.
Ben