Programme

• Jean-Baptiste Jeannin, 13:30 – 14:15

• Alexandra Silva, 14:15 – 15:00

• Henning Basold, 15:15 – 16:00

CoCaml: Programming with Coinductive Types

Jean-Baptiste Jeannin ¹

Recursive functions defined on a coalgebraic datatype C may not converge if there are cycles in the input, that is, if the input object is not well-founded. Even so, there is often a useful solution. Unfortunately, current functional programming languages provide no support for specifying alternative solution methods. There are numerous examples in which it would be useful to do so: free variables, alpha-conversion, and substitution in infinitary lambda-terms; halting probabilities and expected running times of probabilistic protocols; abstract interpretation; and constructions involving finite automata. In each case the function would diverge under the standard semantics of recursion.

In this talk, we propose programming language constructs that allow the specification of alternative solutions and methods to compute them. We then introduce CoCaml, a functional programming language extending OCaml that implements those constructs and allows us to define functions on coinductive datatypes parameterized by an equation solver.

Initial Algebras of Terms, with binding and algebraic structure

Alexandra Silva ^{2 3}

In this talk, we illustrate the power of initiality by exploiting it in categories of algebra-valued presheaves $\mathrm{EM}(T)^N$, for a monad T on Sets. The use of presheaves to obtain certain calculi of expressions (with variable binding) was introduced by Fiore, Plotkin, and Turi. They used set-valued presheaves, whereas here the presheaves take values in a category $\mathrm{EM}(T)$ of Eilenberg-Moore algebras. This generalisation allows us to develop a theory where more structured calculi can be obtained. The use of algebras means also that we work in a linear context and need a separate operation $!$ for replication, for instance to describe strength for an endofunctor on $\mathrm{EM}(T)$. We apply the resulting theory to give systematic descriptions of non-trivial calculi: we introduce non- deterministic and weighted lambda terms and expressions for automata as initial algebras, and we formalise relevant equations diagrammatically.

Polynomial-based calculi for linear circuits

Henning Basold ²

In this talk we look at calculi which describe a variety of different types of linear circuits¹. Among these types are circuits which are closed or open (i.e., have no inputs or have them resp.) and those which have feedback loops (i.e., can use previous computations). Examples can be found in [M] or [R].

We will derive completeness results for each of these system types. As the title suggests, all calculi will be based on polynomials (in one or several variables or with even more structure). We refer to these as flat calculi. Such a flat calculus corresponds to a circuit without feedback. For example the closed circuits without feedback are represented by simple polynomials like $1 + aX + bX^3$.

To be able to describe feedback loops we build formal fractions over these flat calculi. We get a general completeness result for all the calculi arising from the construction of fractions by exposing a common structure among the flat calculi.

All methods used so far are of algebraic nature. But since linear circuits correspond to some kinds of streams and stream transformations (rational in a certain sense) we will discuss the suspected coalgebraic structure. Milius presents in [M] for example a complete calculus for closed circuits with feedback. The proof there is based on the coalgebraic structure. We will discuss the problems which arise from trying to capture the presented results in a coalgebraic way.

¹ Linear circuits are only build from scalar multiplication and addition, hence the name. They also may contain registers which can store values.

• [M] Stefan Milius. A sound and complete calculus for finite stream circuits. LICS, 2010.
• [R] Jan Rutten. Rational streams coalgebraically. LMCS, 2008.