∞-Groupoid Generated by an Arbitrary Topological λ-Model. (16th April 2021)

• Record Type: Journal Article
• Authors: Martínez-Rivillas, Daniel O; de Queiroz, Ruy J G B
• Is Part Of: Logic journal of the IGPL. Volume 30:Number 3(2022)
• Page Start: 465
• Page End: 488
• Publication Date: 2021-04-16
• Subjects: lambda calculus -- lambda model -- infinity groupoid -- homotopy -- Scott topology; Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1093/jigpal/jzab015
• Languages: English
• ISSNs: 1367-0751

Abstract

Abstract: 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_{\infty }$, to represent the $\lambda $ -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 $\infty $ -groupoid from any lambda model endowed with a topology. We apply this construction for the particular case $D_{\infty }$, 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 $\lambda $ -models with the structure of a non-trivial $\infty $ -groupoid to generalize the proofs of term conversion (e.g., $\beta $ -equality, $\eta $ -equality) to higher-proofs in $\lambda $ -calculus.