FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Combinatorics of explicit substitutions (extended abstract)

Authors: Maciej Bendkowski and Pierre Lescanne

Paper Information

Title:Combinatorics of explicit substitutions (extended abstract)
Authors:Maciej Bendkowski and Pierre Lescanne
Proceedings:HOR Pre-proceedings
Editor: Stefano Guerrini
Keywords:explicit substitution, combinatorics, Catalan numbers, random generation
Abstract:

ABSTRACT. lambda-upsilon is an extension of the lambda-calculus which internalises the calculus of substitutions. In the current paper, we investigate the combinatorial properties of lambda-upsilon focusing on the quantitative aspects of substitution resolution. We exhibit an unexpected correspondence between the counting sequence for lambda-upsilon terms and famous Catalan numbers. As a by-product, we establish effective sampling schemes for random lambda-upsilon terms. We show that typical lambda-upsilon terms represent, in a strong sense, non-strict computations in the classic lambda-calculus. Moreover, typically almost all substitutions are in fact suspended, i.e., unevaluated, under closures. Consequently, we argue that lambda-upsilon is an intrinsically non-strict calculus of explicit substitutions. Finally, we investigate the distribution of various redexes governing the substitution resolution in lambda-upsilon and investigate the quantitative contribution of various substitution primitives.

Pages:6
Talk:Jul 07 10:00 (Session 25)
Paper: