The date for the annunal meeting WG 1.6 is Sunday, July 18, 2018. The WG 1.6 is part of FLOC and will take place one day before the federate conference.
Abstract: This talk is about time cost models for the λ-calculus. To allow the definition of basic complexity classes such as P or EXP directly in the lambda-calculus, a cost models has to be reasonable, that is, polynomially related to the one of Turing machines. For the lambda-calculus the existence of an evaluation strategy whose number of steps is a reasonable cost model has been a long-standing open problem. Positive answers to special cases were known since 1995, but a solution for the general case has been provided only in 2014. The problem is peculiar because some of its aspects are somewhat counterintuitive. This talk is devoted to explain the subtleties of this fundamental topic. The key point that is often misunderstood, and that is here discussed at length, is that being efficient and being reasonable are two unrelated properties of evaluation strategies.
Abstract: In their seminal RTA'05 paper, Bournez and Garnier introduce probabilistic term rewrite system together with a technique, based on Lyapunov ranking functions, for establishing almost-sure termination of such systems. In this talk, I will present recent work with Ugo Dal Lago and Akihisa Yamda where we have revisited Bournez and Garnier's work. First, we have captured reductions of probabilistic rewrite systems in a novel way by means of multidistribution reduction sequences, thus accounting for both the nondeterminism in the choice of the redex and the probabilism intrinsic in firing each rule. Second, we have extended the interpretation method to the probabilistic setting, taking inspiration from Bournez and Garnier's termination technique. This method constitutes a significant generalisation, in particular, it is not restricted to the Reals and can be instantiated, e.g., by matrix interpretations.
Abstract: We present the ∆-calculus, an explicitly typed λ-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories, as described in the Barendregt-Dekker-Statman book on λ-calculi with types, producing a family of ∆-calculi with related intersection typed systems. We show why annotating pure λ-calculus with intersection types is not easy: a classical example is the difficulty to decorate the bound variable of the explicitly typed polymorphic identity λx:?.x such that the type of the identity is (σ → σ) ∩ (τ → τ ): previous attempts showed that the full power of the intersection type discipline can be easily lost. We show why intersection typed systems need a kind of synchronised reduction to fix the subject reduction theorem. The same issues also appear when decorating λ-calculus with union-types. We also show a rewriting-based subtyping algorithm. Finally, we show how the ∆-calculus can be raised to a ∆-framework by adding dependent-types as in the Edinburgh Logical Framework.
The meetings of the working group are public, with the single exception of the business meeting.