Teoría de tipos con funciones parciales

Abstract

En este trabajo se estudia la teoría de tipos con funciones parciales. Para llevar a cabo este estudio, se completa un amplio recorrido. El trabajo parte del contexto en el que nace la teoría de tipos y con qué propositos. Seguidamente se exponen los sistemas de teoría de tipos Q0, Alonzo, PF y LUTINS, de los cuales los tres últimos incluyen funciones parciales. La presentación de los fundamentos de cada sistema permite compararlos y analizar su adecuación para la formalización de las matemáticas y la implementación en computación. Finalmente, se concluye que la teoría de tipos, especialmente con funciones parciales, presenta múltiples ventajas en estos ámbitos. Por este motivo, se presenta también una propuesta pedagógica para la incorporación de la teoría de tipos en la educación general y en las carreras ligadas a las matemáticas aplicadas y computación.

In this project type theory with partial functions is studied. To carry out this investigation, an extensive journey is completed. The work starts from the context in which type theory was born and for what purposes. Next, the type theory systems Q0, Alonzo, PF and LUTINS are presented, the last three including partial functions. The presentation of the fundamentals of each system allows to compare them and analyze their suitability for the formalization of mathematics and implementation in computing. Finally, it is concluded that type theory, especially with partial functions, has multiple advantages in these areas. For this reason, a pedagogical proposal is also presented for the incorporation of type theory to general education and careers linked to applied mathematics and computing.