Máquina Krivine - Krivine machine
Na ciência da computação teórica , a máquina Krivine é uma máquina abstrata (às vezes chamada de máquina virtual ). Como uma máquina abstrata, ele compartilha recursos com as máquinas de Turing e a máquina SECD . A máquina Krivine explica como calcular uma função recursiva. Mais especificamente, visa definir rigorosamente a redução da forma normal de cabeça de um termo lambda usando a redução de chamada por nome . Graças ao seu formalismo, ele conta em detalhes como funciona uma espécie de redução e estabelece a base teórica da semântica operacional das linguagens de programação funcional . Por outro lado, a máquina Krivine implementa call-by-name porque avalia o corpo de um β- redex antes de aplicar o corpo ao seu parâmetro. Em outras palavras, em uma expressão ( λ x . T ) u ela avalia primeiro λ x . t antes de aplicá-lo a u . Em programação funcional , isso significaria que, para avaliar uma função aplicada a um parâmetro, ele avalia primeiro a função antes de aplicá-la ao parâmetro.
A máquina Krivine foi projetada pelo lógico francês Jean-Louis Krivine no início da década de 1980.
Redução da forma normal de chamada por nome e cabeça
A máquina Krivine é baseada em dois conceitos relacionados ao cálculo lambda , ou seja, redução de carga e chamada pelo nome.
Redução da forma normal da cabeça
Um redex (também se diz β-redex) é um termo do cálculo lambda da forma ( λ x . T ) u . Se um termo tem a forma ( λ x . T ) u 1 ... u n , diz-se que é um redex de cabeça . Uma forma normal de cabeça é um termo do cálculo lambda que não é um redex de cabeça. Uma redução de cabeça é uma sequência (não vazia) de contrações de um termo que contrai redexes de cabeça. Uma redução de cabeça de um termo t (que se supõe não estar na forma normal de cabeça) é uma redução de cabeça que começa em um termo t e termina em uma forma normal de cabeça. De um ponto de vista abstrato, a redução de carga é a forma como um programa calcula quando avalia um subprograma recursivo. É importante entender como essa redução pode ser implementada. Um dos objetivos da máquina Krivine é propor um processo para reduzir um termo na forma normal do cabeçote e descrever formalmente esse processo. Como Turing usou uma máquina abstrata para descrever formalmente a noção de algoritmo, Krivine usou uma máquina abstrata para descrever formalmente a noção de redução da forma normal da cabeça.
Um exemplo
O termo (( λ 0) ( λ 0)) ( λ 0) (que corresponde, se alguém usar variáveis explícitas, ao termo ( λx . X ) ( λy . Y ) ( λz . Z )) não é normal de cabeça forma porque ( λ 0) ( λ 0) contrai em ( λ 0) produzindo o redex da cabeça ( λ 0) ( λ 0) que se contrai em ( λ 0) e que é, portanto, a forma normal da cabeça de (( λ 0) ( λ 0)) ( λ 0). Dito de outra forma, a forma de contração normal da cabeça é:
- (( λ 0) ( λ 0)) ( λ 0) ➝ ( λ 0) ( λ 0) ➝ λ 0,
que corresponde a:
- ( λx . x ) ( λy . y ) ( λz . z ) ➝ ( λy . y ) ( λz . z ) ➝ λz . z .
Veremos mais adiante como a máquina de Krivine reduz o termo (( λ 0) ( λ 0)) ( λ 0).
Chamada pelo nome
Para implementar a redução de cabeça de um termo uv que é um aplicativo, mas que não é um redex, deve-se reduzir o corpo u para exibir uma abstração e, portanto, criar um redex com v . Quando um redex aparece, ele o reduz. Para reduzir sempre o corpo de um aplicativo é chamado primeiro por nome . A máquina Krivine implementa chamada por nome .
Descrição
A apresentação da máquina de Krivine dada aqui é baseada em notações de termos lambda que usam índices de Bruijn e assume que os termos dos quais ela calcula as formas normais da cabeça são fechados . Ele modifica o estado atual até que não possa mais fazer isso, caso em que obtém uma forma normal de cabeça. Esta forma normal de cabeça representa o resultado do cálculo ou produz um erro, o que significa que o termo a partir do qual começou não está correto. No entanto, ele pode entrar em uma seqüência infinita de transições, o que significa que o termo que ele tenta reduzir não tem forma normal principal e corresponde a um cálculo não finalizado.
Foi provado que a máquina Krivine implementa corretamente a redução da forma normal da chamada pelo nome no cálculo lambda. Além disso, a máquina de Krivine é determinística , uma vez que cada padrão do estado corresponde a no máximo uma transição de máquina.
O Estado
O estado tem três componentes
- um termo ,
- uma pilha ,
- um ambiente .
O termo é um termo λ com índices de Bruijn. A pilha e o ambiente pertencem à mesma estrutura de dados recursiva. Mais precisamente, o ambiente e a pilha são listas de pares <termo, ambiente> , que são chamados de fechamentos . A seguir, a inserção como cabeçalho de uma lista ℓ (pilha ou ambiente) de um elemento a é escrita a: ℓ , enquanto a lista vazia é escrita □. A pilha é o local onde a máquina armazena os fechamentos que devem ser avaliados posteriormente, enquanto o ambiente é a associação entre os índices e os fechamentos em um determinado momento da avaliação. O primeiro elemento do ambiente é o fechamento associado ao índice 0 , o segundo elemento corresponde ao fechamento associado ao índice 1 etc. Se a máquina tem que avaliar um índice, ela busca lá o par <termo, ambiente> o fechamento que produz o termo a ser avaliado e o ambiente no qual esse termo deve ser avaliado. Essas explicações intuitivas permitem entender as regras de funcionamento da máquina. Se alguém escrever t para termo, p para pilha e e para ambiente, os estados associados a essas três entidades serão escritos t , p, e. As regras explicam como a máquina transforma um estado em outro, após identificar os padrões entre os estados.
O estado inicial visa avaliar um termo t , é o estado t , □, □, em que o termo é t e a pilha e o ambiente estão vazios. O estado final (na ausência de erro) é da forma λ t , □, e, ou seja, os termos resultantes são uma abstração junto com seu ambiente e uma pilha vazia.
As transições
A máquina Krivine tem quatro transições: App , Abs , Zero , Succ .
| Nome | Antes | Depois de |
|---|---|---|
|
Aplicativo |
tu , p, e |
t , < u , e>: p, e |
|
Abdômen |
λ t , < u , e '>: p, e |
t , p, < u , e '>: e |
|
Zero |
0 , p, < t , e '>: e |
t , p, e ' |
|
Succ |
n + 1 , p, < t, e '>: e |
n, p, e |
O aplicativo de transição remove o parâmetro de um aplicativo e o coloca na pilha para avaliação posterior. A transição Abs remove o λ do termo e abre o fechamento do topo da pilha e o coloca no topo do ambiente. Este fechamento corresponde ao índice de de Bruijn 0 no novo ambiente. A transição Zero leva o primeiro fechamento do ambiente. O termo desse fechamento passa a ser o termo atual e o ambiente desse fechamento passa a ser o ambiente atual. A transição Succ remove o primeiro fechamento da lista de ambientes e diminui o valor do índice.
Dois exemplos
Vamos avaliar o termo ( λ 0 0) ( λ 0) que corresponde ao termo ( λ x . X x ) ( λ x . X ). Vamos começar com o estado ( λ 0 0) ( λ 0), □, □.
|
( λ 0 0) ( λ 0), □, □ |
|
λ 0 0, [< λ 0, □>], □ |
|
0 0, □, [< λ 0, □>] |
|
0, [<0, < λ 0, □ >>], [< λ 0, □>] |
|
λ 0, [<0, < λ 0, □ >>], □ |
|
0, □, [<0, < λ 0, □ >>] |
|
0, □, [< λ 0, □>] |
|
λ 0 , □, □ |
A conclusão é que a forma normal da cabeça do termo ( λ 0 0) ( λ 0) é λ 0. Isso se traduz com variáveis em: a forma normal da cabeça do termo ( λ x . X x ) ( λ x . X ) é λ x . x .
Vamos avaliar o termo (( λ 0) ( λ 0)) ( λ 0) como mostrado abaixo:
| (( λ 0) ( λ 0)) ( λ 0), □, □ |
| ( λ 0) ( λ 0), [<( λ 0), □>], □ |
| ( λ 0), [<( λ 0), □>, <( λ 0), □>], □ |
| 0, [<( λ 0), □>], [<( λ 0), □>] |
| λ 0, [<( λ 0), □>], □ |
| 0, □, [<( λ 0), □>] |
| ( λ 0), □, □ |
Isso confirma o fato acima de que a forma normal do termo (( λ 0) ( λ 0)) ( λ 0) é ( λ 0).
Veja também
Notas
Referências
O conteúdo desta edição foi traduzido do artigo da Wikipedia francês existente em fr: Machine de Krivine ; veja sua história para atribuição.
Bibliografia
- Jean-Louis Krivine: Uma máquina de cálculo lambda chamada por nome . Higher-Order and Symbolic Computation 20 (3): 199-207 (2007) archive .
- Curien, Pierre-Louis (1993). Combinadores categóricos, algoritmos sequenciais e funcionais (2ª ed.). Birkhaüser.
- Frédéric Lang: Explicando a máquina Krivine preguiçosa usando substituição e endereços explícitos . Arquivo de Higher-Order and Symbolic Computation 20 (3): 257-270 (2007) .
- Olivier Danvy (Ed.): Editorial da edição especial de Higher-Order and Symbolic Computation on the Krivine machine, vol. 20 (3) (2007)
links externos
-
Mídia relacionada à máquina Krivine no Wikimedia Commons
