Fredrik Dahlqvist ; Renato Neves - A Complete V-Equational System for Graded lambda-Calculus

entics:12299 - Electronic Notes in Theoretical Informatics and Computer Science, November 23, 2023, Volume 3 - Proceedings of MFPS XXXIX -
A Complete V-Equational System for Graded lambda-CalculusArticle

Authors: Fredrik Dahlqvist ; Renato Neves

    Modern programming frequently requires generalised notions of program equivalence based on a metric or a similar structure. Previous work addressed this challenge by introducing the notion of a V-equation, i.e. an equation labelled by an element of a quantale V, which covers inter alia (ultra-)metric, classical, and fuzzy (in)equations. It also introduced a V-equational system for the linear variant of lambda-calculus where any given resource must be used exactly once. In this paper we drop the (often too strict) linearity constraint by adding graded modal types which allow multiple uses of a resource in a controlled manner. We show that such a control, whilst providing more expressivity to the programmer, also interacts more richly with V-equations than the linear or Cartesian cases. Our main result is the introduction of a sound and complete V-equational system for a lambda-calculus with graded modal types interpreted by what we call a Lipschitz exponential comonad. We also show how to build such comonads canonically via a universal construction, and use our results to derive graded metric equational systems (and corresponding models) for programs with timed and probabilistic behaviour.

    Volume: Volume 3 - Proceedings of MFPS XXXIX
    Published on: November 23, 2023
    Accepted on: October 16, 2023
    Submitted on: September 19, 2023
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Category Theory,68Q01,F.3.0

    Consultation statistics

    This page has been seen 85 times.
    This article's PDF has been downloaded 73 times.