-
An Introduction to Different Approaches to Initial Semantics
Authors:
Thomas Lamiaux,
Benedikt Ahrens
Abstract:
Characterizing programming languages with variable binding as initial objects, was first achieved by Fiore, Plotkin, and Turi in their seminal paper published at LICS'99. To do so, in particular to prove initiality theorems, they developed a framework based on monoidal categories, functors with strengths, and $Σ$-monoids. An alternative approach using modules over monads was later introduced by Hi…
▽ More
Characterizing programming languages with variable binding as initial objects, was first achieved by Fiore, Plotkin, and Turi in their seminal paper published at LICS'99. To do so, in particular to prove initiality theorems, they developed a framework based on monoidal categories, functors with strengths, and $Σ$-monoids. An alternative approach using modules over monads was later introduced by Hirschowitz and Maggesi, for endofunctor categories, that is, for particular monoidal categories. This approach has the advantage of providing a more general and abstract definition of signatures and models; however, no general initiality result is known for this notion of signature. Furthermore, Matthes and Uustalu provided a categorical formalism for constructing (initial) monads via Mendler-style recursion, that can also be used for initial semantics. The different approaches have been developed further in several articles. However, in practice, the literature is difficult to access, and links between the different strands of work remain underexplored.
In the present work, we give an introduction to initial semantics that encompasses the three different strands. We develop a suitable "pushout" of Hirschowitz and Maggesi's framework with Fiore's, and rely on Matthes and Uustalu's formalism to provide modular proofs. For this purpose, we generalize both Hirschowitz and Maggesi's framework, and Matthes and Uustalu's formalism to the general setting of monoidal categories studied by Fiore and collaborators. Moreover, we provide fully worked out presentation of some basic instances of the literature, and an extensive discussion of related work explaining the links between the different approaches.
△ Less
Submitted 17 January, 2024;
originally announced January 2024.
-
Univalent Double Categories
Authors:
Niels van der Weide,
Nima Rasekh,
Benedikt Ahrens,
Paige Randall North
Abstract:
Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for examp…
▽ More
Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for example in functional programming. Double categories are a natural generalization of categories which incorporate the data of two separate classes of morphisms, allowing a more nuanced representation of relationships and interactions between objects. Similar to category theory, double categories have been successfully applied to various situations in mathematics and computer science, in which objects naturally exhibit two types of morphisms. Examples include categories themselves, but also lenses, petri nets, and spans. While categories have already been formalized in a variety of proof assistants, double categories have received far less attention. In this paper we remedy this situation by presenting a formalization of double categories via the proof assistant Coq, relying on the Coq UniMath library. As part of this work we present two equivalent formalizations of the definition of a double category, an unfolded explicit definition and a second definition which exhibits excellent formal properties via 2-sided displayed categories. As an application of the formal approach we establish a notion of univalent double category along with a univalence principle: equivalences of univalent double categories coincide with their identities
△ Less
Submitted 13 October, 2023;
originally announced October 2023.
-
Substitution for Non-Wellfounded Syntax with Binders through Monoidal Categories
Authors:
Ralph Matthes,
Kobe Wullaert,
Benedikt Ahrens
Abstract:
We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation. Our construction of the syntax and its substitution takes place in category theory, notably by using monoidal categories and strong functors between them. A language is specified by a multi-sorted binding signature, say Σ. First, we provide sufficient criteria for Σ to ge…
▽ More
We describe a generic construction of non-wellfounded syntax involving variable binding and its monadic substitution operation. Our construction of the syntax and its substitution takes place in category theory, notably by using monoidal categories and strong functors between them. A language is specified by a multi-sorted binding signature, say Σ. First, we provide sufficient criteria for Σ to generate a language of possibly infinite terms, through ω-continuity. Second, we construct a monadic substitution operation for the language generated by Σ. A cornerstone in this construction is a mild generalization of the notion of heterogeneous substitution systems developed by Matthes and Uustalu; such a system encapsulates the necessary corecursion scheme for implementing substitution. The results are formalized in the Coq proof assistant, through the UniMath library of univalent mathematics.
△ Less
Submitted 7 May, 2024; v1 submitted 10 August, 2023;
originally announced August 2023.
-
Formalizing Monoidal Categories and Actions for Syntax with Binders
Authors:
Benedikt Ahrens,
Ralph Matthes,
Kobe Wullaert
Abstract:
We discuss some aspects of our work on the mechanization of syntax and semantics in the UniMath library, based on the proof assistant Coq. We focus on experiences where Coq (as a type-theoretic proof assistant with decidable typechecking) made us use more theory or helped us to see theory more clearly.
We discuss some aspects of our work on the mechanization of syntax and semantics in the UniMath library, based on the proof assistant Coq. We focus on experiences where Coq (as a type-theoretic proof assistant with decidable typechecking) made us use more theory or helped us to see theory more clearly.
△ Less
Submitted 7 October, 2023; v1 submitted 30 July, 2023;
originally announced July 2023.
-
Univalent Monoidal Categories
Authors:
Kobe Wullaert,
Ralph Matthes,
Benedikt Ahrens
Abstract:
Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study them in a univalent setting. Specifically, we show that the bicategory of univalent monoidal categories is univalent. Furt…
▽ More
Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study them in a univalent setting. Specifically, we show that the bicategory of univalent monoidal categories is univalent. Furthermore, we construct a Rezk completion for monoidal categories: we show how any monoidal category is weakly equivalent to a univalent monoidal category, universally. We have fully formalized these results in UniMath, a library of univalent mathematics in the Coq proof assistant.
△ Less
Submitted 19 May, 2023; v1 submitted 6 December, 2022;
originally announced December 2022.
-
Category Theory for Programming
Authors:
Benedikt Ahrens,
Kobe Wullaert
Abstract:
In these lecture notes, we give a brief introduction to some elements of category theory. The choice of topics is guided by applications to functional programming. Firstly, we study initial algebras, which provide a mathematical characterization of datatypes and recursive functions on them. Secondly, we study monads, which give a mathematical framework for effects in functional languages. The note…
▽ More
In these lecture notes, we give a brief introduction to some elements of category theory. The choice of topics is guided by applications to functional programming. Firstly, we study initial algebras, which provide a mathematical characterization of datatypes and recursive functions on them. Secondly, we study monads, which give a mathematical framework for effects in functional languages. The notes include many problems and solutions.
△ Less
Submitted 2 September, 2022;
originally announced September 2022.
-
Univalent foundations and the equivalence principle
Authors:
Benedikt Ahrens,
Paige Randall North
Abstract:
In this paper, we explore the 'equivalence principle' (EP): roughly, statements about mathematical objects should be invariant under an appropriate notion of equivalence for the kinds of objects under consideration. In set theoretic foundations, EP may not always hold: for instance, the statement '1 \in N' is not invariant under isomorphism of sets. In univalent foundations, on the other hand, EP…
▽ More
In this paper, we explore the 'equivalence principle' (EP): roughly, statements about mathematical objects should be invariant under an appropriate notion of equivalence for the kinds of objects under consideration. In set theoretic foundations, EP may not always hold: for instance, the statement '1 \in N' is not invariant under isomorphism of sets. In univalent foundations, on the other hand, EP has been proven for many mathematical structures. We first give an overview of earlier attempts at designing foundations that satisfy EP. We then describe how univalent foundations validates EP.
△ Less
Submitted 3 February, 2022;
originally announced February 2022.
-
Bicategorical type theory: semantics and syntax
Authors:
Benedikt Ahrens,
Paige Randall North,
Niels van der Weide
Abstract:
We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by develo** the semantics, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; we study both specific…
▽ More
We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by develo** the semantics, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.
△ Less
Submitted 12 October, 2023; v1 submitted 25 January, 2022;
originally announced January 2022.
-
The solutions to single-variable polynomials, implemented and verified in Lean
Authors:
Nicholas Dyson,
Benedikt Ahrens,
Jacopo Emmenegger
Abstract:
In this work, we describe our experience in learning the use of a computer proof assistant - specifically, Lean - from scratch, through proving formulae for the solutions of polynomial equations. Specifically, in this work we characterize the solutions of quadratic, cubic, and quartic polynomials over certain fields, specifically, fields with operations returning square and cubic roots of characte…
▽ More
In this work, we describe our experience in learning the use of a computer proof assistant - specifically, Lean - from scratch, through proving formulae for the solutions of polynomial equations. Specifically, in this work we characterize the solutions of quadratic, cubic, and quartic polynomials over certain fields, specifically, fields with operations returning square and cubic roots of characteristic other than two or three. The purpose of this work is thus twofold. Firstly, it describes the learning experience of a starting Lean user, including a detailed comparison between our work in Lean and very closely related work in Coq. Secondly, our results represent a modest improvement over the aforementioned related work in Coq, which we hope will be of some scientific interest.
△ Less
Submitted 1 January, 2022;
originally announced January 2022.
-
Implementing a Category-Theoretic Framework for Typed Abstract Syntax
Authors:
Benedikt Ahrens,
Ralph Matthes,
Anders Mörtberg
Abstract:
In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant.
In the present work, we describe what was necessary to generalize that work to account for simply-typed languages. First, some definitions had to be generalized to account for the natural…
▽ More
In previous work ("From signatures to monads in UniMath"), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof assistant.
In the present work, we describe what was necessary to generalize that work to account for simply-typed languages. First, some definitions had to be generalized to account for the natural appearance of non-endofunctors in the simply-typed case. As it turns out, in many cases our mechanized results carried over to the generalized definitions without any code change. Second, an existing mechanized library on $ω$-cocontinuous functors had to be extended by constructions and theorems necessary for constructing multi-sorted syntax. Third, the theoretical framework for the semantical signatures had to be generalized from a monoidal to a bicategorical setting, again to account for non-endofunctors arising in the typed case. This uses actions of endofunctors on functors with given source, and the corresponding notion of strong functors between actions, all formalized in UniMath using a recently developed library of bicategory theory. We explain what needed to be done to plug all of these ingredients together, modularly.
The main result of our work is a general construction that, when fed with a signature for a simply-typed language, returns an implementation of that language together with suitable boilerplate code, in particular, a certified monadic substitution operation.
△ Less
Submitted 13 December, 2021;
originally announced December 2021.
-
FourierNets enable the design of highly non-local optical encoders for computational imaging
Authors:
Diptodip Deb,
Zhenfei Jiao,
Ruth Sims,
Alex B. Chen,
Michael Broxton,
Misha B. Ahrens,
Kaspar Podgorski,
Srinivas C. Turaga
Abstract:
Differentiable simulations of optical systems can be combined with deep learning-based reconstruction networks to enable high performance computational imaging via end-to-end (E2E) optimization of both the optical encoder and the deep decoder. This has enabled imaging applications such as 3D localization microscopy, depth estimation, and lensless photography via the optimization of local optical e…
▽ More
Differentiable simulations of optical systems can be combined with deep learning-based reconstruction networks to enable high performance computational imaging via end-to-end (E2E) optimization of both the optical encoder and the deep decoder. This has enabled imaging applications such as 3D localization microscopy, depth estimation, and lensless photography via the optimization of local optical encoders. More challenging computational imaging applications, such as 3D snapshot microscopy which compresses 3D volumes into single 2D images, require a highly non-local optical encoder. We show that existing deep network decoders have a locality bias which prevents the optimization of such highly non-local optical encoders. We address this with a decoder based on a shallow neural network architecture using global kernel Fourier convolutional neural networks (FourierNets). We show that FourierNets surpass existing deep network based decoders at reconstructing photographs captured by the highly non-local DiffuserCam optical encoder. Further, we show that FourierNets enable E2E optimization of highly non-local optical encoders for 3D snapshot microscopy. By combining FourierNets with a large-scale multi-GPU differentiable optical simulation, we are able to optimize non-local optical encoders 170$\times$ to 7372$\times$ larger than prior state of the art, and demonstrate the potential for ROI-type specific optical encoding with a programmable microscope.
△ Less
Submitted 2 November, 2022; v1 submitted 21 April, 2021;
originally announced April 2021.
-
The Univalence Principle
Authors:
Benedikt Ahrens,
Paige Randall North,
Michael Shulman,
Dimitris Tsementzis
Abstract:
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of…
▽ More
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk's completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences.
Our work builds on Makkai's First-Order Logic with Dependent Sorts, but is expressed in Voevodsky's Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.
△ Less
Submitted 29 August, 2022; v1 submitted 11 February, 2021;
originally announced February 2021.
-
A Higher Structure Identity Principle
Authors:
Benedikt Ahrens,
Paige Randall North,
Michael Shulman,
Dimitris Tsementzis
Abstract:
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a…
▽ More
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with "isomorphisms" between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call "indiscernibilities", using only the dependency structure rather than any notion of composition.
△ Less
Submitted 23 June, 2020; v1 submitted 14 April, 2020;
originally announced April 2020.
-
Reduction Monads and Their Signatures
Authors:
Benedikt Ahrens,
André Hirschowitz,
Ambroise Lafont,
Marco Maggesi
Abstract:
In this work, we study 'reduction monads', which are essentially the same as monads relative to the free functor from sets into multigraphs. Reduction monads account for two aspects of the lambda calculus: on the one hand, in the monadic viewpoint, the lambda calculus is an object equipped with a well-behaved substitution; on the other hand, in the graphical viewpoint, it is an oriented multigraph…
▽ More
In this work, we study 'reduction monads', which are essentially the same as monads relative to the free functor from sets into multigraphs. Reduction monads account for two aspects of the lambda calculus: on the one hand, in the monadic viewpoint, the lambda calculus is an object equipped with a well-behaved substitution; on the other hand, in the graphical viewpoint, it is an oriented multigraph whose vertices are terms and whose edges witness the reductions between two terms.
We study presentations of reduction monads. To this end, we propose a notion of 'reduction signature'. As usual, such a signature plays the role of a virtual presentation, and specifies arities for generating operations---possibly subject to equations---together with arities for generating reduction rules. For each such signature, we define a category of models; any model is, in particular, a reduction monad. If the initial object of this category of models exists, we call it the 'reduction monad presented (or specified) by the given reduction signature'.
Our main result identifies a class of reduction signatures which specify a reduction monad in the above sense. We show in the examples that our approach covers several standard variants of the lambda calculus.
△ Less
Submitted 14 November, 2019;
originally announced November 2019.
-
Bicategories in Univalent Foundations
Authors:
Benedikt Ahrens,
Dan Frumin,
Marco Maggesi,
Niccolò Veltri,
Niels van der Weide
Abstract:
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicabi…
▽ More
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.
△ Less
Submitted 15 August, 2022; v1 submitted 4 March, 2019;
originally announced March 2019.
-
Modular specification of monads through higher-order presentations
Authors:
Benedikt Ahrens,
André Hirschowitz,
Ambroise Lafont,
Marco Maggesi
Abstract:
In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of `models', and they give a monadicity result which implies that this category has an initial object, which is the language p…
▽ More
In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of `models', and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair.
In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating (`higher-order') operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to $β$- and $η$-equalities. Such a 2-signature is hence a pair $(Σ,E)$ of a binding signature $Σ$ and a family $E$ of equations for $Σ$. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context.
We associate, to each 2-signature $(Σ,E)$, a category of `models of $(Σ,E)$; and we say that a 2-signature is `effective' if this category has an initial object; the monad underlying this (essentially unique) object is the `monad specified by the 2-signature'. Not every 2-signature is effective; we identify a class of 2-signatures, which we call `algebraic', that are effective.
Importantly, our 2-signatures together with their models enjoy `modularity': when we glue (algebraic) 2-signatures together, their initial models are glued accordingly.
We provide a computer formalization for our main results.
△ Less
Submitted 3 March, 2019;
originally announced March 2019.
-
Presentable signatures and initial semantics
Authors:
Benedikt Ahrens,
André Hirschowitz,
Ambroise Lafont,
Marco Maggesi
Abstract:
We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions.
In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object -- if it exists -- in a suitable category of models. In our framework, the existe…
▽ More
We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions.
In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object -- if it exists -- in a suitable category of models. In our framework, the existence of an associated syntax to a signature is not automatically guaranteed. We identify, via the notion of presentation of a signature, a large class of signatures that do generate a syntax.
Our (presentable) signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend them to include several other significant examples of syntactic constructions.
One key feature of our notions of signature, syntax, and presentation is that they are highly compositional, in the sense that complex examples can be obtained by gluing simpler ones. Moreover, through the Initial Semantics approach, our framework provides, beyond the desired algebra of terms, a well-behaved substitution and the induction and recursion principles associated to the syntax.
This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu.
The main results presented in the paper are computer-checked within the UniMath system.
△ Less
Submitted 25 May, 2021; v1 submitted 9 May, 2018;
originally announced May 2018.
-
Categorical structures for type theory in univalent foundations
Authors:
Benedikt Ahrens,
Peter LeFanu Lumsdaine,
Vladimir Voevodsky
Abstract:
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps betw…
▽ More
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences.
We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure.
We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.
△ Less
Submitted 8 September, 2018; v1 submitted 11 May, 2017;
originally announced May 2017.
-
From signatures to monads in UniMath
Authors:
Benedikt Ahrens,
Ralph Matthes,
Anders Mörtberg
Abstract:
The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it - in particular, general inductive types are not part of the system.
In this work, we part…
▽ More
The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept as small as possible in order to ease verification of it - in particular, general inductive types are not part of the system.
In this work, we partially remedy the lack of inductive types by constructing some datatypes and their associated induction principles from other type constructors. This involves a formalization of a category-theoretic result on the construction of initial algebras, as well as a mechanism to conveniently use the datatypes obtained. We also connect this construction to a previous formalization of substitution for languages with variable binding. Altogether, we construct a framework that allows us to concisely specify, via a simple notion of binding signature, a language with variable binding. From such a specification we obtain the datatype of terms of that language, equipped with a certified monadic substitution operation and a suitable recursion scheme. Using this we formalize the untyped lambda calculus and the raw syntax of Martin-Löf type theory.
△ Less
Submitted 2 December, 2016;
originally announced December 2016.
-
Heterogeneous substitution systems revisited
Authors:
Benedikt Ahrens,
Ralph Matthes
Abstract:
Matthes and Uustalu (TCS 327(1-2):155-174, 2004) presented a categorical description of substitution systems capable of capturing syntax involving binding which is independent of whether the syntax is made up from least or greatest fixed points. We extend this work in two directions: we continue the analysis by creating more categorical structure, in particular by organizing substitution systems i…
▽ More
Matthes and Uustalu (TCS 327(1-2):155-174, 2004) presented a categorical description of substitution systems capable of capturing syntax involving binding which is independent of whether the syntax is made up from least or greatest fixed points. We extend this work in two directions: we continue the analysis by creating more categorical structure, in particular by organizing substitution systems into a category and studying its properties, and we develop the proofs of the results of the cited paper and our new ones in UniMath, a recent library of univalent mathematics formalized in the Coq theorem prover.
△ Less
Submitted 17 January, 2016;
originally announced January 2016.
-
Non-wellfounded trees in Homotopy Type Theory
Authors:
Benedikt Ahrens,
Paolo Capriotti,
Régis Spadotti
Abstract:
We prove a conjecture about the constructibility of coinductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presence of inductive types, coinductive types are derivable. Indeed, in this work, we construct coinductive types in a subsystem of Homotopy Type Theory; this subsystem is given by Intensional Martin-Löf type theory with natur…
▽ More
We prove a conjecture about the constructibility of coinductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presence of inductive types, coinductive types are derivable. Indeed, in this work, we construct coinductive types in a subsystem of Homotopy Type Theory; this subsystem is given by Intensional Martin-Löf type theory with natural numbers and Voevodsky's Univalence Axiom. Our results are mechanized in the computer proof assistant Agda.
△ Less
Submitted 12 April, 2015;
originally announced April 2015.
-
Terminal semantics for codata types in intensional Martin-Löf type theory
Authors:
Benedikt Ahrens,
Régis Spadotti
Abstract:
In this work, we study the notions of relative comonad and comodule over a relative comonad, and use these notions to give a terminal coalgebra semantics for the coinductive type families of streams and of infinite triangular matrices, respectively, in intensional Martin-Löf type theory. Our results are mechanized in the proof assistant Coq.
In this work, we study the notions of relative comonad and comodule over a relative comonad, and use these notions to give a terminal coalgebra semantics for the coinductive type families of streams and of infinite triangular matrices, respectively, in intensional Martin-Löf type theory. Our results are mechanized in the proof assistant Coq.
△ Less
Submitted 22 April, 2014; v1 submitted 6 January, 2014;
originally announced January 2014.
-
Initial Semantics for Reduction Rules
Authors:
Benedikt Ahrens
Abstract:
We give an algebraic characterization of the syntax and operational semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed syntax with variable binding and equipped with reduction rules via a universal property, namely as the initial object of some category of models. For this purpose, we employ techniques developed in two previous works: in the firs…
▽ More
We give an algebraic characterization of the syntax and operational semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed syntax with variable binding and equipped with reduction rules via a universal property, namely as the initial object of some category of models. For this purpose, we employ techniques developed in two previous works: in the first work we model syntactic translations between languages over different sets of types as initial morphisms in a category of models. In the second work we characterize untyped syntax with reduction rules as initial object in a category of models. In the present work, we combine the techniques used earlier in order to characterize simply-typed syntax with reduction rules as initial object in a category. The universal property yields an operator which allows to specify translations---that are semantically faithful by construction---between languages over possibly different sets of types.
As an example, we upgrade a translation from PCF to the untyped lambda calculus, given in previous work, to account for reduction in the source and target. Specifically, we specify a reduction semantics in the source and target language through suitable rules. By equip** the untyped lambda calculus with the structure of a model of PCF, initiality yields a translation from PCF to the lambda calculus, that is faithful with respect to the reduction semantics specified by the rules.
This paper is an extended version of an article published in the proceedings of WoLLIC 2012.
△ Less
Submitted 20 March, 2019; v1 submitted 22 December, 2012;
originally announced December 2012.
-
Initiality for Typed Syntax and Semantics
Authors:
Benedikt Ahrens
Abstract:
In this thesis we give an algebraic characterization of the syntax and semantics of simply-typed languages. More precisely, we characterize simply-typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. We specify a language by a 2-signature (Σ, A), that is, a signature on two levels: the syntactic level Σ specifies the sorts and…
▽ More
In this thesis we give an algebraic characterization of the syntax and semantics of simply-typed languages. More precisely, we characterize simply-typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. We specify a language by a 2-signature (Σ, A), that is, a signature on two levels: the syntactic level Σ specifies the sorts and terms of the language, and associates a sort to each term. The semantic level A specifies, through inequations, reduction rules on the terms of the language. To any given 2-signature (Σ, A) we associate a category of "models" of (Σ, A). We prove that this category has an initial object, which integrates the terms freely generated by Σ and the reduction relation - on those terms - generated by A. We call this object the programming language generated by (Σ, A).
Initiality provides an iteration principle which allows to specify translations on the syntax, possibly to a language over different sorts. Furthermore, translations specified via the iteration principle are by construction type-safe and faithful with respect to reduction.
To illustrate our results, we consider two examples extensively: firstly, we specify a double negation translation from classical to intuitionistic propositional logic via the category-theoretic iteration principle. Secondly, we specify a translation from PCF to the untyped lambda calculus which is faithful with respect to reduction in the source and target languages.
In a second part, we formalize some of our initiality theorems in the proof assistant Coq. The implementation yields a machinery which, when given a 2-signature, returns an implementation of its associated abstract syntax together with certified substitution operation, iteration operator and a reduction relation generated by the specified reduction rules.
△ Less
Submitted 20 June, 2012;
originally announced June 2012.
-
Initiality for Typed Syntax and Semantics
Authors:
Benedikt Ahrens
Abstract:
We give an algebraic characterization of the syntax and semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. For this purpose, we employ techniques developed in two previous works: in [2], we model syntactic translations between lan…
▽ More
We give an algebraic characterization of the syntax and semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed binding syntax equipped with reduction rules via a universal property, namely as the initial object of some category. For this purpose, we employ techniques developed in two previous works: in [2], we model syntactic translations between languages over different sets of types as initial morphisms in a category of models. In [1], we characterize untyped syntax with reduction rules as initial object in a category of models. In the present work, we show that those techniques are modular enough to be combined: we thus characterize simply-typed syntax with reduction rules as initial object in a category. The universal property yields an operator which allows to specify translations - that are semantically faithful by construction - between languages over possibly different sets of types.
We specify a language by a 2-signature, that is, a signature on two levels: the syntactic level specifies the types and terms of the language, and associates a type to each term. The semantic level specifies, through inequations, reduction rules on the terms of the language. To any given 2-signature we associate a category of models. We prove that this category has an initial object, which integrates the types and terms freely generated by the 2-signature, and the reduction relation on those terms generated by the given inequations. We call this object the (programming) language generated by the 2-signature.
[1] Ahrens, B.: Modules over relative monads for syntax and semantics (2011), arXiv:1107.5252, to be published in Math. Struct. in Comp. Science
[2] Ahrens, B.: Extended Initiality for Typed Abstract Syntax. Logical Methods in Computer Science 8(2), 1-35 (2012)
△ Less
Submitted 20 June, 2012;
originally announced June 2012.
-
Modules over relative monads for syntax and semantics
Authors:
Benedikt Ahrens
Abstract:
We give an algebraic characterization of the syntax and semantics of a class of languages with variable binding.
We introduce a notion of 2-signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2-signature $S$ we associate a category of "models" of $S$. This category has an initial object, which integrates the terms freely generat…
▽ More
We give an algebraic characterization of the syntax and semantics of a class of languages with variable binding.
We introduce a notion of 2-signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2-signature $S$ we associate a category of "models" of $S$. This category has an initial object, which integrates the terms freely generated by $S$, and which is equipped with reductions according to the inequations given in $S$. We call this initial object the language generated by $S$. Models of a 2--signature are built from relative monads and modules over such monads. Through the use of monads, the models---and in particular, the initial model---come equipped with a substitution operation that is compatible with reduction in a suitable sense.
The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2-signature, provides the associated programming language with reduction relation and certified substitution.
△ Less
Submitted 18 November, 2013; v1 submitted 26 July, 2011;
originally announced July 2011.
-
Extended Initiality for Typed Abstract Syntax
Authors:
Benedikt Ahrens
Abstract:
Initial Semantics aims at interpreting the syntax associated to a signature as the initial object of some category of 'models', yielding induction and recursion principles for abstract syntax. Zsidó proves an initiality result for simply-typed syntax: given a signature S, the abstract syntax associated to S constitutes the initial object in a category of models of S in monads. However, the iterat…
▽ More
Initial Semantics aims at interpreting the syntax associated to a signature as the initial object of some category of 'models', yielding induction and recursion principles for abstract syntax. Zsidó proves an initiality result for simply-typed syntax: given a signature S, the abstract syntax associated to S constitutes the initial object in a category of models of S in monads. However, the iteration principle her theorem provides only accounts for translations between two languages over a fixed set of object types. We generalize Zsidó's notion of model such that object types may vary, yielding a larger category, while preserving initiality of the syntax therein. Thus we obtain an extended initiality theorem for typed abstract syntax, in which translations between terms over different types can be specified via the associated category-theoretic iteration operator as an initial morphism. Our definitions ensure that translations specified via initiality are type-safe, i.e. compatible with the ty** in the source and target language in the obvious sense. Our main example is given via the propositions-as-types paradigm: we specify propositions and inference rules of classical and intuitionistic propositional logics through their respective typed signatures. Afterwards we use the category--theoretic iteration operator to specify a double negation translation from the former to the latter. A second example is given by the signature of PCF. For this particular case, we formalize the theorem in the proof assistant Coq. Afterwards we specify, via the category-theoretic iteration operator, translations from PCF to the untyped lambda calculus.
△ Less
Submitted 5 April, 2012; v1 submitted 24 July, 2011;
originally announced July 2011.
-
Initial Semantics for higher-order typed syntax in Coq
Authors:
Benedikt Ahrens,
Julianna Zsido
Abstract:
Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof assistant. The main theorem was first proved on paper in the second author's PhD thesis in 2010, and verified formally shortly afterwards. To a simply-typed binding…
▽ More
Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof assistant. The main theorem was first proved on paper in the second author's PhD thesis in 2010, and verified formally shortly afterwards. To a simply-typed binding signature S over a fixed set T of object types we associate a category called the category of representations of S. We show that this category has an initial object Sigma(S). From its construction it will be clear that the object Sigma(S) merits the name abstract syntax associated to S. Our theorem is implemented and proved correct in the proof assistant Coq through heavy use of dependent types. The approach through monads gives rise to an implementation of syntax where both terms and variables are intrinsically typed, i.e. where the object types are reflected in the meta-level types. This article is to be seen as a research article rather than about the formalization of a classical mathematical result. The nature of our theorem - involving lengthy, technical proofs and complicated algebraic structures - makes it particularly interesting for formal verification. Our goal is to promote the use of computer theorem provers as research tools, and, accordingly, a new way of publishing mathematical results: a parallel description of a theorem and its formalization should allow the verification of correct transcription of definitions and statements into the proof assistant, and straightforward but technical proofs should be well-hidden in a digital library. We argue that Coq's rich type theory, combined with its various features such as implicit arguments, allows a particularly readable formalization and is hence well-suited for communicating mathematics.
△ Less
Submitted 17 September, 2011; v1 submitted 5 December, 2010;
originally announced December 2010.
