Qual é a diferença entre estratégias de redução e estratégias de avaliação?

Do artigo sobre estratégia de avaliação na Wikipedia:

A noção de estratégia de redução no cálculo lambda é semelhante, mas distinta.

Do artigo sobre estratégia de redução na Wikipedia:

É semelhante, mas sutilmente diferente da noção de estratégia de avaliação em ciência da computação.

Qual é a distinção sutil entre estratégias de avaliação e estratégias de redução que esses dois artigos sugerem? Eles são apenas dois conceitos semelhantes de domínios diferentes?

Uma estratégia de redução é uma função no Lambda que seleciona um redex (expressão redutível) de todos os redexes possíveis - dependendo do que você define como redex.

Informalmente, uma estratégia de avaliação é a ordem em que uma linguagem avalia seus argumentos. Uma estratégia de passagem de parâmetros é o que o idioma entrega à função.

Para entender a conexão entre eles, estude o artigo de Plotkin sobre Chamada por nome, Chamada por valor e cálculo lambda. Ele explica claramente que você deseja escolher AXIOMS ​​distintos, dependendo de qual ordem de avaliação você deseja. Para Cb-name, você deseja o axioma beta antigo e, para cb-value, deseja um axioma de valor beta. Se você fizer isso, todos os meta-teoremas funcionam da mesma maneira para os dois sabores. Mais tarde mostrei (com muitos colaboradores) que essa ideia generaliza tudo o que o mundo da PL estudou.

É tudo técnico, não um poema que possa ser interpretado. Basta ler sobre isso.

- Matthias Felleisen

ps Eu direi que acho que as pessoas terão mais facilidade em entender o artigo de Plotkin da Parte I em nosso livro Redex. Mas sim, é 3x o comprimento.

O artigo da wikipedia "Estratégia de redução" é inteiramente extraído de uma edição específica feita por um IP anônimo no artigo "Estratégia de avaliação".

A visão que ele representa não é consensual, no sentido em que suspeito que relativamente poucas pessoas do campo darão espontaneamente essa resposta se você perguntar a eles "você distinguiria os nomes 'estratégia de redução' e 'estratégia de avaliação'?". Só ouvi isso de Matthias Felleisen, que é inflexível sobre a importância dessa distinção - e suponho que esse ponto de vista seja compartilhado por outros que tiveram a chance de dedicar algum tempo para discutir esses pontos em detalhes com ele.

Meu entendimento atual desse ponto (mas ainda não estudei os detalhes técnicos com toda a justiça) é sobre o seguinte: trata-se de usar a semântica "grande passo" versus semântica "pequeno passo" - essa distinção é padrão e compreendida por todos no campo. A semântica de pequenos passos define um passo atômico de redução e, em geral, o resultado ainda é redutível. A semântica de grandes etapas define uma "grande" etapa de redução que vai do programa inicial ao seu valor (ou algum tipo mais rico de "resposta" se o seu idioma tiver outros efeitos observáveis ​​que não o retorno de um valor, por exemplo, entrada / saída ou estado mutável).

Se você definir uma relação de passo grande e passo pequeno, poderá verificar se a semântica de passo grande está incluída no fechamento transitivo da relação de passo pequeno e se a relação de passo pequeno não se reduz a outros termos bloqueados aqueles alcançados pela relação de grande passo ou divergem se a redução de grande passo for definida. Esta é a relação de coerência esperada entre ambos.

Penso que a redação do artigo pode ser mais ou menos descrita, em termos modernos, como "estratégia de avaliação é a relação de grande passo", "estratégia de redução é a relação de pequeno passo". Observe que a discussão feita no artigo "Estratégia de redução" é principalmente sobre artigos e pesquisas (e, mais importante, pontos de vista eloquentes formados durante a leitura e escrita) entre 1973 e 1991, em um momento em que essas noções nasceram e provavelmente não tão bem compreendido quanto hoje. (a semântica de passo grande foi enfatizada por Kahn em 1987, e um dos trabalhos mais importantes sobre a semântica de passo pequeno é Wright e Felleisen, 1992)

Para o lado mais opinativo do motivo pelo qual Felleisen insiste na importância dessa diferença (ou seja, por que pode haver mais do que apenas "pequeno passo vs. grande passo, meh"), meu entendimento atual é o seguinte: O ponto que está sendo feito é que a semântica de pequenas etapas deve ser vista como um detalhe de implementação. oa semântica, de acordo com esse argumento, é a função abstrata que mapeia cada programa com seu valor / resposta, e o restante são dispositivos de implementação projetados para aproximar esse valor (ou raciocinar sobre a equivalência induzida por essa semântica). Quando dizemos grande passo hoje, pensamos em um sistema de regras de inferência de natureza sintática, mas a "estratégia de redução" que está sendo discutida acima é, na verdade, sua abstração como um mapeamento. (Não acho que isso dê mais expressividade ou força à noção na prática, mas a torna mais abstrata.)

Então, acho que o que esta página da Wikipedia e Matthias Felleisen estão dizendo é algo como: "Defina sua avaliação da maneira que desejar, mas no final das contas, o que importa é o modo como seus programas são mapeados para seus valores / respostas / comportamentos, e é isso que deve ser chamado de 'semântica operacional' e fundamentado. ".

Observe que essa posição contraria um pouco a distinção atual (que eu acho bastante consensual, mas pode ser um viés cultural da minha parte) entre "semântica operacional" e "semântica denotacional", onde a primeira é vista como de natureza mais sintática. (definida como uma relação de redução), e a última é tipicamente caracterizada pelo fato de que programas equivalentes computacionalmente têm exatamente a mesma denotação (portanto, a denotação é inconsciente do mecanismo de computação real). Sob essa última visão, o que é proposto como uma "estratégia de avaliação" ou "semântica operacional" nos artigos e minha explicação acima preferiria ser visto como uma semântica denotacional - mas reconhecidamente de natureza mais concreta do que a maioria: valores / respostas / comportamentos estão mais próximos de objetos sintáticos do que muitos domínios semânticos.

Referências: para entender esse ponto de vista, provavelmente é útil voltar à sua fonte proclamada, que é o artigo de Gordon Plotkin em 1973. Você também pode ter boa sorte tentando um dos últimos artigos citados na wikipedia; Eu descobri, por exemplo, que "Parameter-Passing and Lambda Calculus", de Crank e Felleisen, 1991, deu uma visão muito clara de sua posição sobre o assunto nas primeiras páginas.