Selected Papers of the 4th International Conference on Formal Structures and Deduction (FSCD 2019)

Editors: Herman Geuvers, Femke van Raamsdonk

This special issue contains full versions of six papers presented at FSCD 2019, the Fourth International Conference on Formal Structures for Computation and Deduction that was held in Dortmund, Germany, on June 24--30, 2019.

FSCD ({\\tt http://fscd-conference.org/}) covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Initially building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logic and proof theory, new emerging models of computation, semantics and verification in challenging areas.

The fourth edition of FSCD attracted 69 submissions, of which 30 were selected for presentation at the conference. We invited the authors of seven selected papers to submit an extended version to this special issue. These submissions received two or three additional reports and underwent several rounds of reviewing. One paper was in an early stage withdrawn by the authors, and six papers found their way to this special issue.

These six papers illustrate a variety of subjects and techniques that are typical for FSCD. % The paper by Mirai Ikebuchi considers the question of how to find a lower bound on the number of axioms needed to define an equational theory using techniques from homology theory. % Jonathan Sterling, Carlo Angiuli and Daniel Gratzer present a version of Cartesian cubical type theory for Bishop sets. % These two papers %%% are special because their authors were awarded a FSCD 2019 Best Paper Award for Junior Researchers by the Program Committee of FSCD 2019. % The special issue contains four more papers. % The paper by Domininique Larchey-Wendling and Yannick Forster presents a formalization in the proof assistant %%% checker Coq of the undecidability of solvability of Diophantine equations. % The paper %%% on differentials and distances in probabilistic coherence spaces by Thomas Ehrhard explores a semantical view on extending probabilistic programming languages with derivatives. % The paper by Thierry Coquand, Simon Huber and Christian Sattler about cubical type theory uses a sconing argument to prove both a homotopy canonicity result and a canonicity result. % Claudia Faggian's paper considers the classical rewriting concepts uniqueness of normal forms and strategies in a probabilistic setting.

We thank all who contributed to FSCD 2019. We thank the PC %%% program committee of FSCD 2019 for their advice in the selection process. We are very grateful to the referees for their valuable and constructive contribution and for the time they devoted to this work on top of the additional workload due to the Covid pandemic. We thank all authors for carefully preparing their papers. Finally, we are grateful to LMCS for making this special issue possible, and we in particular thank Brigitte Pientka for her support during the process.

Herman Geuvers, Femke van Raamsdonk
Guest Editors of the FSCD 2019 Special Issue

1. Canonicity and homotopy canonicity for cubical type theory

Thierry Coquand ; Simon Huber ; Christian Sattler.

Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.

2. Hilbert's Tenth Problem in Coq (Extended Version)

Dominique Larchey-Wendling ; Yannick Forster.

We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem -- in our case by a Minsky machine -- is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer. Additionally, we prove the reverse direction and show that every Diophantine relation is recognisable by $\mu$-recursive functions and give a certified compiler from $\mu$-recursive functions to Minsky machines.

3. A Cubical Language for Bishop Sets

Jonathan Sterling ; Carlo Angiuli ; Daniel Gratzer.

We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) using Artin gluing.

4. Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms

Claudia Faggian.

While a mature body of work supports the study of rewriting systems, abstract tools for Probabilistic Rewriting are still limited. In this paper we study the question of uniqueness of the result (unique limit distribution), and develop a set of proof techniques to analyze and compare reduction strategies. The goal is to have tools to support the operational analysis of probabilistic calculi (such as probabilistic lambda-calculi) where evaluation allows for different reduction choices (hence different reduction paths).

5. Differentials and distances in probabilistic coherence spaces

Thomas Ehrhard.

In probabilistic coherence spaces, a denotational model of probabilistic functional languages, morphisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.

6. A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods

Mirai Ikebuchi.

It is well-known that some equational theories such as groups or boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. Malbos and Mimram investigated a general method to find a lower bound of the cardinality of the set of equational axioms (or rewrite rules) that is equivalent to a given equational theory (or term rewriting systems), using homological algebra. Their method is an analog of Squier's homology theory on string rewriting systems. In this paper, we develop the homology theory for term rewriting systems more and provide a better lower bound under a stronger notion of equivalence than their equivalence. The author also implemented a program to compute the lower bounds, and experimented with 64 complete TRSs.