-
The Theory of an Arbitrary Higher $λ$-Model
Authors:
Daniel O. Martínez-Rivillas,
Ruy J. G. B. de Queiroz
Abstract:
One takes advantage of some basic properties of every homotopic $λ$-model (e.g.\ extensional Kan complex) to explore the higher $βη$-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher $λ$-terms, whose equality rules would be…
▽ More
One takes advantage of some basic properties of every homotopic $λ$-model (e.g.\ extensional Kan complex) to explore the higher $βη$-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher $λ$-terms, whose equality rules would be contained in the theory of any $λ$-homotopic model.
△ Less
Submitted 26 April, 2023; v1 submitted 13 November, 2021;
originally announced November 2021.
-
Solving Homotopy Domain Equations
Authors:
Daniel O. Martínez-Rivillas,
Ruy J. G. B. de Queiroz
Abstract:
In order to get $λ$-models with a rich structure of $\infty$-groupoid, which we call "homotopy $λ$-models", a general technique is described for solving domain equations on any cartesian closed $\infty$-category (c.c.i.) with enough points. Finally, the technique is applied in a particular c.c.i., where some examples of homotopy $λ$-models are given.
In order to get $λ$-models with a rich structure of $\infty$-groupoid, which we call "homotopy $λ$-models", a general technique is described for solving domain equations on any cartesian closed $\infty$-category (c.c.i.) with enough points. Finally, the technique is applied in a particular c.c.i., where some examples of homotopy $λ$-models are given.
△ Less
Submitted 9 September, 2022; v1 submitted 2 April, 2021;
originally announced April 2021.
-
Towards a Homotopy Domain Theory
Authors:
Daniel O. Martínez-Rivillas,
Ruy J. G. B. de Queiroz
Abstract:
An appropriate framework is put forward for the construction of $λ$-models with $\infty$-groupoid structure, which we call \textit{homotopic $λ$-models}, through the use of an $\infty$-category with cartesian closure and enough points. With this, we establish the start of a project of generalization of Domain Theory and $λ$-calculus, in the sense that the concept of proof (path) of equality of…
▽ More
An appropriate framework is put forward for the construction of $λ$-models with $\infty$-groupoid structure, which we call \textit{homotopic $λ$-models}, through the use of an $\infty$-category with cartesian closure and enough points. With this, we establish the start of a project of generalization of Domain Theory and $λ$-calculus, in the sense that the concept of proof (path) of equality of $λ$-terms is raised to \textit{higher proof} (homotopy).
△ Less
Submitted 26 October, 2022; v1 submitted 29 July, 2020;
originally announced July 2020.
-
The $\infty$-groupoid generated by an arbitrary topological $λ$-model
Authors:
Daniel O. Martínez-Rivillas,
Ruy J. G. B. de Queiroz
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 inferenc…
▽ More
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 $λ$-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 $λ$-models with the structure of a non-trivial $\infty$-groupoid to generalize the proofs of term conversion (e.g., $β$-equality, $η$-equality) to higher-proofs in $λ$-calculus.
△ Less
Submitted 17 January, 2021; v1 submitted 13 June, 2019;
originally announced June 2019.
