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

• Ano de defesa: 2020
• Autor(a) principal: MARTÍNEZ RIVILLAS, Daniel Orlando
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: Universidade Federal de Pernambuco; UFPE; Brasil; Programa de Pos Graduacao em Ciencia da Computacao
• Palavras-chave em Português: Teoria da computação; Cálculo lambda
• Link de acesso: https://repositorio.ufpe.br/handle/123456789/38554

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.