Mostrar código-fonte de Propriedades de normalização forte e fraca

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==
=== Cálculo lambda não tipado ===
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 <math>\lambda x . x x x</math>. Ele tem a seguinte regra de reescrita: para qualquer termo, <math>t</math>,

: <math>(\mathbf{\lambda} x . x x x) t \rightarrow t t t</math>

Mas considere o que acontece quando aplicamos <math>\lambda x . x x x</math> a si mesmo:
{|
| <math>(\mathbf{\lambda} x . x x x) (\lambda x . x x x)</math>
| <math> \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math>  \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math>  \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)</math>
|-
|
| <math>\ldots\,</math>
|}

Portanto o termo  <math>(\lambda x . x x x) (\lambda x . x x x)</math> não é nem fortemente nem fracamente normalizante.

=== Cálculo lambda tipado ===

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.<ref>Conor McBride (May 2003), [http://www.haskell.org/pipermail/haskell-cafe/2003-May/004343.html "on termination"] (posted to the Haskell-Cafe mailing list).</ref>

==Ver também==
* [[Cálculo lambda tipado]]
* [[Reescrita]]
* [[Programação funcional total]]
* [[Conjectura de Barendregt–Geuvers–Klop]]
* [[Lema de Newman]]

{{Referências}}



[[Categoria:Lógica matemática]]
[[Categoria:Ciências formais]]