## Announcement

It is our pleasure to announce that the 15th workshop Computational Logic and Applications CLA'20 will be held on the 12th and 13th of October 2020. Since the physical version of the workshop had to be cancelled this year due to the global pandemic, this edition of CLA will be held on-line to help the community stay in touch.

The main purpose of CLA is to provide an open, free access forum for scientific research concentrated around combinatorial and quantitative aspects of mathematical logic and their applications in computer science.

We cordially invite all researchers interested in topics such as:

• combinatorics of lambda calculus and related formalisms,
• quantitative aspects of program evaluation and normalisation,
• asymptotic enumeration in computational logic,
• statistical properties of formulae, terms and programs,
• random generation of large combinatorial structures in computational logic,
• randomness in software testing and counter-example generation methods.

## Invited speakers

• Mirai Ikebuchi (Massachusetts Institute of Technology)

Homological Methods in Rewriting

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. In this talk, we will see a way to find a lower bound of the number of axioms. The inequality that gives the lower bound is obtained by analyzing the algebraic structure, called the homology group, associated with the given equational theory. I will explain how equational theories and rewriting systems relate to abstract algebra, what homology groups in general settings are like, and what the homology groups of equational theories give us.

• Marc Noy (Universitat Politècnica de Catalunya)

Limiting probabilities of first order sentences in sparse random graphs

Given a class of random graphs $G$ and a first order property $A$, we consider the limiting probability that $A$ is satisfied in $G$ when the number of vertices goes to infinity. In the classical random graph model $G(n,p=c/n)$ in the sparse regime, we find a critical value $c' \sim 0.93$ such that the set of limiting probabilities is dense in the interval $[0,1]$ if and only if $c > c'$. We will sketch the proof of this result and will discuss its extension to sparse hypergraphs and other models of random sparse random graphs.

(Joint work with Alberto Larrauri and Tobias Müller)

## Contributed talks

• Maciej Bendkowski
A note on the asymptotic expressiveness of ZF and ZFC
• Olivier Bodini, Alexandros Singh and Noam Zeilberger
Distribution of Parameters in Certain Fragments of the Linear and Planar λ-calculus
• Andrew Elvey Price, Wenjie Fang and Michael Wallner
Compacted binary trees admit stretched exponentials
• Antoine Genitrini
Reduced Ordered Binary Decision Diagrams as compacted tree-structures: Enumeration and Sampling
• Katarzyna Grygiel and Guan-Ru Yu
In search of a bijection between β-normal 3-indecomposable planar lambda terms and β(0,1)-trees
• Michaël Moortgat
The Tamari order for $D^3$ and derivability in semi-associative Lambek-Grishin Calculus
• Martin Pépin
Statistical Analysis of Non-Deterministic Fork-Join Processes
• Ryoma Sin'Ya
A quantitative approach to the primitive words conjecture
• Richard Statman
Algebraic and combinatorial structures intrinsic to functional programming
• Paul Tarau and Valeria de Paiva
Training Neural Networks as Theorem Provers via the Curry-Howard Isomorphism

## Open problem session

The aim of this session is not only to encourage participants to present the problems they are currently struggling with, but also to provide an opportunity for collaborative brainstorming. Everyone interested in sharing an open problem is asked to send a short presentation in pdf (preferably 2-3 slides) to grygiel@tcs.uj.edu.pl up to two days before the workshop starts.

During the open problem session all contributors briefly present their problems and next everyone is invited to join discussions on separate channels, each devoted to a different problem. Depending on the number of submissions, one or two time slots are planned for discussion.

## Program

The schedule is also available in the ics format.

Be careful: All the times below are given in Coordinated Universal Time (UTC).

#### Monday, October 12th

7:30-7:45 UTC  Welcome and brief technical overview

7:45-8:00 UTC  Pierre Lescanne and Marek Zaionc
A brief history of CLA

We would like to present breaking points in the short history of CLA from the very beginning in 2001 till now. We would like also to remind problems which have been inspiration for us.

