Solvability = Typability + Inhabitation
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-01-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5041/pdf |
| _version_ | 1797268588702203904 |
|---|---|
| author | Antonio Bucciarelli Delia Kesner Simona Ronchi Della Rocca |
| author_facet | Antonio Bucciarelli Delia Kesner Simona Ronchi Della Rocca |
| author_sort | Antonio Bucciarelli |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:52Z |
| format | Article |
| id | doaj.art-ca208024fc91482192d05c305ca3245f |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:52Z |
| publishDate | 2021-01-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-ca208024fc91482192d05c305ca3245f2024-03-08T10:33:15ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-01-01Volume 17, Issue 110.23638/LMCS-17(1:7)20215041Solvability = Typability + InhabitationAntonio BucciarelliDelia KesnerSimona Ronchi Della RoccaWe 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.https://lmcs.episciences.org/5041/pdfcomputer science - logic in computer sciencecomputer science - programming languages |
| spellingShingle | Antonio Bucciarelli Delia Kesner Simona Ronchi Della Rocca Solvability = Typability + Inhabitation Logical Methods in Computer Science computer science - logic in computer science computer science - programming languages |
| title | Solvability = Typability + Inhabitation |
| title_full | Solvability = Typability + Inhabitation |
| title_fullStr | Solvability = Typability + Inhabitation |
| title_full_unstemmed | Solvability = Typability + Inhabitation |
| title_short | Solvability = Typability + Inhabitation |
| title_sort | solvability typability inhabitation |
| topic | computer science - logic in computer science computer science - programming languages |
| url | https://lmcs.episciences.org/5041/pdf |
| work_keys_str_mv | AT antoniobucciarelli solvabilitytypabilityinhabitation AT deliakesner solvabilitytypabilityinhabitation AT simonaronchidellarocca solvabilitytypabilityinhabitation |