Selected Papers of the 7th International Conference on Formal Structures and Deduction (FSCD 2022)

Editors: Amy Felty and Georg Moser

Preface


This special issue contains extended versions of papers presented at
FSCD 2022, the 7th International Conference on Formal Structures for
Computation and Deduction. FSCD 2022 was held from August 2--5 in Haifa, Israel,
as part of the Federated Logic Conference (FLoC).




FSCD covers all aspects of formal
structures for computation and deduction from theoretical foundations
to applications. 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, models of computation,
semantics, and verification in new challenging areas.




The papers selected for this special issue underwent a reviewing
process in two stages. In the first stage, the FSCD program committee
selected 31 papers out of 59 submissions. From the papers presented
at the conference, we invited authors of selected papers to submit
revised and extended versions of their work to this special issue.




In the second stage, the submitted extended papers were reviewed
following the usual high standards of LMCS, and six were accepted.
The topics of the papers include category theory, logic,
quantum computation, rewriting, semantics and type theory.
%Thus, reflecting upon traditional and recent hot topics of FSCD. In the following,
The papers thus reflect upon traditional and recent hot topics of FSCD. In the following,
we give a brief description of each of the accepted papers.




A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential by Francesco Dagnino and Francesco Gavazzo.


This work provides foundational understanding of operational logical relations and contains two contributions: first the authors give a general categorical framework of logical relations for (call-by-value) operational semantics. As the second (and main) contribution, the authors give a categorical generalization/understanding of a recent relational-lifting technique called differential logical relations.




Addition and Differentiation of ZX-Diagrams
by Emmanuel Jeandel, Simon Perdrix and Margarita Veshchezerova.

The ZX-calculus is a powerful framework for reasoning in quantum computing. The paper establishes
a way to represent the sum of two ZX-diagrams as another ZX-diagram, based on which the authors continue
to establish a representation theorem for differentiation. This establishes solutions to problems that had been considered in the ZX-calculus community for a couple of years already.




An Analysis of Tennenbaum's Theorem in Constructive Type Theory
by Marc Hermes and Dominik Kirst.


Four variants of Tennenbaum's theorem are given (including one under an anti-classical axiom which rules out any non-standard model). They are all already known from the literature and the contribution is to formalize them in full detail, formally analyzing the logical assumptions they rely on.
The conference version was awarded the FSCD 2022 Best Paper Award by Junior Researchers.




Compositional Confluence Criteria
by Kiraku Shintani and Nao Hirokawa.

The authors show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms.




Galois Connecting Call-By-Value and Call-By-Name
by Dylan McDermott and Alan Mycroft.

The paper establishes a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with computational effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. This nice and elegant contribution crystallizes an intuition that seems to be fairly well established in existing results.




Stabilized Profunctors and Stable Species of Structures
by Marcelo Fiore, Zeinab Galal and Hugo Paquet .


The paper generalizes the notion of polynomial functor so that the 2-category of generalized polynomial functors becomes a cartesian closed bicategory. This serves as a model of simply typed lambda calculus, and will lead to further research towards a model of linear logic and differential lambda calculus.




Foremost, we would like to thank all the authors for their professional work to prepare
submissions, and the reviewers for their very constructive and helpful suggestions to
improve the original submissions. Further, we would like to thank Herman
Geuvers as chair of the Steering Committee of FSCD, as well as Brigitte Pientka, as Executive Editor of
LMCS. Their advice has been invaluable. Finally, we would like to thank the layout editors at LMCS, handling
the final steps of the publication process.




Amy Felty and Georg Moser

Guest Editors of the FSCD 2022 Special Issue



1. Galois connecting call-by-value and call-by-name

Dylan McDermott ; Alan Mycroft.
We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with computational effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving properties like these. The key ingredient is Levy's call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We show that the call-by-value and call-by-name translations of expressions into call-by-push-value have related observable behaviour under certain conditions on computational effects, which we identify. We then use this fact to construct maps between the call-by-value and call-by-name interpretations of types, and identify further properties of effects that imply these maps form a Galois connection. These properties hold for some computational effects (such as divergence), but not others (such as mutable state). This gives rise to a general reasoning principle that relates call-by-value and call-by-name. We apply the reasoning principle to example computational effects including divergence and nondeterminism.