Video      Photos from 2004 and 2005

8:15-8:50 UTC  Ryoma Sin'ya
A quantitative approach to the primitive words conjecture

A non-empty word $w$ is said to be primitive if it is not a power of a shorter words, i.e., ($w \neq u^n$ for any $|u| < |w|$ and $n > 1$). The notion of primitivity of words plays a central role in algebraic coding theory and combinatorics on words. Whether the set of all primitive words $Q$ is context-free or not is a well-known long-standing open problem posed by Dömösi, Horváth and Ito in 1991.

In this talk, we give a brief intuition why this problem is hard to solve, based on a quantitative observation. In particular, we describe a special quantitative property that, although $Q$ is "very large" (i.e., density one), any regular subset of $Q$ is "very small" (i.e., density zero).

Slides      Video

9:00-9:35 UTC  Michaël Moortgat
The Tamari order for $D^3$ and derivability in semi-associative Lambek-Grishin Calculus

This is work in progress on extending the Tamari order for the two-dimensional Dyck language $D^2$ of well-balanced parentheses to the three-dimensional case, and on modelling the Tamari order for $D^3$ in terms of derivability in an extended version of Lambek's (1961) Syntactic Calculus going back to V.N. Grishin (1983).

Extended abstract      Slides      Video

9:45-10:35 UTC  Marc Noy
(Invited talk) Limiting probabilities of first order sentences in sparse random graphs

Given a class of random graphs $G$ and a first order property $A$, we consider the limiting probability that $A$ is satisfied in $G$ when the number of vertices goes to infinity. In the classical random graph model $G(n,p=c/n)$ in the sparse regime, we find a critical value $c' \sim 0.93$ such that the set of limiting probabilities is dense in the interval $[0,1]$ if and only if $c > c'$. We will sketch the proof of this result and will discuss its extension to sparse hypergraphs and other models of random sparse random graphs.

(Joint work with Alberto Larrauri and Tobias Müller)

Slides      Video

10:35-12:00 UTC  Lunch break

12:00-12:35 UTC  Katarzyna Grygiel and Guan-Ru Yu
In search of a bijection between $\beta$-normal 3-indecomposable planar lambda terms and $\beta$(0,1)-trees

During his CLA 2019 talk, Noam Zeilberger posed the following conjecture: β-normal internally 3-edge-connected planar lambda terms are counted by the OEIS sequence A000257. This very sequence is already known to enumerate other structures, among others β(0,1)-trees, i.e., rooted plane trees whose nodes are labeled with non-negative integers in the following way:

• leaves have label 0;
• the label of the root is one more than the sum of its children’s labels;
• the label of any other node exceeds the sum of its children’s labels by at most one.
In our talk we aim at presenting our approaches to find a constructive bijection between these two families of objects. So far, we have managed to find out some building blocks that, when smartly combined together, hopefully could lead us to establish a full recursive procedure for the translation in question. We strongly believe that our ideas can be further expanded and we count on the interaction with the audience.

Extended abstract      Slides      Video

12:45-13:20 UTC  Olivier Bodini, Alexandros Singh and Noam Zeilberger
Distribution of Parameters in Certain Fragments of the Linear and Planar $\lambda$-calculus

The combinatorial aspects of lambda calculus are an active area of research, having various interactions with subjects such as the study of combinatorial maps.

We focus on the linear and planar lambda calculus and various fragments thereof, including open and closed terms, as well as restrictions to terms having no proper closed subterms (known as bridgeless terms).

We present an analysis of some basic parameters of these classes of lambda terms. For open linear, planar, and bridgeless planar lambda terms, we discuss the limit distributions of free variables. For closed linear lambda terms we furthermore discuss the limit distributions of identity-subterms and closed subterms, as well as the asymptotic probability that a random such term is an abstraction. Finally, for open planar and bridgeless planar lambda terms we discuss the asymptotic probabilities of such random terms being abstractions.

The above serve to illuminate typical aspects of large random linear, planar, and bridgeless planar lambda terms.

