Typed lambda-calculi and superclasses of regular functions
L\^e Th\`anh D\~ung Nguy\^en

TL;DR
This paper explores the use of typed lambda-calculi and Church encodings to characterize classes of string-to-string functions, including polyregular and regular functions, linking automata theory with lambda calculus for implicit computational complexity.
Contribution
It demonstrates the inclusion of certain transduction classes within lambda-calculus-based classes and encodes regular functions in the elementary affine lambda-calculus, advancing understanding of lambda-calculus expressivity.
Findings
Some transduction classes are included in lambda-calculus-defined classes.
Regular functions can be encoded in the elementary affine lambda-calculus.
The work sheds light on the expressivity of the simply typed lambda-calculus.
Abstract
We propose to use Church encodings in typed lambda-calculi as the basis for an automata-theoretic counterpart of implicit computational complexity, in the same way that monadic second-order logic provides a counterpart to descriptive complexity. Specifically, we look at transductions i.e. string-to-string (or tree-to-tree) functions - in particular those with superlinear growth, such as polyregular functions, HDT0L transductions and S\'enizergues's "k-computable mappings". Our first results towards this aim consist showing the inclusion of some transduction classes in some classes defined by lambda-calculi. In particular, this sheds light on a basic open question on the expressivity of the simply typed lambda-calculus. We also encode regular functions (and, by changing the type of programs considered, we get a larger subclass of polyregular functions) in the elementary affine…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Computability, Logic, AI Algorithms
