Normalização de termos no cáculo dos combinadores

Abstract

Neste trabalho apresenta-se um estudo clássico do Cálculo dos Combinadores Não Tipado e Tipado e aborda-se ainda o Cálculo T de Gödel como uma extensão do Cálculo dos Combinadores Tipado. No Cálculo dos Combinadores Não Tipado prova-se que é válido o Teorema de Church-Rosser e que existem alguns resultados não decidíveis, como saber se um termo admite ou não forma normal. Para o Cálculo dos Combinadores Tipado mostra-se que também é válido o Teorema de Church-Rosser e que esta teoria satisfaz o Teorema da Normalização Forte. Prova-se que estes dois últimos Teoremas também são satisfeitos pelo Cálculo T de Gödel.

This thesis presents a classical study of the Untyped and Typed Combinatory Calculus; furthermore, it studies Gödel's T Calculus as an extension of the Typed Combinatory Calculus. Regarding the Untyped Combinatory Calculus, this work proves that the Church- Rosser Theorem is valid and some undecidability results (e.g., it is undecidable whether a term admits a normal form). As far as the Typed Combinatory Calculus is concerned, not only the Church- Rosser Theorem is valid but it also enjoys the propriety of Strong Normalization. This is also the case for Gödel's T Calculus. Herein, we prove these Theorems.