eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
1
634
10.4230/LIPIcs.FSCD.2021
article
LIPIcs, Volume 195, FSCD 2021, Complete Volume
Kobayashi, Naoki
1
https://orcid.org/0000-0002-0537-0604
The University of Tokyo, Japan
LIPIcs, Volume 195, FSCD 2021, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021/LIPIcs.FSCD.2021.pdf
LIPIcs, Volume 195, FSCD 2021, Complete Volume
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
0:i
0:xvi
10.4230/LIPIcs.FSCD.2021.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Kobayashi, Naoki
1
https://orcid.org/0000-0002-0537-0604
The University of Tokyo, Japan
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.0/LIPIcs.FSCD.2021.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
1:1
1:32
10.4230/LIPIcs.FSCD.2021.1
article
Duality in Action (Invited Talk)
Downen, Paul
1
https://orcid.org/0000-0003-0165-9387
Ariola, Zena M.
1
https://orcid.org/0000-0001-5551-8294
Department of Computer & Information Science, University of Oregon, Eugene, OR, USA
The duality between "true" and "false" is a hallmark feature of logic. We show how this duality can be put to use in the theory and practice of programming languages and their implementations, too. Starting from a foundation of constructive logic as dialogues, we illustrate how it describes a symmetric language for computation, and survey several applications of the dualities found therein.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.1/LIPIcs.FSCD.2021.1.pdf
Duality
Logic
Curry-Howard
Sequent Calculus
Rewriting
Compilation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
2:1
2:9
10.4230/LIPIcs.FSCD.2021.2
article
Completion and Reduction Orders (Invited Talk)
Hirokawa, Nao
1
https://orcid.org/0000-0002-8499-0501
Japan Advanced Institute of Science and Technology, Ishikawa, Japan
We present three techniques for improving the Knuth-Bendix completion procedure and its variants: An order extension by semantic labeling, a new confluence criterion for terminating term rewrite systems, and inter-reduction for maximal completion.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.2/LIPIcs.FSCD.2021.2.pdf
term rewriting
completion
reduction order
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
3:1
3:21
10.4230/LIPIcs.FSCD.2021.3
article
Process-As-Formula Interpretation: A Substructural Multimodal View (Invited Talk)
Pimentel, Elaine
1
https://orcid.org/0000-0002-7113-0801
Olarte, Carlos
2
https://orcid.org/0000-0002-7264-7773
Nigam, Vivek
3
https://orcid.org/0000-0003-4089-1218
Department of Mathematics, Federal University of Rio Grande Do Norte, Natal, Brazil
School of Science and Technology, Federal University of Rio Grande Do Norte, Natal, Brazil
Huawei Munich Research Center, Germany
In this survey, we show how the processes-as-formulas interpretation, where computations and proof-search are strongly connected, can be used to specify different concurrent behaviors as logical theories. The proposed interpretation is parametric and modular, and it faithfully captures behaviors such as: Linear and spatial computations, epistemic state of agents, and preferences in concurrent systems. The key for this modularity is the incorporation of multimodalities in a resource aware logic, together with the ability of quantifying on such modalities. We achieve tight adequacy theorems by relying on a focusing discipline that allows for controlling the proof search process.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.3/LIPIcs.FSCD.2021.3.pdf
Linear logic
proof theory
process calculi
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
4:1
4:4
10.4230/LIPIcs.FSCD.2021.4
article
Some Formal Structures in Probability (Invited Talk)
Staton, Sam
1
University of Oxford, UK
This invited talk will discuss how developments in the Formal Structures for Computation and Deduction can also suggest new directions for the foundations of probability theory. I plan to focus on two aspects: abstraction, and laziness. I plan to highlight two challenges: higher-order random functions, and stochastic memoization.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.4/LIPIcs.FSCD.2021.4.pdf
Probabilistic programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
5:1
5:17
10.4230/LIPIcs.FSCD.2021.5
article
The Expressive Power of One Variable Used Once: The Chomsky Hierarchy and First-Order Monadic Constructor Rewriting
Simonsen, Jakob Grue
1
Department of Computer Science, University of Copenhagen, Denmark
We study the implicit computational complexity of constructor term rewriting systems where every function and constructor symbol is unary or nullary. Surprisingly, adding simple and natural constraints to rule formation yields classes of systems that accept exactly the four classes of languages in the Chomsky hierarchy.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.5/LIPIcs.FSCD.2021.5.pdf
Constructor term rewriting
Chomsky Hierarchy
Implicit Complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
6:1
6:6
10.4230/LIPIcs.FSCD.2021.6
article
Church’s Semigroup Is Sq-Universal
Statman, Rick
1
Carnegie Mellon University, Pittsburgh, PA, USA
We prove Church’s lambda calculus semigroup is sq-universal.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.6/LIPIcs.FSCD.2021.6.pdf
lambda calculus
Church’s semigroup
sq-universal
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
7:1
7:18
10.4230/LIPIcs.FSCD.2021.7
article
Call-By-Value, Again!
Kerinec, Axel
1
Manzonetto, Giulio
1
Ronchi Della Rocca, Simona
2
Laboratoire LIPN, CNRS UMR 7030, Université Sorbonne Paris-Nord, France
Computer Science Department, University of Torino, Italy
The quest for a fully abstract model of the call-by-value λ-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically.
We study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many λ-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus - namely valuability, potential valuability and solvability - both semantically, through the notion of approximants, and logically, by means of the type assignment system. We mainly focus on the characterizations of solvability, as they constitute an original result. Finally, we prove the decidability of the inhabitation problem for our type system by exhibiting a non-deterministic algorithm, which is proven sound, correct and terminating.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.7/LIPIcs.FSCD.2021.7.pdf
λ-calculus
call-by-value
intersection types
solvability
inhabitation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
8:1
8:18
10.4230/LIPIcs.FSCD.2021.8
article
Predicative Aspects of Order Theory in Univalent Foundations
de Jong, Tom
1
https://orcid.org/0000-0003-1585-3172
Escardó, Martín Hötzel
1
https://orcid.org/0000-0002-4091-6334
University of Birmingham, UK
We investigate predicative aspects of order theory in constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky’s propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. We prove our results for a general class of posets, which includes directed complete posets, bounded complete posets and sup-lattices, using a technical notion of a δ_V-complete poset. We also show that nontrivial locally small δ_V-complete posets necessarily lack decidable equality. Specifically, we derive weak excluded middle from assuming a nontrivial locally small δ_V-complete poset with decidable equality. Moreover, if we assume positivity instead of nontriviality, then we can derive full excluded middle. Secondly, we show that each of Zorn’s lemma, Tarski’s greatest fixed point theorem and Pataraia’s lemma implies propositional resizing. Hence, these principles are inherently impredicative and a predicative development of order theory must therefore do without them. Finally, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.8/LIPIcs.FSCD.2021.8.pdf
order theory
constructivity
predicativity
univalent foundations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
9:1
9:22
10.4230/LIPIcs.FSCD.2021.9
article
A Strong Call-By-Need Calculus
Balabonski, Thibaut
1
Lanco, Antoine
2
Melquiond, Guillaume
2
Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Gif-sur-Yvette, 91190, France
Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, LMF, Gif-sur-Yvette, 91190, France
We present a call-by-need λ-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness.
The calculus is shown to be normalizing in a strong sense: Whenever a λ-term t admits a normal form n in the λ-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.9/LIPIcs.FSCD.2021.9.pdf
strong reduction
call-by-need
evaluation strategy
normalization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
10:1
10:17
10.4230/LIPIcs.FSCD.2021.10
article
A Bicategorical Model for Finite Nondeterminism
Galal, Zeinab
1
IRIF, Université de Paris, France
Finiteness spaces were introduced by Ehrhard as a refinement of the relational model of linear logic. A finiteness space is a set equipped with a class of finitary subsets which can be thought of being subsets that behave like finite sets. A morphism between finiteness spaces is a relation that preserves the finitary structure. This model provided a semantics for finite non-determism and it gave a semantical motivation for differential linear logic and the syntactic notion of Taylor expansion. In this paper, we present a bicategorical extension of this construction where the relational model is replaced with the model of generalized species of structures introduced by Fiore et al. and the finiteness property now relies on finite presentability.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.10/LIPIcs.FSCD.2021.10.pdf
Differential linear logic
Species of structures
Finiteness
Bicategorical semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
11:1
11:14
10.4230/LIPIcs.FSCD.2021.11
article
Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions
Saotome, Kenji
1
Nakazawa, Koji
1
Kimura, Daisuke
2
Nagoya University, Japan
Toho University, Japan
Cyclic proof systems are sequent-calculus style proof systems that allow circular structures representing induction, and they are considered suitable for automated inductive reasoning. However, Kimura et al. have shown that the cyclic proof system for the symbolic heap separation logic does not satisfy the cut-elimination property, one of the most fundamental properties of proof systems. This paper proves that the cyclic proof system for the bunched logic with only nullary inductive predicates does not satisfy the cut-elimination property. It is hard to adapt the existing proof technique chasing contradictory paths in cyclic proofs since the bunched logic contains the structural rules. This paper proposes a new proof technique called proof unrolling. This technique can be adapted to the symbolic heap separation logic, and it shows that the cut-elimination fails even if we restrict the inductive predicates to nullary ones.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.11/LIPIcs.FSCD.2021.11.pdf
cyclic proofs
cut-elimination
bunched logic
separation logic
linear logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
12:1
12:18
10.4230/LIPIcs.FSCD.2021.12
article
A Functional Abstraction of Typed Invocation Contexts
Cong, Youyou
1
https://orcid.org/0000-0003-2315-6182
Ishio, Chiaki
2
Honda, Kaho
3
Asai, Kenichi
3
Tokyo Institute of Technology, Japan
Ochanomizu University, Tokyo,Japan
Ochanomizu University, Tokyo, Japan
In their paper "A Functional Abstraction of Typed Contexts", Danvy and Filinski show how to derive a type system of the shift and reset operators from a CPS translation. In this paper, we show how this method scales to Felleisen’s control and prompt operators. Compared to shift and reset, control and prompt exhibit a more dynamic behavior, in that they can manipulate a trail of contexts surrounding the invocation of captured continuations. Our key observation is that, by adopting a functional representation of trails in the CPS translation, we can derive a type system that allows fine-grain reasoning of programs involving manipulation of invocation contexts.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.12/LIPIcs.FSCD.2021.12.pdf
delimited continuations
control operators
control and prompt
CPS translation
type system
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
13:1
13:21
10.4230/LIPIcs.FSCD.2021.13
article
Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity
Galmiche, Didier
1
Gawek, Marta
1
Méry, Daniel
1
Université de Lorraine, CNRS, LORIA, Nancy, France
In this paper we consider the intuitionistic sentential calculus with Suszko’s identity (ISCI). After recalling the basic concepts of the logic and its associated Hilbert proof system, we introduce a new sound and complete class of models for ISCI which can be viewed as algebraic counterparts (and extensions) of sheaf-theoretic topological models of intuitionistic logic. We use this new class of models, called Beth semantics for ISCI, to derive a first labelled sequent calculus and show its adequacy w.r.t. the standard Hilbert axiomatization of ISCI. This labelled proof system, like all other current proof systems for ISCI that we know of, does not enjoy the subformula property, which is problematic for achieving termination. We therefore introduce a second labelled sequent calculus in which the standard rules for identity are replaced with new special rules and show that this second calculus admits cut-elimination. Finally, using a key regularity property of the forcing relation in Beth models, we show that the eigenvariable condition can be dropped, thus leading to the termination and decidability results.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.13/LIPIcs.FSCD.2021.13.pdf
Algebraic Semantics
Beth Models
Labelled Deduction
Intuitionistic Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
14:1
14:19
10.4230/LIPIcs.FSCD.2021.14
article
New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial
Das, Anupam
1
https://orcid.org/0000-0002-0142-3676
Rice, Alex A.
2
https://orcid.org/0000-0002-2698-5122
University of Birmingham, UK
University of Cambridge, UK
A linear inference is a valid inequality of Boolean algebra in which each variable occurs at most once on each side. Equivalently, it is a linear rewrite rule on Boolean terms that constitutes a valid implication. Linear inferences have played a significant role in structural proof theory, in particular in models of substructural logics and in normalisation arguments for deep inference proof systems.
Systems of linear logic and, later, deep inference are founded upon two particular linear inferences, switch : x ∧ (y ∨ z) → (x ∧ y) ∨ z, and medial : (w ∧ x) ∨ (y ∧ z) → (w ∨ y) ∧ (x ∨ z). It is well-known that these two are not enough to derive all linear inferences (even modulo all valid linear equations), but beyond this little more is known about the structure of linear inferences in general. In particular despite recurring attention in the literature, the smallest linear inference not derivable under switch and medial ("switch-medial-independent") was not previously known.
In this work we leverage recently developed graphical representations of linear formulae to build an implementation that is capable of more efficiently searching for switch-medial-independent inferences. We use it to find two "minimal" 8-variable independent inferences and also prove that no smaller ones exist; in contrast, a previous approach based directly on formulae reached computational limits already at 7 variables. One of these new inferences derives some previously found independent linear inferences. The other exhibits structure seemingly beyond the scope of previous approaches we are aware of; in particular, its existence contradicts a conjecture of Das and Strassburger.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.14/LIPIcs.FSCD.2021.14.pdf
rewriting
linear inference
proof theory
linear logic
implementation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
15:1
15:21
10.4230/LIPIcs.FSCD.2021.15
article
A Modular Associative Commutative (AC) Congruence Closure Algorithm
Kapur, Deepak
1
Department of Computer Science, University of New Mexico, Albuquerque, NM, USA
Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing the congruence closure by abstracting nonflat terms by constants as proposed first in Kapur’s congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency and/or have identities, as well as their various combinations. The algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into Satisfiability modulo Theories (SMT) solvers.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.15/LIPIcs.FSCD.2021.15.pdf
Congruence Closure
Associative and Commutative
Word Problems
Finitely Presented Algebras
Equational Theories
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
16:1
16:19
10.4230/LIPIcs.FSCD.2021.16
article
Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators
Fujii, Maika
1
Asai, Kenichi
1
Ochanomizu University, Tokyo, Japan
This paper derives an abstract machine and a virtual machine for the λ-calculus with four variants of delimited-control operators: shift/reset, control/prompt, shift₀/reset₀, and control₀/prompt₀. Starting from Shan’s definitional interpreter for the four operators, we successively apply various meaning-preserving transformations. Both trails of invocation contexts (needed for control and control₀) and metacontinuations (needed for shift₀ and control₀) are defunctionalized and eventually represented as a list of stack frames. The resulting virtual machine clearly models not only how the control operators and captured continuations behave but also when and which portion of stack frames is copied to the heap.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.16/LIPIcs.FSCD.2021.16.pdf
delimited-control operators
functional derivation
CPS transformation
defunctionalization
abstract machine
virtual machine
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
17:1
17:22
10.4230/LIPIcs.FSCD.2021.17
article
Positional Injectivity for Innocent Strategies
Blondeau-Patissier, Lison
1
Clairambault, Pierre
1
Université Lyon, EnsL, UCBL, CNRS, LIP, F-69342, Lyon Cedex 07, France
In asynchronous games, Melliès proved that innocent strategies are positional: their behaviour only depends on the position, not the temporal order used to reach it. This insightful result shaped our understanding of the link between dynamic (i.e. game) and static (i.e. relational) semantics.
In this paper, we investigate the positionality of innocent strategies in the traditional setting of Hyland-Ong-Nickau-Coquand pointer games. We show that though innocent strategies are not positional, total finite innocent strategies still enjoy a key consequence of positionality, namely positional injectivity: they are entirely determined by their positions. Unfortunately, this does not hold in general: we show a counter-example if finiteness and totality are lifted. For finite partial strategies we leave the problem open; we show however the partial result that two strategies with the same positions must have the same P-views of maximal length.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.17/LIPIcs.FSCD.2021.17.pdf
Game Semantics
Innocence
Relational Semantics
Positionality
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
18:1
18:20
10.4230/LIPIcs.FSCD.2021.18
article
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq
Larchey-Wendling, Dominique
1
https://orcid.org/0000-0001-9860-7203
Université de Lorraine, CNRS, LORIA, Vandœuvre-lès-Nancy, France
We present an alternate undecidability proof for entailment in (intuitionistic) multiplicative sub-exponential linear logic (MSELL). We contribute the result and its mechanised proof to the Coq library of synthetic undecidability. The result crucially relies on the undecidability of the halting problem for two counters Minsky machines, which we also hand out to the library. As a seed of undecidability, we start from FRACTRAN halting which we (many-one) reduce to Minsky machines termination by implementing Euclidean division using two counters only. We then give an alternate presentation of those two counters machines as sequent rules, where computation is performed by proof-search, and halting reduced to provability. We use this system called non-deterministic two counters Minsky machines to describe and compare both the legacy reduction to linear logic, and the more recent reduction to MSELL. In contrast with that former MSELL undecidability proof, our correctness argument for the reduction uses trivial phase semantics in place of a focused calculus.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.18/LIPIcs.FSCD.2021.18.pdf
Undecidability
computability theory
many-one reduction
Minsky machines
Fractran
sub-exponential linear logic
Coq
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
19:1
19:17
10.4230/LIPIcs.FSCD.2021.19
article
An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems
Kim, Dohan
1
Lynch, Christopher
1
Clarkson University, Potsdam, NY, USA
Rewriting modulo equations has been researched for several decades but due to the lack of suitable orderings, there are some limitations to rewriting modulo permutation equations. Given a finite set of permutation equations E, we present a new RPO-based ordering modulo E using (permutation) group actions and their associated orbits. It is an E-compatible reduction ordering on terms with the subterm property and is E-total on ground terms. We also present a completion and ground completion method for rewriting modulo a finite set of permutation equations E using our ordering modulo E. We show that our ground completion modulo E always admits a finite ground convergent (modulo E) rewrite system, which allows us to obtain the decidability of the word problem of ground theories modulo E.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.19/LIPIcs.FSCD.2021.19.pdf
Recursive Path Ordering
Permutation Equation
Permutation Group
Rewrite System
Completion
Ground Completion
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
20:1
20:19
10.4230/LIPIcs.FSCD.2021.20
article
Some Axioms for Mathematics
Blanqui, Frédéric
1
https://orcid.org/0000-0001-7438-5554
Dowek, Gilles
1
https://orcid.org/0000-0001-6253-935X
Grienenberger, Émilie
1
Hondet, Gabriel
1
Thiré, François
2
Université Paris-Saclay, ENS Paris-Saclay, LMF, CNRS, Inria, France
Nomadic Labs, Paris, France
The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.20/LIPIcs.FSCD.2021.20.pdf
logical framework
axiomatic theory
dependent types
rewriting
interoperabilty
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
21:1
21:22
10.4230/LIPIcs.FSCD.2021.21
article
Non-Deterministic Functions as Non-Deterministic Processes
Paulus, Joseph W. N.
1
Nantes-Sobrinho, Daniele
2
https://orcid.org/0000-0002-1959-8730
Pérez, Jorge A.
1
3
https://orcid.org/0000-0002-1452-6180
University of Groningen, The Netherlands
University of Brasília, Brazil
CWI, Amsterdam, The Netherlands
We study encodings of the λ-calculus into the π-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider λ^↯_⊕, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider 𝗌π, a π-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of λ^↯_⊕ into 𝗌π and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in λ^↯_⊕ via typed processes in 𝗌π. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.21/LIPIcs.FSCD.2021.21.pdf
Resource calculi
π-calculus
intersection types
session types
linear logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
22:1
22:18
10.4230/LIPIcs.FSCD.2021.22
article
Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor
Veltri, Niccolò
1
https://orcid.org/0000-0002-7230-3436
Department of Software Science, Tallinn University of Technology, Estonia
The finite powerset functor is a construct frequently employed for the specification of nondeterministic transition systems as coalgebras. The final coalgebra of the finite powerset functor, whose elements characterize the dynamical behavior of transition systems, is a well-understood object which enjoys many equivalent presentations in set-theoretic foundations based on classical logic.
In this paper, we discuss various constructions of the final coalgebra of the finite powerset functor in constructive type theory, and we formalize our results in the Cubical Agda proof assistant. Using setoids, the final coalgebra of the finite powerset functor can be defined from the final coalgebra of the list functor. Using types instead of setoids, as it is common in homotopy type theory, one can specify the finite powerset datatype as a higher inductive type and define its final coalgebra as a coinductive type. Another construction is obtained by quotienting the final coalgebra of the list functor, but the proof of finality requires the assumption of the axiom of choice. We conclude the paper with an analysis of a classical construction by James Worrell, and show that its adaptation to our constructive setting requires the presence of classical axioms such as countable choice and the lesser limited principle of omniscience.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.22/LIPIcs.FSCD.2021.22.pdf
type theory
finite powerset
final coalgebra
Cubical Agda
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
23:1
23:19
10.4230/LIPIcs.FSCD.2021.23
article
Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs
Dal Lago, Ugo
1
2
https://orcid.org/0000-0001-9200-070X
Gavazzo, Francesco
1
2
https://orcid.org/0000-0002-2159-0615
University of Bologna, Italy
INRIA Sophia Antipolis, France
We investigate program equivalence for linear higher-order (sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear λ-calculus with explicit copying and algebraic effects à la Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are intensional aspects of computation, with effects, which are, instead, extensional. We review some of the notions of equivalences for linear calculi proposed in the literature and show their limitations when applied to effectful calculi where copying is a first-class citizen. We then introduce resource transition systems, namely transition systems whose states are built over tuples of programs representing the available resources, as an operational semantics accounting for both intensional and extensional interactive behaviours of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.23/LIPIcs.FSCD.2021.23.pdf
algebraic effects
linearity
program equivalence
full abstraction
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
24:1
24:22
10.4230/LIPIcs.FSCD.2021.24
article
Z; Syntax-Free Developments
van Oostrom, Vincent
1
https://orcid.org/0000-0002-4818-7383
Universität Innsbruck, Austria
We present the Z-property and instantiate it to various rewrite systems: associativity, positive braids, self-distributivity, the lambda-calculus, lambda-calculi with explicit substitutions, orthogonal TRSs, .... The Z-property is proven equivalent to Takahashi’s angle property by means of a syntax-free notion of development. We show that several classical consequences of having developments such as confluence, normalisation, and recurrence, can be regained in a syntax-free way, and investigate how the notion corresponds to the classical syntactic notion of development in term rewriting.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.24/LIPIcs.FSCD.2021.24.pdf
rewrite system
confluence
normalisation
recurrence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
25:1
25:22
10.4230/LIPIcs.FSCD.2021.25
article
Recursion and Sequentiality in Categories of Sheaves
Matache, Cristina
1
Moss, Sean
1
Staton, Sam
1
University of Oxford, UK
We present a fully abstract model of a call-by-value language with higher-order functions, recursion and natural numbers, as an exponential ideal in a topos. Our model is inspired by the fully abstract models of O'Hearn, Riecke and Sandholm, and Marz and Streicher. In contrast with semantics based on cpo’s, we treat recursion as just one feature in a model built by combining a choice of modular components.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.25/LIPIcs.FSCD.2021.25.pdf
Denotational semantics
Full abstraction
Recursion
Sheaf toposes
CPOs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
26:1
26:17
10.4230/LIPIcs.FSCD.2021.26
article
Polymorphic Automorphisms and the Picard Group
Hofstra, Pieter
1
Parker, Jason
2
Scott, Philip J.
1
Dept. of Mathematics & Statistics, University of Ottawa, Canada
Department of Mathematics & Computer Science, Brandon University, Canada
We investigate the concept of definable, or inner, automorphism in the logical setting of partial Horn theories. The central technical result extends a syntactical characterization of the group of such automorphisms (called the covariant isotropy group) associated with an algebraic theory to the wider class of quasi-equational theories. We apply this characterization to prove that the isotropy group of a strict monoidal category is precisely its Picard group of invertible objects. Furthermore, we obtain an explicit description of the covariant isotropy group of a presheaf category.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.26/LIPIcs.FSCD.2021.26.pdf
Partial Horn Theories
Monoidal Categories
Definable Automorphisms
Polymorphism
Indeterminates
Normal Forms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
27:1
27:23
10.4230/LIPIcs.FSCD.2021.27
article
What’s Decidable About (Atomic) Polymorphism?
Pistone, Paolo
1
Tranchini, Luca
2
University of Bologna, Italy
Eberhard Karls Universität Tübingen, Germany
Due to the undecidability of most type-related properties of System F like type inhabitation or type checking, restricted polymorphic systems have been widely investigated (the most well-known being ML-polymorphism). In this paper we investigate System Fat, or atomic System F, a very weak predicative fragment of System F whose typable terms coincide with the simply typable ones. We show that the type-checking problem for Fat is decidable and we propose an algorithm which sheds some new light on the source of undecidability in full System F. Moreover, we investigate free theorems and contextual equivalence in this fragment, and we show that the latter, unlike in the simply typed lambda-calculus, is undecidable.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.27/LIPIcs.FSCD.2021.27.pdf
Atomic System F
Predicative Polymorphism
ML-Polymorphism
Type-Checking
Contextual Equivalence
Free Theorems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
28:1
28:19
10.4230/LIPIcs.FSCD.2021.28
article
Coalgebra Encoding for Efficient Minimization
Deifel, Hans-Peter
1
https://orcid.org/0000-0002-9542-9664
Milius, Stefan
1
https://orcid.org/0000-0002-2021-1644
Wißmann, Thorsten
2
https://orcid.org/0000-0001-8993-6486
Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Radboud University Nijmegen, The Netherlands
Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.28/LIPIcs.FSCD.2021.28.pdf
Coalgebra
Partition refinement
Transition systems
Minimization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
29:1
29:23
10.4230/LIPIcs.FSCD.2021.29
article
On the Logical Strength of Confluence and Normalisation for Cyclic Proofs
Das, Anupam
1
https://orcid.org/0000-0002-0142-3676
University of Birmingham, UK
In this work we address the logical strength of confluence and normalisation for non-wellfounded typing derivations, in the tradition of "cyclic proof theory". We present a circular version CT of Gödel's system T, with the aim of comparing the relative expressivity of the theories CT and T. We approach this problem by formalising rewriting-theoretic results such as confluence and normalisation for the underlying "coterm" rewriting system of CT within fragments of second-order arithmetic.
We establish confluence of CT within the theory RCA₀, a conservative extension of primitive recursive arithmetic and IΣ1. This allows us to recast type structures of hereditarily recursive operations as "coterm" models of T. We show that these also form models of CT, by formalising a totality argument for circular typing derivations within suitable fragments of second-order arithmetic. Relying on well-known proof mining results, we thus obtain an interpretation of CT into T; in fact, more precisely, we interpret level-n-CT into level-(n+1)-T, an optimum result in terms of abstraction complexity.
A direct consequence of these model-theoretic results is weak normalisation for CT. As further results, we also show strong normalisation for CT and continuity of functionals computed by its type 2 coterms.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.29/LIPIcs.FSCD.2021.29.pdf
confluence
normalisation
system T
circular proofs
reverse mathematics
type structures
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
30:1
30:19
10.4230/LIPIcs.FSCD.2021.30
article
Abstract Clones for Abstract Syntax
Arkor, Nathanael
1
https://orcid.org/0000-0002-4092-7930
McDermott, Dylan
2
https://orcid.org/0000-0002-6705-1449
University of Cambridge, UK
Reykjavik University, Iceland
We give a formal treatment of simple type theories, such as the simply-typed λ-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed λ-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as β- and η-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.30/LIPIcs.FSCD.2021.30.pdf
simple type theories
abstract clones
second-order abstract syntax
substitution
variable binding
presentations
free algebras
induction
logical relations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
31:1
31:22
10.4230/LIPIcs.FSCD.2021.31
article
Tuple Interpretations for Higher-Order Complexity
Kop, Cynthia
1
https://orcid.org/0000-0002-6337-2544
Vale, Deivid
1
https://orcid.org/0000-0003-1350-3478
Department of Software Science, Radboud University Nijmegen, The Netherlands
We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are mapped to tuples of natural numbers and higher-order terms to functions between those tuples. Tuples may carry information relevant to the type; for instance, a term of type nat may be associated to a pair ⟨ cost, size ⟩ representing its evaluation cost and size. This class of interpretations results in a more fine-grained notion of complexity than runtime or derivational complexity, which makes it particularly useful to obtain complexity bounds for higher-order rewriting systems.
We show that rewriting systems compatible with tuple interpretations admit finite bounds on derivation height. Furthermore, we demonstrate how to mechanically construct tuple interpretations and how to orient β and η reductions within our technique. Finally, we relate our method to runtime complexity and prove that specific interpretation shapes imply certain runtime complexity bounds.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.31/LIPIcs.FSCD.2021.31.pdf
Complexity
higher-order term rewriting
many-sorted term rewriting
polynomial interpretations
weakly monotonic algebras
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2021-07-06
195
32:1
32:22
10.4230/LIPIcs.FSCD.2021.32
article
Output Without Delay: A π-Calculus Compatible with Categorical Semantics
Sakayori, Ken
1
https://orcid.org/0000-0003-3238-9279
Tsukada, Takeshi
2
https://orcid.org/0000-0002-2824-8708
The University of Tokyo, Japan
Chiba University, Japan
The quest for logical or categorical foundations of the π-calculus (not limited to session-typed variants) remains an important challenge. A categorical type theory correspondence for a variant of the i/o-typed π-calculus was recently revealed by Sakayori and Tsukada, but, at the same time, they exposed that this categorical semantics contradicts with most of the behavioural equivalences. This paper diagnoses the nature of this problem and attempts to fill the gap between categorical and operational semantics. We first identify the source of the problem to be the mismatch between the operational and categorical interpretation of a process called the forwarder. From the operational viewpoint, a forwarder may add an arbitrary delay when forwarding a message, whereas, from the categorical viewpoint, a forwarder must not add any delay when forwarding a message. Led by this observation, we introduce a calculus that can express forwarders that do not introduce delay. More specifically, the calculus we introduce is a variant of the π-calculus with a new operational semantics in which output actions are forced to happen as soon as they get unguarded. We show that this calculus (i) is compatible with the categorical semantics and (ii) can encode the standard π-calculus.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.32/LIPIcs.FSCD.2021.32.pdf
π-calculus
categorical semantics
linear approximation