Announcement

It is our pleasure to announce that the 14th workshop Computational Logic and Applications CLA'19 will be held on the 1st and 2nd of July 2019 in Versailles, France. 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.

Local Committee

Steering Committee

Invited speakers

  • Samuele Giraudo (LIGM, Univ. Marne-la-Vallée, France)

      Combinatorial operads, rewrite systems, and formal grammars

    Term rewrite systems appear in several domains of mathematics and computer science. They can be used for instance as models of computation in computer science or as devices to compute over operations in abstract algebra. Here, we focus on operads, that are algebraic structures formalizing the notion of operations with several inputs and one output. The objects of free operads can be seen as planar rooted trees (or linear terms on some alphabet). We explore here some links between operad theory and combinatorics and in particular with enumeration theory. We also explain how operads lead to a generalization of both context-free grammars and regular tree grammars in order to specify languages of various sorts of combinatorial objects (and not only of words or trees).

  • Clemens Grabmayer (Gran Sasso Science Institute, L'Aquila, Italy)

     Modeling Terms in the Lambda-Calculus with letrec (by Term Graphs and Finite-State Automata)

    My aim is to demonstrate the usefulness of graph representations for lambda terms with the recursion construct lectrec that go beyond those that are used in standard compilers and reduction engines for functional programming languages. I will explain representations of lambda-letrec terms as term graphs and finite-state automata that not only (i) are faithful to the unfolding semantics of terms (like graphs used by reduction engines), but also (ii) facilitate the use of the standard methods such as bisimulation collapse/checking and DFA-minimization/equivalence-testing (unlike graphs used by reduction engines). The chosen representations stay close to the term notation: they employ scope-sharing, but not the costly context-sharing mechanisms from optimal lambda reduction. They make it easy to go from terms to graphs, and back again.

    I will motivate these graph representations by a rewrite system for parsing the scope structure of lambda terms. It yields a characterization of those infinite lambda-terms that are the unfolding semantics of lambda-letrec terms: strongly regular infinite lambda-terms with a regular structure, and finitely entangled, nested scopes.

    The main part of my talk will concern the definition, and efficient implementation of maximal sharing for functional programs in their core language, the lambda calculus with letrec. I will show how terms with lambda-bindings and recursion can be represented by, appropriately defined, higher-order term graphs, that those can be encoded as first- order term graphs, and that these in turn can be represented as deterministic finite-state automata (DFAs). Via these correspondences and DFA-minimization, maximally shared forms of higher-order terms can be computed. I will explain the complexity of these methods, and demon- strate a Haskell implementation that we have developed for that purpose.

    Time permitting, I will also describe a conceptual abstraction of the scope-sharing graph respresentations for lambda-letrec terms in the form of `nested term graphs'.

    The results I will present have been obtained in framework of the research project ROS at Utrecht University together with Jan Rochel, those on nested term graphs together with Vincent van Oostrom.

Important dates

Deadlines are midnight anywhere-on-earth.

  • June 11, 2019: submission deadline for talk proposals
  • June 14, 2019: speaker notification for workshop
  • June 24, 2019: registration deadline
  • July 1-2, 2019: workshop
  • September 30, 2019: submission deadline for contributions to the DMTCS special issue.

Program

  Monday, July 1st

  9:00-9:20 Welcome breakfast

9:20-10:30 Samuele Giraudo (slides)
(Invited talk) Combinatorial operads, rewrite systems, and formal grammars

Term rewrite systems appear in several domains of mathematics and computer science. They can be used for instance as models of computation in computer science or as devices to compute over operations in abstract algebra. Here, we focus on operads, that are algebraic structures formalizing the notion of operations with several inputs and one output. The objects of free operads can be seen as planar rooted trees (or linear terms on some alphabet). We explore here some links between operad theory and combinatorics and in particular with enumeration theory. We also explain how operads lead to a generalization of both context-free grammars and regular tree grammars in order to specify languages of various sorts of combinatorial objects (and not only of words or trees).

  10:30-11:00 Coffee and tea break

11:00-11:35 George Kaye (slides)
A visualiser for linear lambda terms as 3-valent rooted maps

This talk will present and demonstrate a set of online tools to aid in the systematic exploration of the topological properties of linear lambda-terms when represented as 3-valent rooted maps. The first tool is a lambda-term visualiser, which visualises a lambda-term specified by the user as a rooted map on the screen. There is also functionality related to the normalisation of terms: terms can be reduced to their normal form, or a normalisation graph can be viewed. The visualiser is complemented by a lambda-term gallery, which can generate and display terms that satisfy criteria specified by the user, such as number of crossings in their corresponding maps. These tools can be used for a variety of different applications, including: examining the structure of different terms; disproving conjectures regarding various subsets of the lambda calculus; or investigating special normalisation properties held by different sets of lambda-terms. The tools can be found at https://www.georgejkaye.com/fyp.

11:35-12:10 Frédéric Voisin and Marie-Claude Gaudel (slides)
Drawing uniformly at random in dynamic sets of paths

Random generation of combinatorial structures can be used for model-based automatic generation of tests or traces: previous works have reported on their successful application to randomised structural program testing or probabilistic exploration of very large models. In the case of structural program testing, random generation is used to first draw a set of paths in the control flow graph of the program. Then, some solver is used for trying to derive input values to traverse these paths during runs of the program: this process is incremental, collecting the conditions encountered when traversing the path and trying to solve their conjunction. A well-known problem is that not all paths of the control flow graph correspond to feasible runs. When an unfeasible path is drawn, it is simply discarded and another path is drawn. This is a severe limitation in the case of programs with a high ratio of infeasible paths. We show how to improve the method by using for the drawing the information about paths already drawn, more precisely the infeasible prefixes already detected. In addition to the counting table used by the recursive method for uniformly generating combinatorial structures, we introduce a trie structure that allows to exclude all paths with an already detected infeasible prefix. Our derived drawing algorithm is uniform among all paths that do not have a known infeasible prefix. Due to the fact that the number of extensions of infeasible prefixes may be (and is often) large, their elimination from the subsequent drawings is a substantial improvement w.r.t. the classical rejection method. Preliminary experiments are reported and commented.

12:10-12:45 Martin Mariusz Lester (slides)
Understanding the Expressive Power of Unhygienic Substitution in Metaprogramming via Combinatory Logic

We consider the extension of Kiselyov's recent combinatory logic semantics for open lambda terms to calculi with support for metaprogramming, in particular Davies and Pfenning's $\lambda_e^{\rightarrow \Box}$ and Choi and others' $\lambda_S$. We conclude that there is quantitative evidence to support the intuitive belief that unhygienic code substitution adds significant power to a metaprogramming language.

  12:45-14:30 Lunch Break

14:30-15:20 Paul Tarau (slides)
Formula Transformers And Combinatorial Test Generators for Propositional Intuitionistic Theorem Provers

We develop combinatorial test generation algorithms for progressively more powerful theorem provers, covering formula languages ranging from the implicational fragment of intuitionistic logic to full intuitionistic propositional logic. Our algorithms support exhaustive and random generators for formulas of these logics. To provide known-to-be-provable formulas, via the Curry-Howard formulas-as-types correspondence, we use generators for simply-typed lambda terms and combinator expressions. Besides generators for several classes of formulas, we design algorithms that restrict formula generation to canonical representatives of logical equivalence classes and introduce program transformations that reduce formulas to equivalent formulas of a simpler structure. To test the effectiveness of the testing framework itself, we describe use cases for deriving lightweight theorem provers for several of these logics. In particular, we find out that our provers, after preprocessing from disjunction-free formulas to a Nested Horn Clause form achieve $O(n~log(n))$ space complexity without the need to introduce new variables.

15:20-16:10 Liugi Santocanale (slides)
Algebraic logic of paths

Discrete paths in the plane (with North and East steps) from $(0, 0)$ to some point $(n,m)$ are among the most studied objects in enumerative combinatorics [8, 1]; we denote by $P(n,m)$ the set of these paths. It is a curious fact that the sets $P(n, m)$ are also important algebraic models for several kinds of logics. It is well-known that these paths form, under the dominance ordering, a finite distributive lattice, whence a Heyting algebra [4, 3, 11]. It is less known that these paths all together form a quantaloid, that is a category where objects are the positive integers and whose homsets are the lattices $P(n,m)$. This structure arise via the bijection between paths in $P(n, m)$ and order-preserving functions from the chain $\{1,\ldots,n\}$ to the chain $\{0,1,\ldots,m\}$. This is a (non- commutative) star-autonomous quantaloid, where the star (i.e. the duality) is given by reflection along the diagonal. In particular, $P(n,n)$ is an involutive residuated lattice, that is, an algebraic model of non-commutative classical linear logic, see e.g. [10, 7].

In this talk, I’ll firstly introduce the star-autonomous structure and show how this structure has been fruitfully exploited in [5] to construct a continuous generalization both of the weak Bruhat order and of the multinomial lattices [2]. I’ll show then how the combinatorial interpretation of the composition in the world of paths yields bijective proofs of counting results due to Howie [6] and Laradji and Umar [9] and, also, new combinatorial identities [12].

References

  • [1] C. Banderier and P. Flajolet. Basic analytic combinatorics of directed lattice paths. Theoretical Computer Science, 281(1):37–80, 2002.
  • [2] M. K. Bennett and G. Birkhoff. Two families of Newman lattices. Algebra Universalis, 32(1):115–144, 1994.
  • [3] L. Ferrari. Dyck algebras, interval temporal logic, and posets of intervals. SIAM J. Discrete Math., 30(4):1918–1937, 2016.
  • [4] L. Ferrari and R. Pinzani. Lattices of lattice paths. J. Statist. Plann. Inference, 135(1):77–92, 2005.
  • [5] M. J. Gouveia and L. Santocanale. The continuous weak order. Preprint., Dec. 2018.
  • [6] J. M. Howie. Products of idempotents in certain semigroups of transformations. Proc. Edinburgh Math. Soc., 17(2):223–236, 1971.
  • [7] P.Jipsen. Relational algebras, idempotent semirings and generalized bunched implication algebras. In Relational and algebraic methods in Computer Science, volume 10226 of Lecture Notes in Comput. Sci., pages 144–158. Springer, Cham, 2017.
  • [8] C. Krattenthaler. The enumeration of lattice paths with respect to their number of turns. In Advances in Combinatorial Methods and Applications to Probability and Statistics, Stat. Ind. Technol., pages 29–58. Birkhäuser Boston, Boston, MA, 1997.
  • [9] A. Laradji and A. Umar. Combinatorial results for semigroups of order-preserving full transformations. Semigroup Forum, 72(1):51–62, 2006.
  • [10] G. Meloni and L. Santocanale. Relational semantics for distributive linear logic. Available from HAL: https://hal.archives-ouvertes.fr/hal-01851509, Aug. 1995.
  • [11] H. Mühle. A Heyting algebra on Dyck paths of type A and B. Order, 34(2):327– 348, 2017.
  • [12] L. Santocanale. On idempotent discrete paths. In Proceedings of the conference Words, June 2019. To appear.

  16:10-16:40 Coffee and tea break

16:40-17:15 Noam Zeilberger and Jason Reed (slides)
Some topological properties of planar lambda terms

We consider the subsystem of $λ$-calculus consisting of terms which are both linear (every variable used exactly once) and ordered (variables used in the order they are bound). Although this restriction may seem quite draconian, it has a natural logical interpretation, and moreover, it turns out that such terms are in one-to-one correspondence with (rooted) planar 3-valent maps. The latter have been objects of intense study going back to the 19th century, giving an indication that what might at first appear to be a very meager fragment of $λ$-calculus is in fact rich with mathematical structure.

In the talk, I will begin by presenting some background on planar $λ$-calculus, as well as on the correspondence between planar terms and rooted planar 3-valent maps that arises as the restriction of a bijection by Bodini, Gardy, and Jacquot (2013). Then I will discuss work-in-progress with Jason Reed where we take this correspondence seriously and attempt to better understand the topological structure of planar lambda terms, focusing on a logical characterization of $k$-connected terms (for $k=2,3,4$).

  17:30-18:30 Business meeting

  20:00 Dinner

  Tuesday, July 2nd

  9:00-9:20 Welcome breakfast

9:20-10:30 Clemens Grabmayer (slides)
(Invited talk) Modeling Terms in the Lambda-Calculus with letrec (by Term Graphs and Finite-State Automata)

My aim is to demonstrate the usefulness of graph representations for lambda terms with the recursion construct lectrec that go beyond those that are used in standard compilers and reduction engines for functional programming languages. I will explain representations of lambda-letrec terms as term graphs and finite-state automata that not only (i) are faithful to the unfolding semantics of terms (like graphs used by reduction engines), but also (ii) facilitate the use of the standard methods such as bisimulation collapse/checking and DFA-minimization/equivalence-testing (unlike graphs used by reduction engines). The chosen representations stay close to the term notation: they employ scope-sharing, but not the costly context-sharing mechanisms from optimal lambda reduction. They make it easy to go from terms to graphs, and back again.

I will motivate these graph representations by a rewrite system for parsing the scope structure of lambda terms. It yields a characterization of those infinite lambda-terms that are the unfolding semantics of lambda-letrec terms: strongly regular infinite lambda-terms with a regular structure, and finitely entangled, nested scopes.

The main part of my talk will concern the definition, and efficient implementation of maximal sharing for functional programs in their core language, the lambda calculus with letrec. I will show how terms with lambda-bindings and recursion can be represented by, appropriately defined, higher-order term graphs, that those can be encoded as first- order term graphs, and that these in turn can be represented as deterministic finite-state automata (DFAs). Via these correspondences and DFA-minimization, maximally shared forms of higher-order terms can be computed. I will explain the complexity of these methods, and demon- strate a Haskell implementation that we have developed for that purpose.

Time permitting, I will also describe a conceptual abstraction of the scope-sharing graph respresentations for lambda-letrec terms in the form of `nested term graphs'.

The results I will present have been obtained in framework of the research project ROS at Utrecht University together with Jan Rochel, those on nested term graphs together with Vincent van Oostrom.

  10:30-11:00 Coffee and tea break

11:00-11:35 Asada, Kazuyuki and Kobayashi, Naoki and Sin'ya, Ryoma and Tsukada, Takeshi (slides)
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence

It is well known that the length of a $\beta$-reduction sequence of a simply typed $\lambda$-term of order $k$ can be huge; it is as large as $k$-fold exponential in the size of the $\lambda$-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst case: how many simply typed $\lambda$-terms have very long reduction sequences? In this talk, we provide a partial answer to this question, by showing that asymptotically almost every simply typed $\lambda$-term of order $k$ has a reduction sequence as long as $k$-fold exponential in the term size, under the assumption that the arity of functions and the number of variables that may occur in every subterm are bounded above by a constant. To prove it, we have extended the infinite monkey theorem for words to a parameterized one for regular tree languages, which may be of independent interest. The work has been motivated by quantitative analysis of the complexity of higher-order model checking. The content of this talk is based on our previous papers [1].

[1] Asada, Kazuyuki and Kobayashi, Naoki and Sin'ya, Ryoma and Tsukada, Takeshi: "Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence", Logical Methods in Computer Science, Volume 15, Issue 1, 2019 (a preliminary version appeared in FoSSaCS 2017).

11:35-12:10 Katarzyna Grygiel and Isabella Larcher (slides)
Unary profile of lambda terms with restricted De Bruijn indices

In our talk we present an average-case analysis of closed lambda terms with restricted values of De Bruijn indices in the model where each occurrence of a variable contributes one to the size. Given a fixed integer $k$, a lambda term in which values of all De Bruijn indices are bounded by $k$ has the following shape: It starts with $k$ De Bruijn levels, forming the so-called hat of the term, to which some number of $k$-colored Motzkin trees are attached. By means of analytic combinatorics, we show that the size of this hat is constant on average and that the average unary height of $k$-colored Motzkin trees of size $n$ is asymptotically $\Theta(\sqrt{n})$. Combining these two facts, we conclude that the maximal non-empty De Bruijn level in a lambda term with restrictions on De Bruijn indices and of size $n$ is, on average, also of order $\sqrt{n}$. On this basis, we provide the average unary profile of such lambda terms.

12:10-12:45 Lê Thành Dung Nguyen (slides)
Unique perfect matchings, structure from acyclicity and proof nets

Recall the following classical facts about a perfect matching $M$ in a graph $G$:

  • (Berge's lemma) $M$ is the unique perfect matching of $G$ iff it admits no alternating cycle.
  • (Kotzig's theorem) if $M$ is unique then $G$ contains a bridge belonging to $M$.

Taken together this means that the absence of cycle entails the positive existence of some configuration in the graph. As shown by Szeider [1], this is equivalent to several other "structure from acyclicity" properties in graph theory. In this talk I will present such an equivalent property coming from the proof theory of linear logic: the sequentialization theorem for MLL+Mix proof nets (a graphical representation of proofs). I will show how a result by Bellin [2] on proof nets can be rephrased as a very natural statement on unique perfect matchings. To be precise, it relates blossoms to decompositions by successive bridge deletions.

  • [1] On theorems equivalent with Kotzig’s result on graphs with unique 1-factors. Ars Combinatoria, 73:53–64, 2004.
  • [2] Gianluigi Bellin. Subnets of proof-nets in multiplicative linear logic with MIX. Mathematical Structures in Computer Science, 7(6):663–669, 1997.

  12:45-14:30 Lunch Break

14:30-15:05 Zbigniew Gołębiewski and Isabella Larcher (slides)
Asymptotic enumeration of the linear and affine closed lambda terms with natural size

A linear closed $\lambda$-term is a $\lambda$-term in which each variable occurs exactly once and there are no free variables. In an affine closed $\lambda$-term each variable occurs at most once. In this paper we determine the asymptotic formulas for the number of closed linear and affine $\lambda$-terms of natural size $n$ and with the restrictions on the size of variables. Most proofs are based on a singularity analysis of generating functions.

15:05-15:40 Olivier Bodini, Matthieu Dien, Antoine Genitrini and Frédéric Peschanski (slides)
The Combinatorics of Barrier Synchronization

We introduce probabilistic analysis techniques for the testing of programs based on concurrent models. During this talk we study the notion of process synchronization from the point of view of combinatorics. As a first step, we address the quantitative problem of counting the number of executions of simple processes interacting with synchronization barriers. We elaborate a systematic decomposition of processes that produces a symbolic integral formula to solve the problem. Based on this procedure, we develop a generic algorithm to generate process executions uniformly at random. For some interesting sub-classes of processes we propose very efficient counting and random sampling algorithms. All these algorithms have one important characteristic in common: they work on the control graph of processes and thus do not require the explicit construction of the state-space. By consequence, we thus completely avoid the classical combinatorial explosion induced by such processes.

  15:40-16:10 Coffee and tea break

16:10-17:00 Alain Giorgetti (slides)
About the bloom structure of closed linear lambda terms

This work is related to a bijection between closed linear lambda terms and rooted trivalent maps [O. Bodini, D. Gardy, and A. Jacquot, Asymptotics and random sampling for BCI and BCK lambda terms, TCS, 2013]. Ingredients for a formal proof of this bijection, with a proof assistant such as Coq, have been presented at CLA'15 [C. Dubois, A. Giorgetti, and N. Zeiberger, Lambda terms and maps, formally, CLA, 2015] and CLA'18 [C. Dubois and A. Giorgetti, Lambda terms and maps, formally (II), CLA, 2018]. We also introduced at CLA'18 the inductive structure of 'blooms', in bijection with closed linear lambda terms and rooted trivalent maps. We showed the interest of blooms for random and bounded-exhaustive generation of lambda terms and maps. This year I would like to present other properties of blooms, related to closed linear lambda terms and their correspondence with BCI terms.

  17:00 End of the meeting

Registration

Submission of a talk proposal for the meeting should be done no later than June 11, 2019, by sending a short abstract through Easychair. A talk submission should indicate at the beginning of the abstract whether this is for a short (30 minutes) or long (45 minutes) time slot. In the case of a large number of submissions, the steering committee reserves the right to offer a short slot instead of a long one; this information will be given together with the letter of acceptance of the talk.

The steering committee will decide on the meeting’s program by June 14, 2019. Attendance is free upon registration.

The registration for CLA 2019 is now open closed!

I plan to attend the workshop lunch on Monday.
I plan to attend the workshop dinner on Monday
(without an accompanying person).
I plan to attend the workshop lunch on Tuesday.
I plan to attend the workshop dinner on Monday
(with an accompanying person).
I hereby give consent for my personal data to be processed for the purposes of the registration for the Computational Logic and Applications workshop, in accordance with the Regulation (EU) 2016/679 of the European Parliament and of the Council of 27 April 2016 with regard to the processing of personal data and in accordance with the information clause attached to my consent.

Venue

The worshop will be held at the University of Versailles Saint-Quentin, UFR of Sciences.

Location

Presentations will take place in Salle Archimède. Coffee breaks and lunches will take place in Room 104, building Sophie Germain.

Both locations can be found on the campus plan.

Workshop dinner

The workshop dinner will take place on Monday at the Boeuf à la mode (4, rue au Pain, 78000 Versailles). All participants are cordially invited. The price for a single accompanying person is 47 EUR.

List of participants

  1. Maciej Bendkowski (Jagiellonian University)
  2. Olivier Bodini (Université Paris13)
  3. Julien Courtiel (Université de Caen)
  4. Catherine Dubois (ENSIIE -- Samovar)
  5. Sergey Dovgal (Université Paris 13)
  6. Michael Fuchs (National Chiao Tung University)
  7. Danièle Gardy (Université de Versailles Saint-Quentin)
  8. Marie-Claude Gaudel (LRI, Université de Paris-Sud et CNRS, Orsay)
  9. Antoine Genitrini (Sorbonne Université -- LIP6)
  10. Alain Giorgetti (FEMTO-ST Institute - Univ. Bourgogne Franche-Comté)
  11. Samuele Giraudo (LIGM, université Paris-Est Marne-la-Vallée)
  12. Bernhard Gittenberger (TU Wien)
  13. Zbigniew Gołębiewski (Wrocław University of Science and Technology)
  14. Clemens Grabmayer (GSSI L'Aquila)
  15. Katarzyna Grygiel (Technical University in Vienna)
  16. Farzad Jafarrahmani (École Normale Supérieure Paris-Saclay)
  17. George Kaye (University of Birmingham, United Kingdom)
  18. Isabella Larcher (TU Wien)
  19. Pierre Lescanne (ENS Lyon)
  20. Martin Lester (University of Reading)
  21. Nicolas Magaud (Universite de Strasbourg)
  22. Mehdi Naima (Université Paris13, LIPN)
  23. Le Thanh Dung Nguyen (LIPN, Université Paris 13)
  24. Martin Pépin (Sorbonne Université)
  25. Luigi Santocanale (LIS)
  26. Ryoma Shinya (Akita University)
  27. Alexandros Singh (LIPN, Université Paris 13 )
  28. Paul Tarau (University of North Texas)
  29. Frédéric Voisin (LRI, Université Paris-Sud, Orsay)
  30. Marek Zaionc (Theoretical Computer Science, Jagiellonian University)
  31. Noam Zeilberger (University of Birmingham)

Special issue

Following the meeting, a special issue of DMTCS is planned for early 2020 with full papers on the topics of CLA. These papers can be either results presented at the 2019 CLA meeting, or at a former meeting but not published elsewhere, or results not presented at CLA, as long as they fall within the scope of the workshop. The submitted papers should present original research, including survey papers, which is not already published or submitted to publication to another journal.

The editors for the special issue are:

The papers will be refereed according to the usual standards of DMTCS.

Papers should be written in English. The submission process for DMTCS is the standard one for this journal. Ensure that you submit to the special volume CLA 2019 and that you leave the section of the journal unspecified. Authors will be notified of a decision within four months of submission to the special issue.

Submission deadline for contributions to the DMTCS special issue is September 30, 2019.

History

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

Sponsors

The workshop is supported by: