2019/06/30 by Lê Thành Dũng Nguyễn, Nguyên, Lê Thành Dũng
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1907.00467
openalex publication_date 2019/06/30 · openalex created_date 2019/07/12 · openalex updated_date 2026/07/28
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énizergues'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 lambda-calculus, a variant of linear logic originally designed for implicit computational complexity.