Propriedades de Normalização (reescrita abstrata)

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 se todos termos são normalizado fortemente; isto é, se todas as sequências reescritas eventualmente terminam em um termo na forma normal. Um sistema de reescrita também pode ter uma propriedade de normalização fraca, isto signfica que para cada termo, existe pelo menos uma sequência particular da reescrita que eventualmente conduz uma forma normal.

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

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

O Cálculo lambda sem categoria “puro” não satisfaz a propriedade forte da normalização, e nem mesmo a propriedade fraca de normalização. Considere o termo \lambda x . x x x. Ele tem a seguinte regra de reescrita: para qualquer termo, t,

(\mathbf{\lambda} x . x x x) t \rightarrow t t t

Mas considere o que acontece quando aplicamos \lambda x . x x x para si mesmo:

(\mathbf{\lambda} x . x x x) (\lambda x . x x x)  \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x)
  \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)
  \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)
\ldots\,

Portanto o termo (\lambda x . x x x) (\lambda x . x x x) não é uma normalização nem forte e nem fraca.

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

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

Um sistema de cálculo lambda com a propriedade de normalização pode ser vista como uma linguagem de programação com a propriedade que todo programa para. Embora esta seja uma propriedade muito útil, tem uma desvantagem: uma linguagem de programação com a propriedade de normalização não pode ser completude Turing. Isto significa que há funções computáveis que não podem ser definidas simplesmente tipando o cálculo lambda (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).