2019/06/13 by Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz, Martínez-Rivillas, Daniel O. +1
Computer Science · #68Q05 #Advanced Algebra and Logic #Algebraic Topology (math.AT) #Category Theory (math.CT) #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1906.05729
openalex publication_date 2019/06/13 · openalex created_date 2024/04/10 · openalex updated_date 2026/07/28
The lambda calculus is a universal programming language. It can represent the computable functions, and such offers a formal counterpart to the point of view of functions as rules. Terms represent functions and this allows for the application of a term/function to any other term/function, including itself. The calculus can be seen as a formal theory with certain pre-established axioms and inference rules, which can be interpreted by models. Dana Scott proposed the first non-trivial model of the extensional lambda calculus, known as D_∞, to represent the λ-terms as the typical functions of set theory, where it is not allowed to apply a function to itself. Here we propose a construction of an ∞-groupoid from any lambda model endowed with a topology. We apply this construction for the particular case D_∞, and we see that the Scott topology does not provide enough information about the relationship between higher homotopies. This motivates 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-proofs in λ-calculus.