15th Workshop

12-13 October 2020

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.

- 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)

- 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*

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.

The schedule is also available in the ics format.

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

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 Dömösi, Horvá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).

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)

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.

**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.

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

**Open problems by Richard Statman**

**Open problem by Noam Zeilberger**

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

**Extended abstract
Slides
Video**

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

**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.

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**

14:30-15:30 UTC **Business meeting**

Registration is now **open**!

Click here
to register your intention to participate. Virtual attendance is *free* upon registration.

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

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.

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.

For detailed information on technologies to be used please click here.

Steering Committee

- Antoine Genitrini (Sorbonne University, Paris, France)
- Alain Giorgetti (University of Bourgogne Franche-Comté, Besançon, France)
- Bernhard Gittenberger (TU Wien, Austria)
- Katarzyna Grygiel (Jagiellonian University, Kraków, Poland)
- Michał Pałka (Chalmers University of Technology, Gothenburg, Sweden)
- Noam Zeilberger (Ecole Polytechnique, Paris, France)

Program Committee

- Maciej Bendkowski (Jagiellonian University, Kraków, Poland)
- Olivier Bodini (Université Sorbonne Paris Nord, France)
- Joulien Courtiel (Université de Caen, France)
- Antoine Genitrini (Sorbonne University, Paris, France)
- Alain Giorgetti (University of Bourgogne Franche-Comté, Besançon, France)
- Bernhard Gittenberger (TU Wien, Austria)
- Katarzyna Grygiel - co-chair (Jagiellonian University, Kraków, Poland)
- Leonidas Lampropoulos (University of Maryland, USA)
- Ryoma Sin'ya (Akita University, Japan)
- Michael Wallner (TU Wien, Austria)
- Noam Zeilberger - co-chair (Ecole Polytechnique, Paris, France)

Organizing Committee

- Katarzyna Grygiel (Jagiellonian University, Kraków, Poland)
- Alexandros Singh (Université Sorbonne Paris Nord, France)
- Noam Zeilberger (Ecole Polytechnique, Paris, France)

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

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

- 2019, Versailles (France)
- 2018, Paris (France)
- 2017, Göteborg (Sweden)
- 2016, Novi Sad (Serbia)
- 2015, Lyon (France)
- 2012, Kraków (Poland)
- 2011, Wien (Austria)

- 2010, Kraków (Poland)
- 2009, Lyon (France)
- 2008, Kraków (Poland)
- 2007, Kraków (Poland)
- 2005, Chambery (France)
- 2004, Lyon (France)
- 2002, Kraków (Poland)