-
Views
-
Cite
Cite
Daniel O Martínez-Rivillas, Ruy J G B de Queiroz, ∞-Groupoid Generated by an Arbitrary Topological λ-Model, Logic Journal of the IGPL, Volume 30, Issue 3, June 2022, Pages 465–488, https://doi.org/10.1093/jigpal/jzab015
Close - Share Icon Share
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.
