Cálculo lambda: diferença entre contextos e contextos de avaliação

Em primeiro lugar, gostaria de dizer que meu texto abaixo pode conter erros, portanto, sinta-se à vontade para apontar quaisquer erros na minha formulação da pergunta.

Considere um cálculo lambda sem tipo com booleanos e instruções if cujos termos são dados por esta sintaxe:

 t ::= v | t t | if t t t | x
 v ::= \x.t | #t | #f

Os contextos C, neste caso, seriam dados de acordo com esta sintaxe:

C ::= [-] | \x. C | C t | t C | if C t t | if t C t | if t t C 

Além disso, pode-se definir os contextos de avaliação E de acordo com essa outra sintaxe:

E ::= [-] | \x. E | v E | E t | if E t t 

Dividi minha pergunta em três sub-pontos que gostaria de abordar.

1. Quando as duas noções são usadas? Sei, por exemplo, que contextos de avaliação são usados ​​para definir a semântica do cálculo, mas o uso de contextos ainda me escapa. Também gostaria de alguma confirmação do meu conhecimento aqui.
2. Quando um deve ser preferido em relação ao outro e por quê?
3. Você poderia apontar para artigos relevantes que poderiam me ajudar a resolver esse problema?

O contexto é usado para muitos propósitos, mas geralmente para definir congruências em programas. Contextos de avaliação são um subconjunto de contextos. Eles geralmente são usados ​​para definir relações de redução. Deixe-me dar um exemplo de cada um.

Uma maneira formal de definir a igualdade de programas é dizer que dois programas e N são contextualmente iguais e podem se substituir em cada contexto sem uma mudança de comportamento. Podemos definir isso da seguinte maneira: M e N são contextualmente iguais, desde que todos os contextos de fechamento C [ ⋅ ] para M e N : C se nem C [ M $M$$N$$M$$N$$C[\cdot]$$M$$N$ se e somente se C [ N ] ⇓ t . Dizemos que um contexto está sefechando para M , N$C[M] \Downarrow t$$C[N] \Downarrow t$$M, N$$C[M]$ nem possuem variáveis ​​livres. A expressão M ⇓ t significa que o programa M reduz em um número finito de etapas o valor t . (Como um aparte, observe que a definição de equivalência contextual está mais envolvida para noções ricas de computação, por exemplo, processos concorrentes.)$C[N]$$M \Downarrow t$$M$$t$

Por outro lado, contextos de avaliação são contextos que não bloqueiam a avaliação. Mais precisamente, um contexto de avaliação é um termo com um orifício no ponto em que a próxima etapa de redução atômica deve ocorrer (ou pode ocorrer para computação não determinística). Portanto, a seguinte regra deve ser válida para os contextos de avaliação: Como exemplo de uso de contextos de avaliação, considere as regras de redução para ocálculo dovalor-λ-cálculo, onde não reduzimos emλ. Portanto, mesmo quandoM→N, não temos uma reduçãoλx. M→λx. N. Isso pode ser facilmente expresso com a regra contextual geral acima, juntamente com uma gramática para contextos de avaliação que omitemexpressõesλ. Os contextos de avaliação foram usados ​​pela primeira vez em

$$\frac{M \rightarrow N}{E[M] \rightarrow E[N]}$$ $\lambda$$\lambda$$M \rightarrow N$$\lambda x.M \rightarrow \lambda x.N$$\lambda$O relatório revisado sobre as teorias sintáticas do controle e estado seqüenciais por Felleisen e Hieb.

Um contexto é uma noção sintática. Um contexto é um termo com um buraco nele. (Ocasionalmente, existem contextos com vários orifícios, a definição será dada claramente nesse caso.) A sintaxe dos contextos é definida usando a sintaxe dos termos e permitindo que um subtermo seja um orifício $[]$ vez de um termo. Em BNF (eu uso a lambda-cálculo como um exemplo, sem booleans e se afirmações que não trazem nada para o exemplo.):

$$C ::= [] \mid x \mid t \, C \mid C \, t \mid \lambda x.C$$

Juntamente com a definição de um contexto, vem a definição de colocar um termo em um contexto. Se é um contexto e t é um termo, então C [ t ] é o termo obtido colocando t na árvore de sintaxe onde o orifício [ ] está em C [ t $C[]$$t$$C[t]$$t$$[]$$C[t]$ . Essa é basicamente uma substituição na qual a variável é garantida para ocorrer exatamente uma vez (mas observe que a “variável” substituída é uma variável no nível meta, , não uma variável no cálculo lambda ou em outro idioma dos termos t ).$[]$$t$

Os contextos são usados ​​para formular várias definições em semântica. Um exemplo comum é que a maioria das noções de avaliação envolve a definição de contextos nos quais a avaliação pode ser realizada. Por exemplo, considere o cálculo lambda. A noção fundamental de avaliação é dada pela regra da redução beta: onde M { x ← N } é a substituição

$$(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}$$ $M \{x\leftarrow N\}$ aplicado a M .$x \mapsto N$$M$

Esta não é a definição completa de redução beta: dado um termo , ele pode reduzir beta se houver subtermos M e N e uma variável x tal que t = ( λ x . M $t$$M$$N$$x$ ; mas mais geralmente t pode reduzir betase houver um subtermo t ' tal que t ' = ( λ x . M )$t = (\lambda x. M) \, N$$t$$t'$$t' = (\lambda x. M) \, N$ . Outra maneira de expressar isso é que pode reduzir beta se houver um contexto C e alguns termos M e N e uma variável x tal que t = C [ ( λ x . M $t$$C$$M$$N$$x$ . Quando existe tal redução, o lado direito é C [ M { x ← N $t = C[(\lambda x. M) \, N]$ . Para usar uma notação formal, a redução beta é definida pelas seguintes regras de dedução: $C[M \{x\leftarrow N\}]$ A mesma definição pode ser expressa explicitando todos os tipos de contextos:

$$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \qquad \dfrac{M \to_\beta N}{C[M] \to_\beta C[N]} (\gamma)$$ $$\dfrac{}{(\lambda x. M) \, N \to_\beta M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_\beta N}{\lambda x. M \to_\beta \lambda x. N} (C_\lambda) \qquad \dfrac{M \to_\beta N}{M \, P \to_\beta N \, P} (C_{@\lt}) \qquad \dfrac{M \to_\beta N}{P \, M \to_\beta P \, N} (C_{@\gt})$$

Essa definição gera redução beta, ou seja, uma noção de avaliação que permite reduzir qualquer subtermo. Cálculos como realizados em linguagens de programação geralmente não permitem reduzir subtermos dentro de funções: a regra de redução pode ser aplicada apenas no nível superior, ou no lado esquerdo ou no lado direito de um aplicativo. Podemos expressar isso através da definição de um novo tipo de contexto que não permite que todas as formas sintáticas: Podemos usar esta sintaxe para definir a noção semântica de avaliação não parcial:

$$D ::= [] \mid x \mid t \, D \mid D \, t$$ Também poderíamos apresentar essa definição expandindo-a, como fizemos acima para a redução beta completa: $$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} \qquad \dfrac{M \to_{np} N}{D[M] \to_{np} D[N]}$$ $$\dfrac{}{(\lambda x. M) \, N \to_{np} M \{x\leftarrow N\}} (\beta) \\ \dfrac{M \to_{np} N}{M \, P \to_{np} N \, P} (C_{@\lt}) \qquad \dfrac{M \to_{np} N}{P \, M \to_{np} P \, N} (C_{@\gt})$$ $D$ seria chamado de contexto de avaliação porque é usado para definir uma noção de avaliação. Um contexto de avaliação não é um tipo especial de contexto; em vez disso, chamá-lo de contexto de avaliação é uma questão de como o contexto é usado .

$V$

$$V ::= x V_1 \ldots V_n \mid \lambda x. M$$ $$E ::= [] \mid M \, E \mid E \, V$$ Compared with $D$ above, the hole can be on the function side of an application if the argument of the application is a value. Define then the following notion of reduction: $$\dfrac{}{(\lambda x. M) \, V \to_{cbva} M \{x\leftarrow V\}} (\beta_{cbva}) \qquad \dfrac{M \to_\beta N}{E[M] \to_{cbva} E[N]} (\gamma_{cbva})$$ With the restriction that the argument of the function must be a value in the first rule and that lambda abstractions are not contexts, we're defining a call-by-value evaluation strategy. With the further restriction that the argument is evaluated before the function, this is applicative order call by value.