{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T20:03:04Z","timestamp":1776196984133,"version":"3.50.1"},"reference-count":24,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2021,4,16]],"date-time":"2021-04-16T00:00:00Z","timestamp":1618531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,5,21]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>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.<\/jats:p>","DOI":"10.1093\/jigpal\/jzab015","type":"journal-article","created":{"date-parts":[[2021,3,16]],"date-time":"2021-03-16T20:39:03Z","timestamp":1615927143000},"page":"465-488","source":"Crossref","is-referenced-by-count":6,"title":["\u221e-Groupoid Generated by an Arbitrary Topological \u03bb-Model"],"prefix":"10.1093","volume":"30","author":[{"given":"Daniel O","family":"Mart\u00ednez-Rivillas","sequence":"first","affiliation":[{"name":"Centro de Informatica (CIn) Universidade Federal de Pernambuco (UFPE) Av. Jorn. An\u00edbal Fernandes, s\/n - Cidade Universit\u00e1ria, 50740-560, Recife, PE, Brazil"}]},{"given":"Ruy J G B","family":"de Queiroz","sequence":"additional","affiliation":[{"name":"Centro de Informatica (CIn) Universidade Federal de Pernambuco (UFPE) Av. Jorn. An\u00edbal Fernandes, s\/n - Cidade Universit\u00e1ria, 50740-560, Recife, PE, Brazil"}]}],"member":"286","published-online":{"date-parts":[[2021,4,16]]},"reference":[{"key":"2022052312314009900_ref1","first-page":"1","article-title":"Topolog\u00eda de Scott para relaciones de preorden","author":"Acosta","year":"2002","journal-title":"Bolet\u00edn de Matem\u00e1ticas"},{"key":"2022052312314009900_ref2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0305004108001783","article-title":"Homotopy theoretic models of identity types","volume":"146","author":"Awodey","year":"2009","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"2022052312314009900_ref3","volume-title":"The Lambda Calculus, Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"2022052312314009900_ref4","doi-asserted-by":"crossref","first-page":"370","DOI":"10.1112\/plms\/pdq026","article-title":"Types are weak $\\omega $-groupoids","volume":"102","author":"Berg","year":"2011","journal-title":"Proceedings of the London Mathematical Society"},{"key":"2022052312314009900_ref5","doi-asserted-by":"crossref","DOI":"10.1090\/bull\/1616","article-title":"An introduction to univalent foundations for mathematicians","author":"Grayson","year":"2018"},{"key":"2022052312314009900_ref6","volume-title":"Lectures on Algebraic Topology","author":"Greenberg","year":"1967"},{"key":"2022052312314009900_ref7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-0346-0189-4","volume-title":"Simplicial Homotopy Theory","author":"Goerss","year":"2009"},{"key":"2022052312314009900_ref8","volume-title":"Algebraic Topology","author":"Hatcher","year":"2001"},{"key":"2022052312314009900_ref9","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809835","volume-title":"Lambda-Calculus and Combinators, An Introduction","author":"Hindley","year":"2008"},{"key":"2022052312314009900_ref10","first-page":"208","article-title":"The groupoid model refutes uniqueness of identity proof","author":"Hofmann","year":"1994","journal-title":"Logic and Computer Science"},{"key":"2022052312314009900_ref11","article-title":"The simplicial model of univalent foundations","author":"Kapulkin","year":"2012"},{"key":"2022052312314009900_ref12","article-title":"Higher operads, higher categories","author":"Leinster","year":"2003"},{"key":"2022052312314009900_ref13","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1017\/S030500411900015X","article-title":"Semantics of higher inductive types","volume":"169","author":"Lumsdaine","year":"2020","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"2022052312314009900_ref14","article-title":"An intuitionistic theory of types: predicative part","volume-title":"Logic Colloquium\u201973","author":"Martin-L\u00f6f","year":"1973"},{"key":"2022052312314009900_ref15","volume-title":"A Concise Course in Algebraic Topology","author":"May","year":"1999"},{"key":"2022052312314009900_ref16","article-title":"Towards a homotopy domain theory","author":"Mart\u00ednez","year":"2020"},{"key":"2022052312314009900_ref17","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Program","year":"2013"},{"key":"2022052312314009900_ref18","first-page":"245","volume-title":"South American Journal of Logic","author":"de Queiroz","year":"2016"},{"key":"2022052312314009900_ref19","doi-asserted-by":"crossref","first-page":"562","DOI":"10.1093\/jigpal\/jzx015","article-title":"On the identity type as the type of computational paths","volume":"25","author":"Ramos","year":"2017","journal-title":"Logic Journal of the IGPL"},{"key":"2022052312314009900_ref20","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1016\/0304-3975(93)90095-B","article-title":"A type-theoretical alternative to ISWIM, CUCH, OWHY","volume":"121","author":"Scott","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"2022052312314009900_ref21","article-title":"An alternative approach to the calculation of fundamental groups based on labeled natural deduction","author":"Veras","year":"2019"},{"key":"2022052312314009900_ref22","article-title":"A topological application of labelled natural deduction","author":"Veras","year":"2019"},{"key":"2022052312314009900_ref23","article-title":"Computational paths\u2014a weak groupoid","author":"Veras","year":"2020"},{"key":"2022052312314009900_ref24","article-title":"The equivalence axiom and univalent models of type theory","author":"Voevodsky","year":"2010"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/30\/3\/465\/43781601\/jzab015.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/30\/3\/465\/43781601\/jzab015.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T12:32:17Z","timestamp":1653309137000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/30\/3\/465\/6225563"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,16]]},"references-count":24,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2021,4,16]]},"published-print":{"date-parts":[[2022,5,21]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzab015","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2022,6]]},"published":{"date-parts":[[2021,4,16]]}}}