W dniach od 2 kwietnia do 5 kwietnia 2024 r. prowadzone będą prace związane z wdrożeniem nowej wersji systemu Repozytorium UJ. Nie będzie możliwe wprowadzanie nowych informacji do repozytorium. Za utrudnienia przepraszamy.
λν is an extension of the λ-calculus which internalises the calculus of substitutions. In the current paper, we investigate the combinatorial properties of λν focusing on the quantitative aspects of substitution resolution. We exhibit an unexpected correspondence between the counting sequence for λν-terms and famous Catalan numbers. As a by-product, we establish effective sampling schemes for random λν-terms. We show that typical λν-terms represent, in a strong sense, non-strict computations in the classic X-calculus. Moreover, typically almost all substitutions are in fact suspended, i.e. unevaluated, under closures. Consequently, we argue that λν is an intrinsically non-strict calculus of explicit substitutions. Finally, we investigate the distribution of various redexes governing the substitution resolution in λν and investigate the quantitative contribution of various substitution primitives.
liczba arkuszy wydawniczych:
0,81
konferencja:
PPDP '18 Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming; 2018-09-03; 2018-09-05; Frankfurt; Niemcy; ; indeksowana w Scopus; ; PPDP;
wydział: instytut / zakład / katedra:
Wydział Matematyki i Informatyki : Zespół Katedr i Zakładów Informatyki Matematycznej
typ:
artykuł (rozdział) w książce
podtyp:
publikacja pokonferencyjna
Pliki tej pozycji
Plik
Rozmiar
Format
Przeglądanie
Nie ma plików powiązanych z tą pozycją.
Pozycja umieszczona jest w następujących kolekcjach