Por que as abstrações lambda são os únicos termos que são valores no cálculo lambda sem tipo?

Estou confuso com a seguinte afirmação: "Os únicos valores no cálculo lambda sem tipo são abstrações lambda".

Por que os outros termos não são valores? O que significa uma abstração lambda ser um valor? A primeira coisa que me veio à mente foi que talvez as abstrações lambda sejam as únicas formas normais possíveis, mas isso não é verdade, é claro, por exemplo . $(\lambda x.\; x)\;y \to y$

Alguém pode me esclarecer?

logic lambda-calculus codd
fonte

Onde você viu isso? A definição de valor pode variar.

Jmad

(λ x . x) y

$(\lambda x. x)\ y$ não é uma abstração lambda, é uma aplicação, ou seja, a aplicação de

(λ x . x)

$(\lambda x. x)$ para

y

$y$ .

Dave Clarke

@DaveClarke: Eu acho que Jeroen quis dizer que

y

$y$ era uma forma normal (para provar que um valor é uma abstração) e não que era uma abstração (para provar que uma abstração é um valor).

(λ x . x) y

$(λx.x)y$

Jd4

Variáveis são sempre valores, em todos os cálculos.

Fabio F.

@ DaveClarke: Acabei de verificar o livro de Pierce. A confusão surgiu porque a semântica operacional do cálculo lambda é abordada pela primeira vez informalmente. Diz-se em uma nota de rodapé que os únicos valores do cálculo são abstrações lambda. Mais tarde, quando a semântica é formalmente definida, fica claro que apenas termos fechados estão sendo considerados.

codd

Respostas:

Há várias coisas acontecendo aqui:

O idioma que você está falando não possui tipos de dados adicionais, caso contrário, haveria outros tipos de valores.
A estratégia de redução do idioma não reduz dentro de abstrações lambda. Chamada por valor e chamada por nome estão em conformidade com isso. Caso contrário, nem toda abstração lambda seria normal.
Geralmente, considera-se expressões fechadas como programas; portanto, não há variáveis livres; portanto, o exemplo que você apresenta não é considerado.

Outros termos não são valores porque podem ser reduzidos ou não aparecem em programas fechados.

O fato de uma abstração lambda ser um valor significa que não pode mais ser reduzido (dependendo da estratégia de redução).

Para termos abertos, variáveis também são valores.

Dave Clarke
fonte

Isso faz sentido. O principal é que apenas termos fechados devem ser levados em consideração. Vou verificar com a fonte original para ver se isso faz parte da definição formal da semântica operacional.

codd