A 𝜆-model with ∞-groupoid structure based in the Scott’s 𝜆-model D∞

Abstract

The lambda calculus is a universal programming language that represents the functions computable from the point of view of the functions as a rule, that allow the evaluation of a function on any other function. This language can be seen as a theory, with certain pre-established axioms and inference rules, which can be represented by models. Dana Scott proposed the first non-trivial model of the extensional lambda calculus, known as 𝐷∞, in order to represent the 𝜆-terms as the typical functions of set theory, where it is not allowed to evaluate a function about itself. This thesis propose a construction of an ∞-groupoid from any lambda model endowed with a topology. We apply this construction for the particular case 𝐷∞ and we observe that the Scott topology does not provide relevant information about of the relation between higher equivalences. This motivates the search for a new line of research focused on the exploration of 𝜆-models with the structure of a non-trivial ∞-groupoid to generalize the proofs of term conversion (e.g., 𝛽-equality, 𝜂-equality) to higher proof in 𝜆-calculus.