2026-07-24T05:46:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16299 2024-03-06T10:57:10Z ddc:004 open_access

Solvability for Generalized Applications Kesner, Delia Peyrot, Loïc Lambda-calculus Generalized applications Solvability CBN/CBV Quantitative types Solvability is a key notion in the theory of call-by-name lambda-calculus, used in particular to identify meaningful terms. However, adapting this notion to other call-by-name calculi, or extending it to different models of computation - such as call-by-value - , is not straightforward. In this paper, we study solvability for call-by-name and call-by-value lambda-calculi with generalized applications, both variants inspired from von Plato’s natural deduction with generalized elimination rules. We develop an operational as well as a logical theory of solvability for each of them. The operational characterization relies on a notion of solvable reduction for generalized applications, and the logical characterization is given in terms of typability in an appropriate non-idempotent intersection type system. Finally, we show that solvability in generalized applications and solvability in the lambda-calculus are equivalent notions. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Delia Kesner and Loïc Peyrot 2022 Is Part Of LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2022.18 urn:nbn:de:0030-drops-162994 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.18 eng https://creativecommons.org/licenses/by/4.0/legalcode