FICS 2015 Contributed Talks with Abstracts

Abstract: In the modal mu-calculus, a formula is well-formed
if each recursive variable occurs underneath an even number of
negations. By means of De Morgan's laws, it is easy to transform
any well-formed formula in a formula without negations, its negation
normal form.
Moreover, if the initial formula is of size n, its negation normal form is
of size at most n. The full modal mu-calculus and the negation
normal form fragment are thus equally expressive and concise.
In this paper we extend this result to the higher-order fixpoint
logic, an extension of the modal mu-calculus with
higher-order recursive predicate transformers. We present a procedure
that converts a formula of size n into an equivalent formula
without negations of linear size when the number of variables is fixed.
Due to the type system ruling HFL formulas, our procedure significantly
differs from the standard ``negation pushing'' procedure and crucially exploits
type annotations on all subformulas.

Abstract: An independent partition of the set of attributes of a finite relation is any partition of the attributes such that the Cartesian product of the projections of the relation over the elements of the partition yields the original relation. Identifying independent partitions has many applications and corresponds conceptually to revealing orthogonality between sets of dimensions in multidimensional point spaces. Concretely, our work is motivated by the problem of program model decomposition for the static analysis of software families.
This paper addresses the problem of finding maximum independent partitions for finite relations, ignoring the order of the attributes. We develop our theory in terms of the finite lattice of partitions of the set of attributes, ordered by refinement, and the lattice of quotient relations it induces. We present a characterisation of independent partitions in terms of the so-called minimal self-correlated sets of attributes (mincors). We consider a transformer on partitions corresponding to merging overlapping mincors combined with relation quotienting. We show that the transformer is not monotone but increasing and show that the maximum independent partition is its least fixed point. We use some additional properties of the transformer to show that this fixed point is still the limit of the standard approximation sequence as in Kleene's well-known fixed point theorem for continuous functions, giving rise to an iterative fixed point computation procedure. The said procedure is efficient, given an oracle for the mincors.

Abstract: Energy problems are important in the formal analysis of embedded or autonomous systems. Using recent results on *-continuous Kleene ω-algebras, we show here that energy problems can be solved by algebraic manipulations on the transition matrix of energy automata. To this end, we prove general results about certain classes of finitely additive functions on complete lattices which should be of a more general interest.

Abstract: This paper studies the relationship between disjunctive normal form, a syntactic normal form for modal mu, and the alternation hierarchy. First it shows that in some sense the question of alternation depth is much simplified in disjunctive form: all disjunctive formulas which have equivalent tableau have the same syntactic alternation depth. However, tableau equivalence only preserves alternation depth for the disjunctive fragment: there are disjunctive formulas with arbitrarily high alternation depth that are tableau equivalent to alternation-free non-disjunctive formulas. Conversely, there are non-disjunctive formulas of arbitrarily high alternation depth that are tableau equivalent to disjunctive formulas without alternations. This answers negatively the so far open question of whether disjunctive form preserves alternation depth. The classes of formulas studied here illustrate a previously undocumented type of unnecessary syntactic complexity which may contribute to our understanding of why deciding the alternation hierarchy is still an open problem.

Abstract: Two distinct research approaches have been proposed for
assigning a purely extensional semantics to higher-order
logic programming. The former approach uses classical
domain-theoretic tools while the latter builds on a
fixed-point construction defined on a syntactic instantiation
of the source program. The relationships between these two
approaches had not been investigated until now. In this paper
we demonstrate that for a very broad class of programs,
namely the class of definitional programs introduced
by W. W. Wadge, the two approaches coincide (with respect
to ground atoms that involve symbols of the program).
On the other hand, we argue that if existential higher-order
variables are allowed to appear in the bodies of program rules,
the two approaches are in general different. The results of
the paper contribute to a better understanding of the semantics
of higher-order logic programming.

Abstract: Usual termination proofs for a functional program require to check all the possible reduction paths. Due to an exponential gap between the height and size of such the reduction tree, any naive formalization of termination proofs yields no connection to the polynomial complexity of the given program. We solve this problem employing the notion of minimal function graph, a set of pairs of a term and its normal form, which is defined as the least fixed point of a monotone operator. We show that termination proofs for programs reducing under lexicographic path orders (LPO for short) and polynomilally quasi-interpretable can be optimally performed in a weak fragment of Peano arithmetic. This yields an alternative proof of the fact that every function computed by an LPO-terminating, polynomially quasi-interpretable program is computable in polynomial space. The formalization is indeed optimal since every poly-space computable function can be computed by such a program. The crucial observation is that inductive definitions of minimal function graphs for LPO-terminating programs can be approximated with transfinite induction along LPOs.

Abstract: In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types. It is well-known that dependent type theories à la Martin-Löf can be interpreted using fibrations. Modern theorem provers, however, are based on more sophisticated type systems that allow the definition of powerful inductive dependent types (known as inductive families) and, somewhat limited, coinductive dependent types. I define a class of functors on fibrations and show how data type definitions correspond to initial and final dialgebras for these functors. This description is also a proposal of how coinductive types should be treated in type theories, as they appear here simply as dual of inductive types. Finally, I show how dependent data types correspond to algebras and coalgebras, and give a prospect on the correspondence to (generalised) polynomial functors.

Abstract: This paper shows an application of Bloom and Esik's iteration algebras to
model graph data in a graph database query language. Around twenty years
ago, Buneman et al. developed a graph database query language UnQL on the top
of a functional meta-language UnCAL for describing and manipulating
graphs. Recently, the functional programming community has shown renewed
interest in UnCAL, because it provides an efficient graph transformation
language which is useful for various applications, such as bidirectional
computation. However, no mathematical semantics of UnQL/UnCAL graphs has
been developed. In this paper, we give an equational axiomatisation and
algebraic semantics of UnCAL graphs. The main result of this paper is to
prove that completeness of our equational axioms for UnCAL for the original
bisimulation of UnCAL graphs via iteration algebras. Another benefit of
algebraic semantics is a clean characterisation of structural recursion on
graphs using free iteration algebra.

Abstract: In functional programming, datatypes à la carte provide a
convenient modular representation of recursive datatypes, based on
their initial algebra semantics. Unfortunately it is highly
challenging to implement this technique in proof assistants that are
based on type theory, like Coq. The reason is that it involves type
definitions, such as those of type-level fixpoint operators, that are
not strictly positive. The known work-around of impredicative
encodings is problematic, insofar as it impedes conventional inductive
reasoning. Weak induction principles can be used instead, but they
considerably complicate proofs.
This paper proposes a novel and simpler technique to reason
inductively about impredicative encodings, based on Mendler-style
induction. This technique involves dispensing with dependent
induction, ensuring that datatypes can be lifted to predicates and
relying on relational formulations. A case study on proving subject
reduction for structural operational semantics illustrates that the
approach enables modular proofs, and that these proofs are essentially
similar to conventional ones.

Abstract: We present a coalgebraic generalisation of Fischer and Ladner's Propositional Dynamic Logic (PDL) and Parikh's Game Logic (GL). In earlier work, we proved a generic strong completeness result for coalgebraic dynamic logics without iteration. The coalgebraic semantics of such programs is given by a monad $T$, and modalities are interpreted via a predicate lifting $\lambda$ whose transpose is a monad morphism from $T$ to the neighbourhood monad. In this paper, we show that if the monad $T$ carries a complete semilattice structure, then we can define an iteration construct, and suitable notions of diamond-likeness and box-likeness of predicate-liftings which allows for the definition of an axiomatisation which is parametric in $T$, $\lambda$ and a chosen set of pointwise program operations. As our main result, we show that if the pointwise operations are ``negation-free'' and Kleisli composition left-distributes over the induced join on Kleisli arrows, then this axiomatisation yields weak completeness with respect to the class of standard models. As special instances, we recover the weak completeness of PDL and of dual-free Game Logic. As a modest new result we obtain completeness for dual-free GL extended with intersection (demonic choice) of games.

Abstract: The polyadic mu-calculus is a modal fixpoint logic whose formulas define relations
of nodes rather than just sets in labelled transition systems. It can express
exactly the polynomial-time computable and bisimulation-invariant queries on
finite graphs. In this paper we show that the hierarchy defined by fixing the arity
of formulas is strict, i.e. that higher arity yields greater expressive power. The
proof uses a diagonalisation argument.