Opis

• Tytuł:
  The Theory of an Arbitrary Higher \(\lambda\)-Model
• Twórca:
  Martínez-Rivillas, Daniel O.;
  de Queiroz, Ruy J. G. B.
• Współtwórca:
  Martínez-Rivillas, Daniel O. - Universidade Federal de Pernambuco, Centro de Informática, Av. Jornalista Aníbal Fernandes, s/n Recife, Pernambuco, Brazil;
  de Queiroz, Ruy J. G. B. - Universidade Federal de Pernambuco, Centro de Informática, Av. Jornalista Aníbal Fernandes, s/n Recife, Pernambuco, Brazil;
  Martínez-Rivillas, Daniel O. - domr@cin.ufpe.br;
  de Queiroz, Ruy J. G. B. - ruy@cin.ufpe.br
• Opis:
  One takes advantage of some basic properties of every homotopic \(\lambda\)-model (e.g. extensional Kan complex) to explore the higher \(\beta\eta\)-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 \(\lambda\)-terms, whose equality rules would be contained in the theory of any \(\lambda\)-homotopic model.
• Dostępność obiektu:
  Dostęp otwarty
• Prawa: https://creativecommons.org/licenses/by-nc-nd/4.0
• Data:
  2023.06.07;
  2023.04.25
• Typ:
  Other
• Język:
  angielski;
  eng
• Format:
  application/pdf
• Wydawca:
  Wydawnictwo Uniwersytetu Łódzkiego
• Relacja:
  Bulletin of the Section of Logic;1;
  52
• Temat i słowa kluczowe:
  higher lambda calculus;
  homotopic lambda model;
  Kan complex reflexive;
  higher conversion;
  homotopy type-free theory
• Identyfikator:
  0138-0680;
  http://hdl.handle.net/11089/47236 ;
  2449-836X;
  10.18778/0138-0680.2023.11
• Dostawca danych:
  Repozytorium Uniwersytetu Łódzkiego
• Czy mogę z tego obiektu skorzystać?:
  sprawdź warunki licencji
• Rodzaj zawartości:
  pozostałe