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 $\lambda x.xxx$. Ele tem a seguinte regra de reescrita: para qualquer termo, $t$,

$(\mathbf {\lambda } x.xxx)t\rightarrow ttt$

Mas considere o que acontece quando aplicamos $\lambda x.xxx$ a si mesmo:

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

Portanto o termo $(\lambda x.xxx)(\lambda x.xxx)$ 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.

Ver também

• Cálculo lambda tipado
• Reescrita
• Programação funcional total
• Conjectura de Barendregt–Geuvers–Klop
• Lema de Newman