Como tornar o Lambda Calculus forte normalizando sem um sistema de tipos?

Existe algum sistema semelhante ao cálculo lambda com forte normalização, sem a necessidade de adicionar um sistema de tipos sobre ele?

Eu posso pensar em algumas respostas possíveis provenientes da lógica linear.

O mais simples é o cálculo lambda afim: considere apenas termos lambda nos quais todas as variáveis ​​aparecem no máximo uma vez. Essa condição é preservada pela redução e é imediato ver que o tamanho dos termos afins diminui estritamente a cada etapa de redução. Portanto, o cálculo lambda afinado não tipado está fortemente normalizando.

Exemplos mais interessantes (em termos de expressividade) são dados pelos chamados lambda-calculi "leves", decorrentes dos subsistemas de lógica linear introduzidos por Girard em "Light Linear Logic" (Information and Computation 143, 1998), também como "Soft Linear Logic" de Lafont (Teoria da Computação 318, 2004). Existem vários cálculos na literatura, talvez uma boa referência seja a normalização forte de Terui "Light affine lambda cálculo e tempo polinomial" (Archive for Mathematics Logic 46, 2007). Nesse artigo, Terui define um cálculo lambda derivado da lógica afim da luz e prova um forte resultado de normalização para ele. Embora os tipos sejam mencionados no artigo, eles não são usados ​​na prova de normalização. Eles são úteis para uma formulação clara da propriedade principal do cálculo lambda afim da luz, ou seja, que os termos de um determinado tipo representam exatamente as funções Polytime. Resultados semelhantes são conhecidos para computação elementar, usando outros cálculos lambda "leves" (o artigo de Terui contém outras referências).

Como observação lateral, é interessante observar que, em termos teóricos da prova, o cálculo lambda afim corresponde à lógica intuicionista sem a regra da contração. Grishin observou (antes da introdução da lógica linear) que, na ausência de contração, a teoria dos conjuntos ingênua (isto é, com compreensão irrestrita) é consistente (isto é, o paradoxo de Russel não dá uma contradição). A razão é que a eliminação de cortes para a teoria dos conjuntos ingênua sem contração pode ser comprovada por um argumento direto de redução de tamanho (como o que forneci acima) que não depende da complexidade das fórmulas. Através da correspondência de Curry-Howard, essa é exatamente a normalização do cálculo lambda afinado não tipado. É traduzindo o paradoxo de Russel na lógica linear e "aprimorando" as modalidades exponenciais para que nenhuma contradição pudesse ser derivada de que Girard inventou uma lógica linear leve. Como mencionei acima, em termos computacionais, a lógica linear leve fornece uma caracterização das funções computáveis ​​em tempo polinomial. Em termos teóricos da prova, uma teoria ingênua consistente dos conjuntos pode ser definida na lógica linear da luz, de modo que as funções comprovadamente totais sejam exatamente as funções computáveis ​​em tempo polinomial (há outro artigo de Terui sobre isso, "Teoria dos conjuntos afins da luz: uma ingênua teoria dos conjuntos do tempo polinomial ", Studia Logica 77, 2004).

O artigo original de Church e Rosser, "Some Properties of Conversion", descreve algo que pode ser um exemplo do que você está procurando.

Se você usar o cálculo lambda estrito , em que em toda ocorrência de você tem que aparece livre em , sem um sistema de tipos a seguinte propriedade é válida (é o Teorema 2 no artigo de Church e Rosser):$\lambda x.M$$x$$M$

Se é uma forma normal de , existe um número tal que qualquer sequência de reduções iniciando em levará a [equivalência alfa do módulo] após, no máximo, reduções.$B$$A$$m$$A$$B$$m$

Assim, mesmo que você possa escrever termos não termináveis ​​no cálculo lambda estrito (sem tipo), todo termo com uma forma normal normaliza fortemente; isto é, toda sequência de reduções alcançará essa forma normal única.

Aqui está uma divertida, de Neil Jones e Nina Bohr:

Terminação de chamada por valor no Untype$\lambda$

Ele mostra como aplicar a análise de mudança de tamanho (um tipo de análise de fluxo de controle que detecta loops infinitos) em termos tipda . Isso é bastante bom na prática, mas é claro que está restrito a -terms sem constantes definidas (embora o método possa ser estendido para uso mais geral).$\lambda$$\lambda$

A vantagem da digitação, é claro, é o baixo custo de complexidade e a modularidade da abordagem: em geral, as análises de terminação são muito não modulares, mas a digitação pode ser feita "peça por peça".