Se você observar os combinadores recursivos no cálculo lambda sem tipo, como o combinador Y ou o combinador ômega: É claro que todos esses combinadores acabam duplicando uma variável em algum lugar de sua definição.
Além disso, todos esses combinadores são tipificáveis no cálculo lambda de tipo simples, se você o estender com tipos recursivos , onde α é permitido ocorrer negativamente no tipo recursivo.
No entanto, o que acontece se você adicionar tipos recursivos completos (ocorrência negativa) ao fragmento livre de exponencial da lógica linear (ou seja, MALL)?
Então você não tem um exponencial para lhe dar contração. Você pode codificar o tipo de exponencial usando algo como ! Um ≜ u ct . mas não vejo como definir a regra de introdução para ela, pois isso parece exigir um combinador de ponto fixo para definir. E eu estava tentando definir exponenciais, obter contração, obter um combinador de ponto fixo!
É o caso de o MALL e os tipos recursivos irrestritos ainda estarem normalizando‽
fonte
Respostas:
Se as comutações aditivas forem omitidas no MALL, é fácil mostrar que o tamanho de uma prova diminui a cada etapa de eliminação de corte. Se as comutações aditivas forem permitidas, a prova não é tão fácil, mas foi fornecida no artigo “Linear Logic” original. É chamado de Teorema da Normalização Pequena (Corolário 4.22, p71), que diz que enquanto a regra de contração-promoção não estiver envolvida (como é o caso do MALL), a normalização será mantida. O argumento não se baseia nas fórmulas, elas podem ser infinitas (por exemplo, definidas recursivamente).
fonte