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:
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.
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)
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:
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
Program Committee
Organizing Committee
Below you can find the exhaustive list of previous CLA editions: