Quantitative Weak Linearisation

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2022

Autores

Sandra Alves (Autor) FCUP; Ventura, D (Autor) Outra

Ata de Conferência Internacional

Título: Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings

Páginas: 78-95

19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022

27 September 2022 through 29 September 2022

Indexação

ISI Proceedings

Scopus

Outras Informações

ID Authenticus: P-00X-86Z

DOI: 10.1007/978-3-031-17715-6_7

Abstract (EN): Weak linearisation was defined years ago through a static characterization of the intuitive notion of virtual redex, based on (legal) paths computed from the (syntactical) term tree. Weak-linear terms impose a linearity condition only on functions that are applied (consumed by reduction) and functions that are not applied (therefore persist in the term along any reduction) can be non-linear. This class of terms was shown to be strongly normalising with deciding typability in polynomial time. We revisit this notion through non-idempotent intersection types (also called quantitative types). By using an effective characterisation of minimal typings, based on the notion of tightness, we are able to distinguish between ¿consumed¿ and ¿persistent¿ term constructors, which allows us to define an expansion relation, between general ¿ -terms and weak-linear ¿ -terms, whilst preserving normal forms by reduction. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Idioma: Inglês

Tipo (Avaliação Docente): Científica