Antonio Bucciarelli ; Delia Kesner ; Simona Ronchi Della Rocca - Solvability = Typability + Inhabitation

lmcs:5041 - Logical Methods in Computer Science, January 29, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:7)2021
Solvability = Typability + InhabitationArticle

Authors: Antonio Bucciarelli ; Delia Kesner ; Simona Ronchi Della Rocca

    We extend the classical notion of solvability to a lambda-calculus equipped with pattern matching. We prove that solvability can be characterized by means of typability and inhabitation in an intersection type system P based on non-idempotent types. We show first that the system P characterizes the set of terms having canonical form, i.e. that a term is typable if and only if it reduces to a canonical form. But the set of solvable terms is properly contained in the set of canonical forms. Thus, typability alone is not sufficient to characterize solvability, in contrast to the case for the lambda-calculus. We then prove that typability, together with inhabitation, provides a full characterization of solvability, in the sense that a term is solvable if and only if it is typable and the types of all its arguments are inhabited. We complete the picture by providing an algorithm for the inhabitation problem of P.


    Volume: Volume 17, Issue 1
    Published on: January 29, 2021
    Accepted on: November 12, 2020
    Submitted on: December 17, 2018
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1849 times.
    This article's PDF has been downloaded 333 times.