Implicit automata in typed λ-calculi (I, II and III)

In the past few years, Cécilia Pradic and I have been pursuing a research programme aimed at uncovering connections of the form: "the languages/functions recognized by some flavor A of automata are exactly those definable in some typed λ-calculus P, using a certain input/output convention". λ-calculi are minimalistic functional programming languages, and type systems have been used to achieve interesting restrictions on their expressive power in a field called implicit computational complexity – hence the title. The I/O conventions that we use are based on Church encodings, whose connections with automata theory have been leveraged in higher-order model checking (HOMC). Our main inspiration is a result of Hillebrand and Kanellakis (1996): A = regular languages, P = simply typed λ-calculus. We have managed to characterize star-free languages, regular tree functions (in a similar fashion to Gallot, Lemay & Salvati 2020) and comparison-free polyregular functions (a class whose introduction was motivated by our work on λ-calculi!) using type systems based on linear logic (a programming language counterpart of various "copyless" or "single use" restrictions in automata theory). These developments, and the semantic/category-theoretic tools that they involve, are recapitulated in the longer abstract https: //cs-web. swan. ac. uk/~cpradic/smp-abstract. pdfMore recently, I have devised a transducer model, based on the collapsible pushdown automata used in HOMC, that captures the tree-to-tree functions computable by simply typed λ-terms, thus answering a question going back at least to the 1980s. This work can also be seen as a revival of Engelfriet and Vogler's investigations into "high level tree transducers", also in the 1980s. Contributed talk given by Le Thanh Dung NGUYEN

Authors

• Le Thanh Dung NGUYEN

Keywords

No keywords are indexed for this paper.