Cálculo Lambda: Como os contextos de avaliação “funcionam”

No cálculo lambda puro, temos o conjunto de termos definido indutivamente (a gramática):

$$e::= x \mid \lambda x . e \mid e_1 e_2$$

Sob a estratégia de avaliação de valor por chamada, temos as regras de inferência para redução beta e regras sobre como avaliar aplicativos (regras de congruência). Estou tentando entender como os contextos de avaliação podem substituir as regras de congruência sem realmente alterar a sintaxe do idioma. Sem contextos de avaliação, temos o seguinte:

$$\frac{e_1 \rightarrow e_1'}{e_1e_2 \rightarrow e_1'e_2}$$ e $$\frac{e_2 \rightarrow e_2'}{ve_2 \rightarrow ve_2'}.$$

Isso faz sentido, pois se tivermos uma instância de uma expressão , fica claro que é do formato e, portanto,$t = (\lambda f . \lambda x. f x)((\lambda y .y)\lambda z .z)\lambda w.w$$e_1e_2 \rightarrow e_1'e_2$

$$(\lambda f . \lambda x. f x)((\lambda y .y)\lambda z .z)\lambda w.w \rightarrow (\lambda f . \lambda x. f x)(\lambda z .z)\lambda w.w$$

Se substituirmos as regras de congruência pelos contextos de avaliação: , precisamos de apenas uma regra para expressar as regras de congruência da linguagem:

$$E::= [\cdot] \mid Ee \mid vE$$ $$\frac{e \rightarrow e'}{E[e] \rightarrow E[e']}.$$

Estou confuso sobre como os contextos de avaliação podem nos dizer como avaliar a expressão de cima sem alterar a sintaxe do idioma. Não entendo como o contexto da avaliação "funciona" sem reescrever como$t$$t$

$$E_t = (\lambda f . \lambda x. f x)[\cdot]\lambda w.w$$

onde . Não há razão a priori óbvia para avaliar sob chamada por valor sem o conhecimento de . Eu realmente não tenho idéia de onde estou errado. Alguém pode ajudar a corrigir meu pensamento?$t = E_t[((\lambda y .y)\lambda z .z)]$$t$$E_t$

A sutileza reside em onde é feita a distinção entre linguagem e metalinguagem. Como René Magritte colocou:

$(\lambda f. \lambda x. f x) ((\lambda y.y) (\lambda z.z)) (\lambda w.w)$é um termo lambda, escrito na sintaxe dos termos lambda. Vamos chamar isso de termo lambda$t$. Deixei$M$ seja o termo lambda $(\lambda f. \lambda x. f x) ((\lambda y.y) (\lambda z.z))$. eu consigo escrever$t = M \, (\lambda w.w)$(e esta é uma verdadeira igualdade): tudo o que fiz foi dar um nome a um subtermo. Se você considerar o lado direito dessa igualdade "$M \, (\lambda w.w)$”, Não está escrito na sintaxe dos termos lambda; está escrito em uma notação matemática em que permitimos que uma carta represente um termo lambda.

Quando escrevemos uma regra como

$$\frac{e_2 \to e_2'}{v \, e_2 \to v \, e_2'}$$ afirma o seguinte axioma: para qualquer termo lambda $e_2$ e $e_2'$ e qualquer valor $v$, E se $e_2$ reduz a $e_2'$ então $v \, e_2$ reduz a $v \, e_2'$. Aqui estamos novamente usando meta-notações (ou seja, notações matemáticas para raciocinar sobre uma linguagem): a seta$\to$expressar a relação de redução; metavariáveis ​​em que uma letra indica a classificação ($e$ para termos lambda, $v$para valores) e subscritos e números primos distinguem entre metavariáveis ​​do mesmo tipo; a notação de fração para escrever um axioma indutivo.

Quando escrevemos a regra

$$\frac{e \to e'}{E[e] \to v E[e']}$$ então de novo $E[\cdot]$é uma meta-notação, parte da metalinguagem e não da sintaxe lambda-term. A regra significa: para quaisquer termos lambda$e$ e $e'$ e qualquer contexto de avaliação $E[\cdot]$, E se $e$ reduz a $e'$ então $E[e]$ reduz a $E[e']$.

Se chamarmos o contexto $(\lambda f. \lambda x. f x)[\cdot] (\lambda w.w)$ pelo (meta-) nome $E_t$, então $t = E_t[(\lambda y.y)(\lambda z.z)]$. Novamente, essa é uma igualdade entre dois termos lambda, ou seja, o mesmo termo lambda está em ambos os lados do sinal de igual. O que temos à esquerda e à direita são duas meta-notações diferentes para o mesmo termo lambda$(\lambda f. \lambda x. f x) ((\lambda y.y) (\lambda z.z)) (\lambda w.w)$: um que usa um nome que demos a ele, outro que é um pouco mais complicado envolvendo um contexto ao qual demos um nome.

Dado o termo $t$, como você descobre como isso pode reduzir?

• Com a notação usando várias regras, você precisa encontrar uma árvore de deduções (em geral - aqui a derivação é linear, portanto, basta encontrar uma cadeia que conduz a um axioma).
• Com a notação usando contextos de avaliação, é necessário encontrar um contexto de avaliação adequado.

A gramática do contexto da avaliação segue a estrutura das regras de avaliação, portanto, na verdade, não são realmente dois métodos, mas duas maneiras diferentes de expressar a mesma definição.

Para entender isso, recomendo vivamente o seguinte exercício: no seu idioma favorito, implemente a avaliação de chamada por valor de termo lambda de maneira direta, com um tipo representando termos lambda e uma função executando uma etapa de redução.