-
The Essense of Useful Evaluation Through Quantitative Types (Extended Version)
Authors:
Pablo Barenbaum,
Delia Kesner,
Mariana Milicich
Abstract:
Several evaluation notions for lambda calculus qualify as reasonable cost models according to Slot and van Emde Boas' Invariance Thesis. A notable result achieved by Accattoli and Dal Lago is that leftmost-outermost reduction is reasonable, where the term representation uses sharing and the steps are useful. These results, initially studied in call-by-name, have also been extended to call-by-value…
▽ More
Several evaluation notions for lambda calculus qualify as reasonable cost models according to Slot and van Emde Boas' Invariance Thesis. A notable result achieved by Accattoli and Dal Lago is that leftmost-outermost reduction is reasonable, where the term representation uses sharing and the steps are useful. These results, initially studied in call-by-name, have also been extended to call-by-value. However, the existing formulations of usefulness lack inductive structure, making it challenging in particular to define and reason about type systems on top of the untyped syntax. Additionally, no type-based quantitative interpretations exist for useful evaluation. In this work, we establish the first inductive definition of useful evaluation for open weak call-by-value. This new useful strategy connects to a previous implementation of usefulness through a low-level abstract machine, incurring only in linear time overhead, thus providing a reasonable cost model for open call-by-value implementation. We also propose a semantic interpretation of useful call-by-value using a non-idempotent intersection type system equipped with a notion of tightness. The resulting interpretation is quantitative, i.e. provides exact step-count information for program evaluation. This turns out to be the first semantical interpretation in the literature for a notion of useful evaluation.
△ Less
Submitted 29 April, 2024;
originally announced April 2024.
-
Hybrid Intersection Types for PCF (Extended Version)
Authors:
Pablo Barenbaum,
Delia Kesner,
Mariana Milicich
Abstract:
Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit…
▽ More
Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together without making use of an encoding into a common target framework. This work proposes an intersection type system for PCF with a specific notion of evaluation, called PCFH. Evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV-like operational behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of ty** derivations provides upper bounds for the length of the reduction sequences to normal form. This type system is then refined to a tight one, offering exact information regarding the length of normalization sequences. This is the first time that a sound and complete quantitative type system has been designed for a hybrid computational model.
△ Less
Submitted 22 April, 2024;
originally announced April 2024.
-
Semantics of a Relational λ-Calculus (Extended Version)
Authors:
Pablo Barenbaum,
Federico Lochbaum,
Mariana Milicich
Abstract:
We extend the λ-calculus with constructs suitable for relational and functional-logic programming: non-deterministic choice, fresh variable introduction, and unification of expressions. In order to be able to unify λ-expressions and still obtain a confluent theory, we depart from related approaches, such as λProlog, in that we do not attempt to solve higher-order unification. Instead, abstractions…
▽ More
We extend the λ-calculus with constructs suitable for relational and functional-logic programming: non-deterministic choice, fresh variable introduction, and unification of expressions. In order to be able to unify λ-expressions and still obtain a confluent theory, we depart from related approaches, such as λProlog, in that we do not attempt to solve higher-order unification. Instead, abstractions are decorated with a location, which intuitively may be understood as its memory address, and we impose a simple coherence invariant: abstractions in the same location must be equal. This allows us to formulate a confluent small-step operational semantics which only performs first-order unification and does not require strong evaluation (below lambdas). We study a simply typed version of the system. Moreover, a denotational semantics for the calculus is proposed and reduction is shown to be sound with respect to the denotational semantics.
△ Less
Submitted 28 February, 2021; v1 submitted 23 September, 2020;
originally announced September 2020.
