Typed lambda-calculi and superclasses of regular functions

L\^e Th\`anh D\~ung Nguy\^en

arxiv: 1907.00467 · v1 · pith:PCRTE4LNnew · submitted 2019-06-30 · 💻 cs.LO · cs.FL

Typed lambda-calculi and superclasses of regular functions

L\^e Th\`anh D\~ung Nguy\^en This is my paper

Pith reviewed 2026-05-25 11:58 UTC · model grok-4.3

classification 💻 cs.LO cs.FL

keywords Church encodingstyped lambda-calculusregular functionspolyregular functionstransductionselementary affine lambda-calculusimplicit computational complexity

0 comments

The pith

Typed lambda-calculi encode regular functions through Church encodings of strings and functions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proposes Church encodings inside typed lambda-calculi as a way to define classes of string-to-string and tree-to-tree transductions. It establishes inclusions showing that some transduction classes fall inside the functions computed by terms in these calculi. In particular, all regular functions receive encodings inside the elementary affine lambda-calculus. Adjusting the types of the programs considered yields encodings for a larger subclass of polyregular functions. The broader aim is to supply an automata-theoretic counterpart to implicit computational complexity.

Core claim

Church encodings of strings and their transformations inside typed lambda terms allow the elementary affine lambda-calculus to express exactly the regular functions; suitable changes to the types of the programs considered produce encodings for a strictly larger subclass of the polyregular functions.

What carries the argument

Church encodings of strings and transductions inside typed lambda-calculi, with the elementary affine variant as the central calculus.

Load-bearing premise

That Church encodings inside lambda terms faithfully represent the automata-theoretic behavior of the corresponding transductions.

What would settle it

A concrete regular function, such as the function that copies its input string, for which no term exists in the elementary affine lambda-calculus that realizes it under the Church encoding.

read the original 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 lambda-calculus, a variant of linear logic originally designed for implicit computational complexity.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper claims to encode regular functions into elementary affine lambda-calculus via Church encodings and to clarify simply-typed expressivity, but only the abstract is visible so the claims cannot be checked.

read the letter

This paper claims to encode regular functions into the elementary affine lambda-calculus using Church encodings, and to obtain a larger subclass of polyregular functions by changing the types of programs. It also states some inclusion results between transduction classes and lambda-calculus classes that address an open question on the expressivity of the simply typed lambda-calculus. The broader goal is to treat typed lambda-calculi as an automata-theoretic counterpart to implicit computational complexity, parallel to how monadic second-order logic works in descriptive complexity. The classes mentioned include polyregular functions, HDT0L transductions, and Sénizergues's k-computable mappings. What is new is the specific encoding claim for regular functions and the suggestion that varying types yields more polyregular power. The paper does well in laying out a clean motivation and naming the relevant transduction classes without overstatement. The soft spots are straightforward. Only the abstract is available, so there are no definitions of the encodings, no proof sketches, and no verification that the lambda terms actually compute the claimed transductions or match growth rates. The soundness is therefore low until the constructions are seen. The assumption that Church encodings will serve as a suitable basis for this counterpart is plausible on its face but needs the details to hold up. This work is aimed at people who already work across lambda-calculus, linear logic, and automata theory. A reader comfortable with both implicit complexity and transduction classes could extract value from the proposed framework if the encodings check out. It deserves a serious referee because the claims are specific enough to be tested against existing characterizations of regular and polyregular functions. I would recommend sending it to peer review so the technical parts can be examined.

Referee Report

0 major / 1 minor

Summary. The paper proposes using Church encodings within typed lambda-calculi as an automata-theoretic counterpart to implicit computational complexity, analogous to the role of monadic second-order logic in descriptive complexity. It focuses on transductions (string-to-string or tree-to-tree functions) with superlinear growth, including regular functions, polyregular functions, HDT0L transductions, and Sénizergues's k-computable mappings. The central results are inclusion theorems showing that certain transduction classes can be encoded in classes of programs definable in typed lambda-calculi; in particular, regular functions (and a larger subclass of polyregular functions obtained by varying program types) are encoded in the elementary affine lambda-calculus.

Significance. If the claimed encodings are correct and the inclusions hold, the work would establish a novel logical characterization of regular and polyregular transductions inside typed lambda-calculi, potentially resolving open questions about the expressivity of the simply typed lambda-calculus for computing functions. The approach leverages variants of linear logic originally developed for implicit computational complexity, offering a bridge between automata theory and type-theoretic complexity that could yield new decidability or complexity results for transduction classes.

minor comments (1)

The abstract mentions 'Sénizergues's k-computable mappings' but the provided text contains a typographical rendering issue with the accent and name; ensure consistent spelling and citation in the full manuscript.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their detailed summary of the paper and for recognizing its potential to connect typed lambda-calculi with transduction classes. The recommendation is marked 'uncertain,' but no specific major comments or criticisms were provided in the report. We are therefore unable to address any concrete points and stand ready to respond to any questions about the correctness of the encodings or proofs if they are raised.

Circularity Check

0 steps flagged

No significant circularity; derivation consists of direct inclusion proofs via encodings

full rationale

The paper's central results are inclusion theorems establishing that regular functions (and a subclass of polyregular functions) can be encoded into the elementary affine lambda-calculus via Church encodings. These are constructive proofs of expressivity, not statistical predictions, parameter fits, or renamings. No load-bearing step reduces by construction to its own inputs, and no self-citation chain is invoked to justify a uniqueness theorem or ansatz. The derivation is self-contained against the stated semantics of typed lambda-calculi and transduction classes.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract only; no concrete free parameters, axioms, or invented entities can be extracted. The central claim rests on the unstated assumption that the chosen encodings and type systems correctly capture the target transduction classes.

pith-pipeline@v0.9.0 · 5699 in / 1146 out tokens · 41843 ms · 2026-05-25T11:58:16.330404+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

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
IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

linearity appears in automata theory under the name copyless assignment

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.