Extended abstract      Slides      Video

13:30-14:20 UTC  Mirai Ikebuchi
(Invited talk) Homological Methods in Rewriting

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. In this talk, we will see a way to find a lower bound of the number of axioms. The inequality that gives the lower bound is obtained by analyzing the algebraic structure, called the homology group, associated with the given equational theory. I will explain how equational theories and rewriting systems relate to abstract algebra, what homology groups in general settings are like, and what the homology groups of equational theories give us.

Slides      Video

15:15-17:00 UTC  Open problem session 1

Open problems by Richard Statman

Open problem by Noam Zeilberger

#### Tuesday, October 13th

7:45-8:20 UTC  Martin Pépin
Statistical Analysis of Non-Deterministic Fork-Join Processes

I will present a study of the combinatorial structure of concurrent programs with non-deterministic choice and a fork-join style of coordination. As a first step I will establish a link between these concurrent programs and a class of combinatorial structures. Based on this combinatorial interpretation, I develop algorithms aimed at the statistical exploration of the state-space ofprograms. The first algorithm is a uniform random sampler of bounded executions, providing a suitable default exploration strategy. The second algorithm is a random sampler of execution prefixes that allows to control the exploration with respect to the uniform distribution. The fundamental characteristic of these algorithms is that they work on the control graph of the programs and not directly on their state-space, thus providing a way to tackle the state explosion problem.

Extended abstract      Slides      Video      Paper      Implementation

8:30-9:05 UTC  Antoine Genitrini
Reduced Ordered Binary Decision Diagrams as compacted tree-structures: Enumeration and Sampling

Extended abstract      Slides      Video

9:15-9:50 UTC  Andrew Elvey Price, Wenjie Fang and Michael Wallner
Compacted binary trees admit stretched exponentials

A compacted binary tree is a directed acyclic graph encoding a binary tree in which common subtrees are factored and shared, such that they are represented only once. We show that the number of compacted binary trees of size $n$ is asymptotically given by

$\Theta ( n! 4^n e^{3 a_1 n^{1/3}} n^{3/4} ),$
where $a_1$ is the largest root of the Airy function and approximately equal to $-2.338$. Our method involves a new two parameter recurrence which yields an algorithm of quadratic arithmetic complexity for computing the number of compact trees of a given size. We use empirical methods to estimate the values of all terms defined by the recurrence, then we prove by induction that these estimates are sufficiently accurate for large $n$ to determine the asymptotic form of the number of compacted trees. With the same method, we also prove a similar asymptotic form of the number of minimal finite automata recognizing a finite language on a binary alphabet showing the appearance of a stretched exponential.

Extended abstract      Slides      Video

10:00-11:00 UTC  Open problem session 2

Open problem Keisuke Nakano

Video with open problems by Keisuke Nakano and Ryoma Sin'ya

11:00-12:00 UTC  Lunch Break

12:00-12:35 UTC  Maciej Bendkowski
A note on the asymptotic expressiveness of ZF and ZFC

We investigate the asymptotic densities of theorems provable in Zermelo-Fraenkel set theory ZF and its extension ZFC including the axiom of choice. Assuming a canonical De Bruijn representation of formulae, we construct asymptotically large sets of sentences unprovable within ZF, yet provable in ZFC. Furthermore, we link the asymptotic density of ZFC theorems with the provable consistency of ZFC itself. Consequently, if ZFC is consistent, it is not possible to refute the existence of the asymptotic density of ZFC theorems within ZFC. Both these results address a recent question by Zaionc regarding the asymptotic equivalence of ZF and its extension ZFC.

Extended abstract      Slides

12:45-13:20 UTC  Richard Statman
Algebraic and combinatorial structures intrinsic to functional programming

Somewhat eccentric survey of our work in the area of algebraic and combinatorial structures intrinsic to functional programming

Extended abstract      Slides      Video

13:30-14:05 UTC  Paul Tarau and Valeria de Paiva
Training Neural Networks as Theorem Provers via the Curry-Howard Isomorphism

