Propriedades de normalização forte e fraca

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

Na matemática lógica e ciência da computação teórica, um Sistema de Reescrita tem a propriedade de normalização forte ou é terminante (brevemente: a propriedade da normalização ou da terminação) se todos termos são fortemente normalizantes; isto é, se todas as sequências de reescrita eventualmente terminam em um termo irredutível também chamado de forma normal. Um sistema de reescrita também pode ter a propriedade de normalização fraca, isto significa que para cada termo, existe pelo menos uma sequência específica de reescrita que eventualmente conduz a uma forma normal, i.e. a um termo irredutível.

Cálculo lambda[editar | editar código-fonte]

Cálculo lambda não tipado[editar | editar código-fonte]

O Cálculo lambda puro não-tipado não satisfaz a propriedade da normalização forte, e nem mesmo a propriedade da normalização fraca. Considere o termo . Ele tem a seguinte regra de reescrita: para qualquer termo, ,

Mas considere o que acontece quando aplicamos a si mesmo:

Portanto o termo não é nem fortemente nem fracamente normalizante.

Cálculo lambda tipado[editar | editar código-fonte]

Vários sistemas de cálculo lambda tipado incluindo o cálculo lambda simplesmente tipado, o Sistema F de Jean-Yves Girard, e o cálculo de construções de Thierry Coquand, são fortemente normalizantes.

Um sistema de cálculo lambda com a propriedade da normalização pode ser visto como uma linguagem de programação com a propriedade de que todo programa para. Embora esta seja uma propriedade muito útil, há uma desvantagem: uma linguagem de programação com a propriedade de normalização não pode ser Turing-completa. Isto significa que há funções computáveis que não podem ser definidas simplesmente usando o cálculo lambda simplesmente tipado (de forma similar, há funções computáveis que não podem ser calculadas, no cálculo das construções ou Sistema F). Por exemplo, é impossível definir um auto-interpretador em qualquer um dos cálculos citados acima.[1]

Ver também[editar | editar código-fonte]

Referências

  1. Conor McBride (May 2003), "on termination" (posted to the Haskell-Cafe mailing list).