Implicit automata in typed $λ$-calculi II: streaming transducers vs categorical semantics
Lê Thành Dũng Nguyên, Camille Noûs, Cécilia Pradic
备注：
108 pages, 23 figures. Theorem 3.53 was wrong in previous versions. This is corrected and a more detailed proof is provided in a new appendix. Miscellaneous minor typos were also corrected
We characterize regular string transductions as programs in a linear $λ$-calculus with additives. One direction of this equivalence is proved by encoding copyless streaming string transducers (SSTs), which compute regular functions, into our $λ$-calculus. For the converse, we consider a categorical framework for defining automata and transducers over words, which allows us to relate register updates in SSTs to the semantics of the linear $λ$-calculus in a suitable monoidal closed category. To illustrate the relevance of monoidal closure to automata theory, we also leverage this notion to give abstract generalizations of the arguments showing that copyless SSTs may be determinized and that the composition of two regular functions may be implemented by a copyless SST. Our main result is then generalized from strings to trees using a similar approach. In doing so, we exhibit a connection between a feature of streaming tree transducers and the multiplicative/additive distinction of linear logic.
Keywords: MSO transductions, implicit complexity, Dialectica categories, Church encodings
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 lam…
On the topic of probabilistic rewriting, there are several works studying both termination and confluence of different systems. While working with a lambda calculus modelling quantum computation, we found a system with probabilistic rewriting rules and strongly normalizing terms. We examine the effect of small modifications in probabilistic rewriting, affine variables, and strategies on the overall confluence in this strongly normalizing probabilistic calculus.
Dependently typed lambda calculi such as the Logical Framework (LF) are capable of representing relationships between terms through types. By exploiting the "formulas-as-types" notion, such calculi can also encode the correspondence between formulas and their proofs in typing judgments. As such, these calculi provide a natural yet powerful means for specifying varied formal systems. Such specifications can be transformed into a more direct form that uses predicate formulas over simply typed lambda-terms and that thereby provides the basis for their animation using conventional logic programmin…
In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model of linear logic. We first define a simple, finite PCF-like lambda-calculus with booleans, and then we discuss two finite models, one based on finite sets and the other on finite vector spaces. The first model is shown to be fully complete with respect to the operational semantics of the language. The second model is not complete, but we develop an algebraic extension of the finite lambda calculus that recovers completeness. The relationship between the two semantics is describ…
Algebraic lambda-calculi have been studied in various ways, but their semantics remain mostly untouched. In this paper we propose a semantic analysis of a general simply-typed lambda-calculus endowed with a structure of vector space. We sketch the relation with two established vectorial lambda-calculi. Then we study the problems arising from the addition of a fixed point combinator and how to modify the equational theory to solve them. We sketch an algebraic vectorial PCF and its possible denotational interpretations.
The intuitionistic fragment of the call-by-name version of Curien and Herbelin's λ\_mu\_{mu}-calculus is isolated and proved strongly normalising by means of an embedding into the simply-typed lambda-calculus. Our embedding is a continuation-and-garbage-passing style translation, the inspiring idea coming from Ikeda and Nakazawa's translation of Parigot's λ\_mu-calculus. The embedding strictly simulates reductions while usual continuation-passing-style transformations erase permutative reduction steps. For our intuitionistic sequent calculus, we even only need "units of garbage" to be passed. …
Calculi with control operators have been studied to reason about control in programming languages and to interpret the computational content of classical proofs. To make these calculi into a real programming language, one should also include data types. As a step into that direction, this paper defines a simply typed call-by-value lambda calculus with the control operators catch and throw, a data type of lists, and an operator for primitive recursion (a la Goedel's T). We prove that our system satisfies subject reduction, progress, confluence for untyped terms, and strong normalization for wel…
In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inference rules. We propose an extension of the Curry-Howard paradigm of representation, from proofs to solutions: to represent solutions by possibly infinite terms of a dedicated lambda-calculus. This new, comprehensive approach to proof search is exemplified with the sequent calculus LJT for intuitionistic implication logic. A finitary representation is proposed, comprising lambda-terms extended with a formal greatest fix…
Fitch-style modal lambda calculi enable programming with necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator that is denoted by a lock. The addition of locks simplifies the formulation of typing rules for calculi that incorporate different modal axioms, but each variant demands different, tedious and seemingly ad hoc syntactic lemmas to prove normalization. In this work, we take a semantic approach to normalization, called normalization by evaluation (NbE), by leveraging the possible-world semantics of Fitch-style calculi to yield a more m…
Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that control resource consumption. Our main contribution is the source language, a new resource $λ$-calculus with non-determinism and failures, dubbed \ulamf. In \ulamf, resources are split into linear and unrestricted; failures are explicit and arise from this distinction. We define a type system based on intersection types to control resources and fail-prone computa…
Dependently typed lambda calculi such as the Edinburgh Logical Framework (LF) are a popular means for encoding rule-based specifications concerning formal syntactic objects. In these frameworks, relations over terms representing formal objects are naturally captured by making use of the dependent structure of types. We consider here the meaning-preserving translation of specifications written in this style into a predicate logic over simply typed λ-terms. Such a translation can provide the basis for efficient implementation and sophisticated capabilities for reasoning about specifications. We …
We define two extensions of the typed linear lambda-calculus that yield minimal Turing-complete systems. The extensions are based on unbounded recursion in one case, and bounded recursion with minimisation in the other. We show that both approaches are compatible with linearity and typeability constraints. Both extensions of the typed linear lambda-calculus are minimal, in the sense that taking out any of the components breaks the universality of the system. We discuss implementation techniques that exploit the linearity of the calculi. Finally, we apply the results to languages with fixpoint …
We present an approach to modeling computational calculi using higher category theory. Specifically we present a fully abstract semantics for the pi-calculus. The interpretation is consistent with Curry-Howard, interpreting terms as typed morphisms, while simultaneously providing an explicit interpretation of the rewrite rules of standard operational presentations as 2-morphisms. One of the key contributions, inspired by catalysis in chemical reactions, is a method of restricting the application of 2-morphisms interpreting rewrites to specific contexts.
In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a long standing issue. We derive from the semantics a set of typing rules for a simply-typed linear algebraic lambda-calculus, and show how it extends both to classical and quantum lambda-calculi.
We develop algebraic models of simple type theories, laying out a framework that extends universal algebra to incorporate both algebraic sorting and variable binding. Examples of simple type theories include the unityped and simply-typed $λ$-calculi, the computational $λ$-calculus, and predicate logic. Simple type theories are given models in presheaf categories, with structure specified by algebras of polynomial endofunctors that correspond to natural deduction rules. Initial models, which we construct, abstractly describe the syntax of simple type theories. Taking substitution structure into…
We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis.
Many calculi exist for modelling various features of object-oriented languages. Many of them are based on $λ$-calculus and focus either on statically typed class-based languages or dynamic prototype-based languages. We formalize untyped calculus of decorated objects, informally presented by Bugayenko, which is defined in terms of objects and relies on decoration as a primary mechanism of object extension. It is not based on $λ$-calculus, yet with only four basic syntactic constructions is just as complete. We prove the calculus is confluent (i.e. possesses Church-Rosser property), and introduc…
Fair termination is the property of programs that may diverge "in principle" but that terminate "in practice", i.e. under suitable fairness assumptions concerning the resolution of non-deterministic choices. We study a conservative extension of $μ$MALL$^\infty$, the infinitary proof system of the multiplicative additive fragment of linear logic with least and greatest fixed points, such that cut elimination corresponds to fair termination. Proof terms are processes of $π$LIN, a variant of the linear $π$-calculus with (co)recursive types into which binary and (some) multiparty sessions can be e…