Extended abstract      Slides      Video

## Registration

Registration is now open!

Please remember to register early enough to obtain all links required to join the event.

## Submission

Talk proposals should consist of short abstracts (at most 2 pages) describing work-in-progress or previously published work, and can be written in either plain text or pdf format. They will be evaluated by the program committee to determine interest and scope, so talk proposals should give some indication of the relevance to CLA in case this is not immediately obvious. You can also indicate whether you prefer to give a live or pre-recorded talk and the amount of time you would like to speak, although this is left up to the discretion of the program committee.

Submission is done through EasyChair.

## Technical information

As with past editions of CLA, we plan to have both invited and contributed talks, with the opportunity to present either work-in-progress or recently published work in a friendly and informal setting... The only difference is that CLA 2020 will be entirely online! During the workshop we will have live talks mixed with text-based discussions.

## Important dates

• August 31 September 7, 2020 (AoE): submission deadline for talk proposals
• September 14 September 21, 2020 (AoE): speaker notification
• October 11, 2020: registration deadline
• October 12-13, 2020: workshop

## Committees

Steering Committee

Program Committee

Organizing Committee

## List of participants

1. Nicolas Behr (Université de Paris, CNRS, IRIF)
2. Maciej Bendkowski (Jagiellonian University)
3. Olivier Bodini (LIPN, Université Sorbonne Paris Nord)
4. Spencer Breiner (NIST)
5. Julien Clément (CNRS, GREYC, Caen, France)
6. Julien Courtiel (University of Caen Normandie)
7. Matthieu Dien (University of Caen Normandie)
8. Boris Djalal (INRIA)
9. Sergey Dovgal (Université de Bordeaux)
10. Uli Fahrenberg (LIX, École polytechnique)
11. Wenjie Fang (LIGM - Université Gustave Eiffel)
12. Danièle Gardy (Université de Versailles Saint-Quentin)
13. Antoine Genitrini (Sorbonne University)
14. Alain Giorgetti (Institut FEMTO-ST)
15. Katarzyna Grygiel (Jagiellonian University)
16. Youssef El Habouz (Université de Rennes 1)
17. Kei Hibino (Idein Inc.)
18. Mirai Ikebuchi (MIT)
19. Assaf Kfoury (Computer Science Department, Boston University)
20. Toshihiro Koga
21. Konstantinos Kogkalidis (Utrecht University)
22. Pierre Lescanne (ENS de Lyon)
23. Orestis Melkonian (University of Edinburgh)
24. Paul-Andre Mellies (CNRS, Universite de Paris)
25. Michael Moortgat (Utrecht University)
26. Mehdi Naima (Université Sorbonne Paris Nord)
27. Yoshiki Nakamura (Tokyo Institute of Technology)
28. Keisuke Nakano (Tohoku University)
29. Lê Thành Dũng (Tito) Nguyễn (Laboratoire d'informatique de Paris Nord)
30. Marc Noy (Universitat Politècnica de Catalunya in Barcelona)
31. Valeria de Paiva (Topos Institute)
32. Martin Pépin (Sorbonne Université)
33. Jason Reed (GitHub, Inc.)
34. Thomas Seiller (CNRS)
35. Nobutaka Shimizu (The University of Tokyo)
36. Alexandros Singh (LIPN, Université Sorbonne Paris Nord)
37. Ryoma Sin'ya (Akita University)
38. Richard Statman (Carnegie Mellon University)
39. Tadaaki Tanimoto (Sony LSI Design, Inc.)
40. Niccolò Veltri (Tallinn University of Technology)
41. Michael Wallner (TU Wien)
42. Ali Younes (Ecole Polytechnique)
43. Guan-Ru Yu (Academia Sinica, Taiwan)
44. Takao Yuyama (Tokyo Institute of Technology, Japan)
45. Marek Zaionc (Theoretical Computer Science, Jagiellonian University)
46. Noam Zeilberger (Ecole Polytechnique)

## History

Below you can find the exhaustive list of previous CLA editions: