Workshop on Developments in Implicit Computational complExity & Foundational & Practical Aspects of Resource AnalysisDICE-FOPARA 2019

Linear Logic and Defeasible Logic have been adopted to formalise different features of knowledge representation: consumption of resources, and non monotonic reasoning in particular to represent exceptions. Recently, a framework to combine sub-structural features, corresponding to the consumption of resources, with defeasibility aspects to handle potentially conflicting information, has been discussed in literature, by some of the authors. Two applications emerged that are very relevant: energy management and business process management. We illustrate a set of guide lines to determine how to apply linear defeasible logic to those contexts.

Matteo Cristani

Guido Governatori

Francesco Olivieri

Claudio Tomazzoli

Many applications of denotational semantics, such as higher-order model checking or the complexity of normalization, rely on finite semantics for monomorphic type systems. We present two constructions of finite semantics for second-order Multiplicative-Additive Linear Logic (MALL2) and study their properties. We apply this to understand the gap in expressive power between MALL2 and its extension with type fixpoints, and to obtain an implicit characterization of regular languages in Elementary Linear Logic. Furthermore, some semantic results established here lay the groundwork for a sequel paper proposing a new approach to sub-polynomial implicit complexity.

Lê Thành Dũng Nguyễn

Thomas Seiller

CNRS

France

Paolo Pistone

University of Tübingen

Italy

Lorenzo Tortora de Falco

We introduce a new approach to implicit complexity in linear logic, inspired by functional database query languages and using recent developments in effective denotational semantics of polymorphism. We give the first sub-polynomial upper bound in a type system with impredicative polymorphism; adding restrictions on quantifiers yields a characterization of logarithmic space, for which extensional completeness is established via descriptive complexity.

Lê Thành Dũng Nguyễn

Pierre Pradic

We show that Lafont’s system of Soft Linear Logic together with a hierarchical version of digging captures the complexity class EXPTIME.

Brian Redmond

We are concerned with the average case runtime complexity analysis of a prototypical imperative language pWhile in the spirit of Dijkstra’s Guarded Command Language. This language is endowed with primitives for sampling and probabilistic choice so that randomized algorithms can be expressed. Complexity analysis in this setting is particularly appealing as efficiency is one striking reason why randomized algorithms have been introduced and studied: in many cases, the most efficient algorithm for the problem at hand is randomized.

Martin Avanzini

INRIA Sophia Antipolis, France

France

Michael Schaper

University of Innsbruck

Georg Moser

University of Innsbruck

Finding lower bounds in complexity theory has proven to be an extremely difficult task. In this article, we analyze two proofs of complexity lower bound: Ben-Or’s proof of minimal height of algebraic computational trees deciding certain problems and Mulmuley’s proof that restricted Parallel Random Access Machines (prams) over integers can not decide P-complete problems efficiently. We present the aforementioned models of computation in a framework inspired by dynamical systems and models of linear logic : graphings.

This interpretation allows to connect the classical proofs to topological entropy, an invariant of these systems; to devise an algebraic formulation of parallelism of computational models; and finally to strengthen Mulmuley’s result by separating the geometrical insights of the proof from the ones related to the computation and blending these with Ben-Or’s proof. Looking forward, the interpretation of algebraic complexity theory as dynamical system might shed a new light on research programs such as Geometric Complexity Theory.

Luc Pellissier

Thomas Seiller

CNRS

France

We translate the usual class of partial/primitive recursive functions to a pointer recursion framework, accessing actual input values via a pointer reading unit-cost function. These pointer recursive functions classes are equivalent to the usual partial/primitive recursive functions. Complexity-wise, this framework captures in a streamlined way most of the relevant subpolynomial classes. Pointer recursion with the safe/normal tiering discipline of Bellantoni and Cook corresponds to polylogtime computation. We introduce a new, non-size increasing tiering discipline, called tropical tiering. Tropical tiering and pointer recursion, used with some of the most common recursion schemes, capture the classes logspace, logspace/polylogtime, ptime, and NC. Finally, in a fashion reminiscent of the safe recursive functions, tropical tiering is expressed directly in the syntax of the function algebras, yielding the tropical recursive function algebras.

Paulin Jacobé De Naurois

We define a tier based type system to capture the class of Basic Feasible Functionals on an imperative programming language with oracles. Following the seminal work by Kapron and Steinberg on Oracle Turing Machine, we try to ensure a polynomial step count and a bounded lookahead revision on typable and terminating programs. We obtain a soundness result. An open issue is to know whether the polynomial step count can be computed by typable and terminating programs. Consequently, we have only a weak form of completeness.

Emmanuel Hainry

Bruce Kapron

University of Victoria

Canada

Jean-Yves Marion

LORIA

France

Romain Péchoux

INRIA / LORIA

France

We report on progress on a functorial approach to decision problems, making some remarks on how one may define these to be shaves on suitable sites, and the consequences that this has. Some minor results are given (without proofs) but otherwise this is just a synthetic report about work in progress.

Damiano Mazza

CNRS

France

I am chargé de recherche (resarcher) at CNRS, working at the Laboratoire d’Informatique de Paris Nord, Université Paris 13. I’ve held this position since 2008. Previously, I was post-doc at Preuves, Programmes et Systèmes and at LIPN. I did my Ph.D. thesis (which I defended in 2006) at the Institut de Mathématiques de Luminy, in Marseille. Before that, I studied CS Engineering in Rome, Italy (which is where I am from).

We propose an amortized analysis that approximates the resource usage of a Haskell expression. Using the plugin API of GHC, we convert the Haskell code into a simplified representation called GHC Core. We then apply a type-based system which derives linear upper bounds on the resource usage. This setup allows us to analyze real Haskell code, whereas previous implementations of similar analyses do not support any commonly used lazy functional programming languages.

Franz Siglmüller

Motivated by recent results of Kapron and Steinberg (LICS 2018) we introduce new forms of iteration on length in the setting of applied lambda-calculi for higher-type poly-time computability. In particular, in a type-two setting, we consider functionals which capture iteration on input length which bound interaction with the type-one input parameter, by restricting to a constant either the number of times the function parameter may return a value of increasing size, or the number of times the function paramater may be applied to an argument of increasing size. We prove that for any constant bound, the iterators obtained are equivalent, with respect to lambda definability over type one poly-time functions, to the recursor of Cook and Urquhart which captures Cobham’s notion of limited recursion on notation in this setting.

Bruce Kapron

University of Victoria

Canada

Florian Steinberg

INRIA Saclay

Germany

I will discuss Jones’ results which evaluate the expressiveness of higher-order data in the context of term rewriting. In this talk, I will present the original result, and then present the peculiarities that happen when non-deterministic evaluation is admitted.

Cynthia Kop

Radboud University Nijmegen

Netherlands