2. A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential

Francesco Dagnino ; Francesco Gavazzo.
Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a lambda-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations -- a recently introduced notion of higher-order distance between programs -- both pure and effectful, bringing them back to a common picture with traditional ones.

3. An Analysis of Tennenbaum's Theorem in Constructive Type Theory

Marc Hermes ; Dominik Kirst.
Tennenbaum's theorem states that the only countable model of Peano arithmetic (PA) with computable arithmetical operations is the standard model of natural numbers. In this paper, we use constructive type theory as a framework to revisit, analyze and generalize this result. The chosen framework allows for a synthetic approach to computability theory, exploiting that, externally, all functions definable in constructive type theory can be shown computable. We then build on this viewpoint, and furthermore internalize it by assuming a version of Church's thesis, which expresses that any function on natural numbers is representable by a formula in PA. This assumption provides for a conveniently abstract setup to carry out rigorous computability arguments, even in the theorem's mechanization. Concretely, we constructivize several classical proofs and present one inherently constructive rendering of Tennenbaum's theorem, all following arguments from the literature. Concerning the classical proofs in particular, the constructive setting allows us to highlight differences in their assumptions and conclusions which are not visible classically. All versions are accompanied by a unified mechanization in the Coq proof assistant.

4. Compositional Confluence Criteria

Kiraku Shintani ; Nao Hirokawa.
We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. We also show how such a criterion can be used for a reduction method that removes rewrite rules unnecessary for confluence analysis. In addition to them, we prove that Toyama's parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem.

5. Stabilized profunctors and stable species of structures

Marcelo Fiore ; Zeinab Galal ; Hugo Paquet.
We introduce a bicategorical model of linear logic which is a novel variation of the bicategory of groupoids, profunctors, and natural transformations. Our model is obtained by endowing groupoids with additional structure, called a kit, to stabilize the profunctors by controlling the freeness of the groupoid action on profunctor elements. The theory of generalized species of structures, based on profunctors, is refined to a new theory of \emph{stable species} of structures between groupoids with Boolean kits. Generalized species are in correspondence with analytic functors between presheaf categories; in our refined model, stable species are shown to be in correspondence with restrictions of analytic functors, which we characterize as being stable, to full subcategories of stabilized presheaves. Our motivating example is the class of finitary polynomial functors between categories of indexed sets, also known as normal functors, that arises from kits enforcing free actions. We show that the bicategory of groupoids with Boolean kits, stable species, and natural transformations is cartesian closed. This makes essential use of the logical structure of Boolean kits and explains the well-known failure of cartesian closure for the bicategory of finitary polynomial functors between categories of set-indexed families and cartesian natural transformations. The paper additionally develops the model of classical linear logic underlying the cartesian closed structure and clarifies the […]

6. Addition and Differentiation of ZX-diagrams

Emmanuel Jeandel ; Simon Perdrix ; Margarita Veshchezerova.
The ZX-calculus is a powerful framework for reasoning in quantum computing. It provides in particular a compact representation of matrices of interests. A peculiar property of the ZX-calculus is the absence of a formal sum allowing the linear combinations of arbitrary ZX-diagrams. The universality of the formalism guarantees however that for any two ZX-diagrams, the sum of their interpretations can be represented by a ZX-diagram. We introduce a general, inductive definition of the addition of ZX-diagrams, relying on the construction of controlled diagrams. Based on this addition technique, we provide an inductive differentiation of ZX-diagrams. Indeed, given a ZX-diagram with variables in the description of its angles, one can differentiate the diagram according to one of these variables. Differentiation is ubiquitous in quantum mechanics and quantum computing (e.g. for solving optimization problems). Technically, differentiation of ZX-diagrams is strongly related to summation as witnessed by the product rules. We also introduce an alternative, non inductive, differentiation technique rather based on the isolation of the variables. Finally, we apply our results to deduce a diagram for an Ising Hamiltonian.