-
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.
-
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.
-
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
Authors:
José Espírito Santo,
Ralph Matthes,
Luís Pinto
Abstract:
The approach to proof search dubbed "coinductive proof search", and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes develo** a coinductive description of the search space generate…
▽ More
The approach to proof search dubbed "coinductive proof search", and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes develo** a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. We prove the decidability of existence of focused inhabitants, and of finiteness of the number of focused inhabitants for polarized intuitionistic logic, by means of such recursive procedures. Moreover, the polarized logic can be used as a platform from which proof search for other logics is understood. We illustrate the technique with LJT, a focused sequent calculus for full intuitionistic propositional logic (including disjunction). For that, we have to work out the "negative translation" of LJT into LJP (that sees all intuitionistic types as negative types), and verify that the translation gives a faithful representation of proof search in LJT as proof search in the polarized logic. We therefore inherit decidability of both problems studied for LJP and thus get new proofs of these results for LJT.
△ Less
Submitted 30 March, 2021; v1 submitted 31 July, 2020;
originally announced July 2020.
-
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.
-
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
Authors:
José Espírito Santo,
Ralph Matthes,
Luís Pinto
Abstract:
A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending th…
▽ More
A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda-terms, staying within the methods of lambda-calculus and type systems. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and the end products are simple, recursive decision procedures and counting functions.
△ Less
Submitted 11 March, 2017; v1 submitted 7 April, 2016;
originally announced April 2016.
-
A Coinductive Approach to Proof Search through Typed Lambda-Calculi
Authors:
José Espírito Santo,
Ralph Matthes,
Luís Pinto
Abstract:
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 approa…
▽ More
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 fixed point, and a type system that can be seen as a logic of coinductive proofs. In the finitary system, fixed-point variables enjoy a relaxed form of binding that allows the detection of cycles through the type system. Formal sums are used to express alternatives in the search process. Moreover, formal sums are used in the coinductive syntax to define "decontraction" (contraction bottom-up) - an operation whose theory we initiate in this paper. As a semantics, we assign a coinductive lambda-term to each finitary term. The main result is the existence of an equivalent finitary representation for any full solution space expressed coinductively. This result is the main ingredient in the proof that our logic of coinductive proofs is sound and complete with respect to the coinductive semantics. These results are the foundation for an original approach to proof search, where the search builds the finitary representation of the full solution space, and the a posteriori analysis typically consisting in applying a syntax-directed procedure or function. The paper illustrates this for proof search and inhabitation problems in the simply-typed lambda-calculus, reviewing results detailed elsewhere, and including new results that obtain extensive generalizations of the so-called monatomic theorem.
△ Less
Submitted 29 July, 2021; v1 submitted 13 February, 2016;
originally announced February 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.
-
Proceedings Tenth International Workshop on Fixed Points in Computer Science
Authors:
Ralph Matthes,
Matteo Mio
Abstract:
This volume contains the proceedings of the Tenth International Workshop on Fixed Points in Computer Science (FICS 2015) which took place on September 11th and 12th, 2015 in Berlin, Germany, as a satellite event of the conference Computer Science Logic (CSL 2015).
Fixed points play a fundamental role in several areas of computer science. They are used to justify (co)recursive definitions and ass…
▽ More
This volume contains the proceedings of the Tenth International Workshop on Fixed Points in Computer Science (FICS 2015) which took place on September 11th and 12th, 2015 in Berlin, Germany, as a satellite event of the conference Computer Science Logic (CSL 2015).
Fixed points play a fundamental role in several areas of computer science. They are used to justify (co)recursive definitions and associated reasoning techniques. The construction and properties of fixed points have been investigated in many different settings such as: design and implementation of programming languages, logics, verification, databases. The aim of this workshop is to provide a forum for researchers to present their results to those members of the computer science and logic communities who study or apply the theory of fixed points.
Each of the 11 contributed papers of this volume were evaluated by three or four reviewers. Some of the papers were re-reviewed after revision.
Additionally, this volume contains the abstracts of the FICS 2015 invited talks given by Bartek Klin and James Worrell.
△ Less
Submitted 9 September, 2015;
originally announced September 2015.
-
Confluence for classical logic through the distinction between values and computations
Authors:
José Espírito Santo,
Ralph Matthes,
Koji Nakazawa,
Luís Pinto
Abstract:
We apply an idea originated in the theory of programming languages - monadic meta-language with a distinction between values and computations - in the design of a calculus of cut-elimination for classical logic. The cut-elimination calculus we obtain comprehends the call-by-name and call-by-value fragments of Curien-Herbelin's lambda-bar-mu-mu-tilde-calculus without losing confluence, and is based…
▽ More
We apply an idea originated in the theory of programming languages - monadic meta-language with a distinction between values and computations - in the design of a calculus of cut-elimination for classical logic. The cut-elimination calculus we obtain comprehends the call-by-name and call-by-value fragments of Curien-Herbelin's lambda-bar-mu-mu-tilde-calculus without losing confluence, and is based on a distinction of "modes" in the proof expressions and "mode" annotations in types. Modes resemble colors and polarities, but are quite different: we give meaning to them in terms of a monadic meta-language where the distinction between values and computations is fully explored. This meta-language is a refinement of the classical monadic language previously introduced by the authors, and is also developed in the paper.
△ Less
Submitted 10 September, 2014;
originally announced September 2014.
-
A Coinductive Approach to Proof Search
Authors:
José Espírito Santo,
Ralph Matthes,
Luís Pinto
Abstract:
We propose to study proof search from a coinductive point of view. In this paper, we consider intuitionistic logic and a focused system based on Herbelin's LJT for the implicational fragment. We introduce a variant of lambda calculus with potentially infinitely deep terms and a means of expressing alternatives for the description of the "solution spaces" (called Böhm forests), which are a represen…
▽ More
We propose to study proof search from a coinductive point of view. In this paper, we consider intuitionistic logic and a focused system based on Herbelin's LJT for the implicational fragment. We introduce a variant of lambda calculus with potentially infinitely deep terms and a means of expressing alternatives for the description of the "solution spaces" (called Böhm forests), which are a representation of all (not necessarily well-founded but still locally well-formed) proofs of a given formula (more generally: of a given sequent).
As main result we obtain, for each given formula, the reduction of a coinductive definition of the solution space to a effective coinductive description in a finitary term calculus with a formal greatest fixed-point operator. This reduction works in a quite direct manner for the case of Horn formulas. For the general case, the naive extension would not even be true. We need to study "co-contraction" of contexts (contraction bottom-up) for dealing with the varying contexts needed beyond the Horn fragment, and we point out the appropriate finitary calculus, where fixed-point variables are typed with sequents. Co-contraction enters the interpretation of the formal greatest fixed points - curiously in the semantic interpretation of fixed-point variables and not of the fixed-point operator.
△ Less
Submitted 3 September, 2013;
originally announced September 2013.
-
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
Authors:
Jose Espirito Santo,
Ralph Matthes,
Luis Pinto
Abstract:
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 s…
▽ More
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. We apply the same method to other calculi, namely successive extensions of the simply-typed λ-calculus leading to our intuitionistic system, and already for the simplest extension we consider (λ-calculus with generalised application), this yields the first proof of strong normalisation through a reduction-preserving embedding. The results obtained extend to second and higher-order calculi.
△ Less
Submitted 25 May, 2009; v1 submitted 10 March, 2009;
originally announced March 2009.
