-
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.
-
The Benefits of Diligence
Authors:
Victor Arrial,
Giulio Guerrieri,
Delia Kesner
Abstract:
This paper studies the strength of embedding Call-by-Name ({\tt dCBN}) and Call-by-Value ({\tt dCBV}) into a unifying framework called the Bang Calculus ({\tt dBANG}). These embeddings enable establishing (static and dynamic) properties of {\tt dCBN} and {\tt dCBV} through their respective counterparts in {\tt dBANG}. While some specific static properties have been already successfully studied in…
▽ More
This paper studies the strength of embedding Call-by-Name ({\tt dCBN}) and Call-by-Value ({\tt dCBV}) into a unifying framework called the Bang Calculus ({\tt dBANG}). These embeddings enable establishing (static and dynamic) properties of {\tt dCBN} and {\tt dCBV} through their respective counterparts in {\tt dBANG}. While some specific static properties have been already successfully studied in the literature, the dynamic ones are more challenging and have been left unexplored. We accomplish that by using a standard embedding for the (easy) {\tt dCBN} case, while a novel one must be introduced for the (difficult) {\tt dCBV} case. Moreover, a key point of our approach is the identification of {\tt dBANG} diligent reduction sequences, which eases the preservation of dynamic properties from {\tt dBANG} to {\tt dCBN}/{\tt dCBV}. We illustrate our methodology through two concrete applications: confluence/factorization for both {\tt dCBN} and {\tt dCBV} are respectively derived from confluence/factorization for {\tt dBANG}.
△ Less
Submitted 19 April, 2024;
originally announced April 2024.
-
Meaningfulness and Genericity in a Subsuming Framework
Authors:
Delia Kesner,
Victor Arrial,
Giulio Guerrieri
Abstract:
This paper studies the notion of meaningfulness for a unifying framework called dBang-calculus, which subsumes both call-by-name (dCbN) and call-by-value (dCbV). We first characterize meaningfulness in dBang by means of typability and inhabitation in an associated non-idempotent intersection type system previously proposed in the literature. We validate the proposed notion of meaningfulness by sho…
▽ More
This paper studies the notion of meaningfulness for a unifying framework called dBang-calculus, which subsumes both call-by-name (dCbN) and call-by-value (dCbV). We first characterize meaningfulness in dBang by means of typability and inhabitation in an associated non-idempotent intersection type system previously proposed in the literature. We validate the proposed notion of meaningfulness by showing two properties (1) consistency of the theory $\mathcal{H}$ equating meaningless terms and (2) genericity, stating that meaningless subterms have no bearing on the significance of meaningful terms. The theory $\mathcal{H}$ is also shown to have a unique consistent and maximal extension. Last but not least, we show that the notions of meaningfulness and genericity in the literature for dCbN and dCbV are subsumed by the respectively ones proposed here for the dBang-calculus.
△ Less
Submitted 9 April, 2024;
originally announced April 2024.
-
Genericity Through Stratification
Authors:
Victor Arrial,
Giulio Guerrieri,
Delia Kesner
Abstract:
A fundamental issue in the $λ$-calculus is to find appropriate notions for meaningfulness. It is well-known that in the call-by-name $λ$-calculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is not appropriate in the call-by-value $λ$-calculus (CbV). This paper validates the challenging claim that yet another notion, previously introduced in the literat…
▽ More
A fundamental issue in the $λ$-calculus is to find appropriate notions for meaningfulness. It is well-known that in the call-by-name $λ$-calculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is not appropriate in the call-by-value $λ$-calculus (CbV). This paper validates the challenging claim that yet another notion, previously introduced in the literature as potential valuability, appropriately represents meaningfulness in CbV. Akin to CbN, this claim is corroborated by proving two essential properties. The first one is genericity, stating that meaningless subterms have no bearing on evaluating normalizing terms. To prove this (which was an open problem), we use a novel approach based on stratified reduction, indifferently applicable to CbN and CbV, and in a quantitative way. The second property concerns consistency of the smallest congruence relation resulting from equating all meaningless terms. While the consistency result is not new, we provide the first direct operational proof of it. We also show that such a congruence has a unique consistent and maximal extension, which coincides with a well-known notion of observational equivalence. Our results thus supply the formal concepts and tools that validate the informal notion of meaningfulness underlying CbN and CbV.
△ Less
Submitted 31 January, 2024; v1 submitted 22 January, 2024;
originally announced January 2024.
-
Milner's Lambda-Calculus with Partial Substitutions
Authors:
Delia Kesner,
Shane Ó Conchúir
Abstract:
We study Milner's lambda-calculus with partial substitutions. Particularly, we show confluence on terms and metaterms, preservation of \b{eta}-strong normalisation and characterisation of strongly normalisable terms via an intersection ty** discipline. The results on terms transfer to Milner's bigraphical model of the calculus. We relate Milner's calculus to calculi with definitions, to calculi…
▽ More
We study Milner's lambda-calculus with partial substitutions. Particularly, we show confluence on terms and metaterms, preservation of \b{eta}-strong normalisation and characterisation of strongly normalisable terms via an intersection ty** discipline. The results on terms transfer to Milner's bigraphical model of the calculus. We relate Milner's calculus to calculi with definitions, to calculi with explicit substitutions, and to MELL Proof-Nets.
△ Less
Submitted 20 December, 2023;
originally announced December 2023.
-
Quantitative Global Memory
Authors:
Sandra Alves,
Delia Kesner,
Miguel Ramos
Abstract:
We show that recent approaches of static analysis based on quantitative ty** systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory, together with a semantic model based on a (tight) multi-type system that captures exact measures of time and space related to evaluation of programs.…
▽ More
We show that recent approaches of static analysis based on quantitative ty** systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory, together with a semantic model based on a (tight) multi-type system that captures exact measures of time and space related to evaluation of programs. We show that the type system is quantitatively sound and complete with respect to the original operational semantics of the language.
△ Less
Submitted 16 June, 2023; v1 submitted 15 March, 2023;
originally announced March 2023.
-
Node Replication: Theory And Practice
Authors:
Delia Kesner,
Loïc Peyrot,
Daniel Ventura
Abstract:
We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.
We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.
△ Less
Submitted 19 January, 2024; v1 submitted 14 July, 2022;
originally announced July 2022.
-
A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications
Authors:
José Espírito Santo,
Delia Kesner,
Loïc Peyrot
Abstract:
We introduce a call-by-name lambda-calculus $λJn$ with generalized applications which is equipped with distant reduction. This allows to unblock $β$-redexes without resorting to the standard permutative conversions of generalized applications used in the original $ΛJ$-calculus with generalized applications of Joachimski and Matthes. We show strong normalization of simply-typed terms, and we then f…
▽ More
We introduce a call-by-name lambda-calculus $λJn$ with generalized applications which is equipped with distant reduction. This allows to unblock $β$-redexes without resorting to the standard permutative conversions of generalized applications used in the original $ΛJ$-calculus with generalized applications of Joachimski and Matthes. We show strong normalization of simply-typed terms, and we then fully characterize strong normalization by means of a quantitative (i.e. non-idempotent intersection) ty** system. This characterization uses a non-trivial inductive definition of strong normalization --related to others in the literature--, which is based on a weak-head normalizing strategy. We also show that our calculus $λJn$ relates to explicit substitution calculi by means of a faithful translation, in the sense that it preserves strong normalization. Moreover, our calculus $λJn$ and the original $ΛJ$-calculus determine equivalent notions of strong normalization. As a consequence, $λJ$ inherits a faithful translation into explicit substitutions, and its strong normalization can also be characterized by the quantitative ty** system designed for $λJn$, despite the fact that quantitative subject reduction fails for permutative conversions.
△ Less
Submitted 9 January, 2024; v1 submitted 11 January, 2022;
originally announced January 2022.
-
Encoding Tight Ty** in a Unified Framework
Authors:
Delia Kesner,
Andrés Viso
Abstract:
This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, ie. they provide exact information about the length of normaliz…
▽ More
This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, ie. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV.
△ Less
Submitted 28 October, 2021; v1 submitted 2 May, 2021;
originally announced May 2021.
-
A Strong Bisimulation for a Classical Term Calculus
Authors:
Eduardo Bonelli,
Delia Kesner,
Andrés Viso
Abstract:
When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of $λ$-calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on $λ$-terms known as $\simeq_σ$-equivalence, in both the intuitionistic (due to Regnier) and classical (due to Laurent) cases. The purpose of this paper is to uncover a stro…
▽ More
When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of $λ$-calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on $λ$-terms known as $\simeq_σ$-equivalence, in both the intuitionistic (due to Regnier) and classical (due to Laurent) cases. The purpose of this paper is to uncover a strong bisimulation behind $\simeq_σ$-equivalence, as formulated by Laurent for Parigot's $λμ$-calculus. This is achieved by introducing a relation $\simeq$, defined over a revised presentation of $λμ$-calculus we dub $ΛM$.
More precisely, we first identify the reasons behind Laurent's $\simeq_σ$-equivalence on $λμ$-terms failing to be a strong bisimulation. Inspired by Laurent's \emph{Polarized Proof-Nets}, this leads us to distinguish multiplicative and exponential reduction steps on terms. Second, we enrich the syntax of $λμ$ to allow us to track the exponential operations. These technical ingredients pave the way towards a strong bisimulation for the classical case. We introduce a calculus $ΛM$ and a relation $\simeq$ that we show to be a strong bisimulation with respect to reduction in $ΛM$, ie. two $\simeq$-equivalent terms have the exact same reduction semantics, a result which fails for Regnier's $\simeq_σ$-equivalence in $λ$-calculus as well as for Laurent's $\simeq_σ$-equivalence in $λμ$. Although $\simeq$ is formulated over an enriched syntax and hence is not strictly included in Laurent's $\simeq_σ$, we show how it can be seen as a restriction of it.
△ Less
Submitted 17 April, 2024; v1 submitted 14 January, 2021;
originally announced January 2021.
-
The Bang Calculus Revisited
Authors:
Antonio Bucciarelli,
Delia Kesner,
Alejandro Ríos,
Andrés Viso
Abstract:
Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Callby-Name (CBN) and Call-by-Value (CBV) semantics. The essence of this paradigm is captured by the Bang Calculus, a (concise) term language connecting CBPV and Linear Logic.
This paper presents a revisited version of the Bang Calculus, called $λ!$, enjoying some important properties missing in the original formulation. Indeed,…
▽ More
Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Callby-Name (CBN) and Call-by-Value (CBV) semantics. The essence of this paradigm is captured by the Bang Calculus, a (concise) term language connecting CBPV and Linear Logic.
This paper presents a revisited version of the Bang Calculus, called $λ!$, enjoying some important properties missing in the original formulation. Indeed, the new calculus integrates permutative conversions to unblock value redexes while being confluent at the same time. A second contribution is related to nonidempotent types. We provide a quantitative type system for our $λ!$-calculus, and we show that the length of the (weak) reduction of a typed term to its normal form plus the size of this normal form is bounded by the size of its type derivation. We also explore the properties of this type system with respect to CBN/CBV translations. We keep the original CBN translation from $λ$-calculus to the Bang Calculus, which preserves normal forms and is sound and complete with respect to the (quantitative) type system for CBN. However, in the case of CBV, we reformulate both the translation and the type system to restore two main properties: preservation of normal forms and completeness. Last but not least, the quantitative system is refined to a tight one, which transforms the previous upper bound on the length of reduction to normal form plus its size into two independent exact measures for them.
△ Less
Submitted 5 May, 2023; v1 submitted 10 February, 2020;
originally announced February 2020.
-
A Quantitative Understanding of Pattern Matching
Authors:
Sandra Alves,
Delia Kesner,
Daniel Ventura
Abstract:
This paper shows that the recent approach to quantitative ty** systems for programming languages can be extended to pattern matching features. Indeed, we define two resource aware type systems, named U and E, for a lambda-calculus equipped with pairs for both patterns and terms. Our ty** systems borrow some basic ideas from [BKRDR15], which characterises (head) normalisation in a qualitative w…
▽ More
This paper shows that the recent approach to quantitative ty** systems for programming languages can be extended to pattern matching features. Indeed, we define two resource aware type systems, named U and E, for a lambda-calculus equipped with pairs for both patterns and terms. Our ty** systems borrow some basic ideas from [BKRDR15], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But in contrast to [BKRDR15], our (static) systems also provides quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of normalisation sequences plus the size of their corresponding normal forms, while system E, which can be seen as a refinement of system U, produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs, instead of the disjoint unions in [BKRDR15], thus avoiding an overlap between "being a pair" and "being duplicable", resulting in an essential tool to reason about quantitativity. Secondly, ty** sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (c.f. length) and space (c.f. size). Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors. Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta reduction, substitution and matching steps are counted separately.
△ Less
Submitted 4 December, 2019;
originally announced December 2019.
-
Strong Bisimulation for Control Operators
Authors:
Eduardo Bonelli,
Delia Kesner,
Andrés Viso
Abstract:
The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation $\simeq$, defined over a revised presentation of Parigot's $λμ$-calculus we dub $ΛM$. Our result builds on two fundamental ingredients: (1) factorization of $λμ$-reduction into multiplicative and exponential steps by means of exp…
▽ More
The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation $\simeq$, defined over a revised presentation of Parigot's $λμ$-calculus we dub $ΛM$. Our result builds on two fundamental ingredients: (1) factorization of $λμ$-reduction into multiplicative and exponential steps by means of explicit term operators of $ΛM$, and (2) translation of $ΛM$-terms into Laurent's polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation $\simeq$ is shown to characterize structural equivalence in PPN. Most notably, $\simeq$ is shown to be a strong bisimulation with respect to reduction in $ΛM$, i.e. two $\simeq$-equivalent terms have the exact same reduction semantics, a result which fails for Regnier's $σ$-equivalence in $λ$-calculus as well as for Laurent's $σ$-equivalence in $λμ$.
△ Less
Submitted 16 October, 2019; v1 submitted 21 June, 2019;
originally announced June 2019.
-
Solvability = Typability + Inhabitation
Authors:
Antonio Bucciarelli,
Delia Kesner,
Simona Ronchi Della Rocca
Abstract:
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 canon…
▽ More
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.
△ Less
Submitted 28 January, 2021; v1 submitted 14 December, 2018;
originally announced December 2018.
-
Tight Ty**s and Split Bounds
Authors:
Beniamino Accattoli,
Stéphane Graham-Lengrand,
Delia Kesner
Abstract:
Multi types---aka non-idempotent intersection types---have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of the result. Recent results show that the number of steps can be taken as a reasonable time complexity measure. At the same time, however, these results suggest th…
▽ More
Multi types---aka non-idempotent intersection types---have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of the result. Recent results show that the number of steps can be taken as a reasonable time complexity measure. At the same time, however, these results suggest that multi types provide quite lax complexity bounds, because the size of the result can be exponentially bigger than the number of steps.
Starting from this observation, we refine and generalise a technique introduced by Bernadet & Graham-Lengrand to provide exact bounds for the maximal strategy. Our ty** judgements carry two counters, one measuring evaluation lengths and the other measuring result sizes. In order to emphasise the modularity of the approach, we provide exact bounds for four evaluation strategies, both in the lambda-calculus (head, leftmost-outermost, and maximal evaluation) and in the linear substitution calculus (linear head evaluation).
Our work aims at both capturing the results in the literature and extending them with new outcomes. Concerning the literature, it unifies de Carvalho and Bernadet & Graham-Lengrand via a uniform technique and a complexity-based perspective. The two main novelties are exact split bounds for the leftmost strategy---the only known strategy that evaluates terms to full normal forms and provides a reasonable complexity measure---and the observation that the computing device hidden behind multi types is the notion of substitution at a distance, as implemented by the linear substitution calculus.
△ Less
Submitted 6 July, 2018;
originally announced July 2018.
-
Non-idempotent types for classical calculi in natural deduction style
Authors:
Delia Kesner,
Pierre Vial
Abstract:
In the first part of this paper, we define two resource aware ty** systems for the λμ-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head red…
▽ More
In the first part of this paper, we define two resource aware ty** systems for the λμ-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments-based on decreasing measures of type derivations-to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head reduction and the maximal reduction sequences to normal-form. In the second part of this paper, the λμ-calculus is refined to a small-step calculus called λμs, which is inspired by the substitution at a distance paradigm. The λμs-calculus turns out to be compatible with a natural extensionof the non-idempotent interpretations of λμ, i.e., λμs-reduction preserves and decreases ty** derivations in an extended appropriate ty** system. We thus derive a simple arithmetical characterization of strongly λμs-normalizing terms by means of ty**.
△ Less
Submitted 13 January, 2020; v1 submitted 15 February, 2018;
originally announced February 2018.
-
Call-by-Need, Neededness and All That
Authors:
Delia Kesner,
Alejandro Ríos,
Andrés Viso
Abstract:
We show that call-by-need is observationally equivalent to weak-head needed reduction. The proof of this result uses a semantical argument based on a (non-idempotent) intersection type system called $\mathcal{V}$. Interestingly, system $\mathcal{V}$ also allows to syntactically identify all the weak-head needed redexes of a term.
We show that call-by-need is observationally equivalent to weak-head needed reduction. The proof of this result uses a semantical argument based on a (non-idempotent) intersection type system called $\mathcal{V}$. Interestingly, system $\mathcal{V}$ also allows to syntactically identify all the weak-head needed redexes of a term.
△ Less
Submitted 8 September, 2020; v1 submitted 31 January, 2018;
originally announced January 2018.
-
Inhabitation for Non-idempotent Intersection Types
Authors:
Antonio Bucciarelli,
Delia Kesner,
Simona Ronchi Della Rocca
Abstract:
The inhabitation problem for intersection types in the lambda-calculus is known to be undecidable. We study the problem in the case of non-idempotent intersection, considering several type assignment systems, which characterize the solvable or the strongly normalizing lambda-terms. We prove the decidability of the inhabitation problem for all the systems considered, by providing sound and complete…
▽ More
The inhabitation problem for intersection types in the lambda-calculus is known to be undecidable. We study the problem in the case of non-idempotent intersection, considering several type assignment systems, which characterize the solvable or the strongly normalizing lambda-terms. We prove the decidability of the inhabitation problem for all the systems considered, by providing sound and complete inhabitation algorithms for them.
△ Less
Submitted 2 August, 2018; v1 submitted 11 December, 2017;
originally announced December 2017.
-
On abstract normalisation beyond neededness
Authors:
Eduardo Bonelli,
Delia Kesner,
Carlos Lombardi,
Alejandro Rios
Abstract:
We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focussing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first…
▽ More
We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focussing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first prove a normalisation theorem for abstract rewrite systems (ARS), a general rewriting framework encompassing many rewriting systems developed by P-A.Melliès in his PhD thesis. The theorem states that multistep strategies reducing so called necessary and never-grip** sets of redexes at a time are normalising in any ARS. Grip** refers to an abstract property reflecting the behavior of higher-order substitution. We then apply this result to the particular case of PPC, a calculus of patterns and to the lambda-calculus with parallel-or.
△ Less
Submitted 9 May, 2016; v1 submitted 5 December, 2014;
originally announced December 2014.
-
Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications
Authors:
Delia Kesner,
Petrucio Viana
Abstract:
This document contains the proceedings of the Seventh International Workshop on Logical and Semantic Frameworks, with Applications, which was held on September 29 and 30, 2012, in Rio de Janeiro, Brazil. It contains 11 regular papers (9 long and 2 short) accepted for presentation at the meeting, as well as extended abstracts of invited talks by Torben Braüner (Roskilde University, Denmark), Maribe…
▽ More
This document contains the proceedings of the Seventh International Workshop on Logical and Semantic Frameworks, with Applications, which was held on September 29 and 30, 2012, in Rio de Janeiro, Brazil. It contains 11 regular papers (9 long and 2 short) accepted for presentation at the meeting, as well as extended abstracts of invited talks by Torben Braüner (Roskilde University, Denmark), Maribel Fernández (King's College London, United Kingdom), Edward Hermann Haeusler (PUC-Rio, Brazil) and Alexandre Miquel (École Normale Supérieure de Lyon, France).
△ Less
Submitted 28 March, 2013;
originally announced March 2013.
-
Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
Authors:
Beniamino Accattoli,
Delia Kesner
Abstract:
Inspired by a recent graphical formalism for lambda-calculus based on linear logic technology, we introduce an untyped structural lambda-calculus, called lambda j, which combines actions at a distance with exponential rules decomposing the substitution by means of weakening, contraction and derelicition. First, we prove some fundamental properties of lambda j such as confluence and preservation o…
▽ More
Inspired by a recent graphical formalism for lambda-calculus based on linear logic technology, we introduce an untyped structural lambda-calculus, called lambda j, which combines actions at a distance with exponential rules decomposing the substitution by means of weakening, contraction and derelicition. First, we prove some fundamental properties of lambda j such as confluence and preservation of beta-strong normalisation. Second, we add a strong bisimulation to lambda j by means of an equational theory which captures in particular Regnier's sigma-equivalence. We then complete this bisimulation with two more equations for (de)composition of substitutions and we prove that the resulting calculus still preserves beta-strong normalization. Finally, we discuss some consequences of our results.
△ Less
Submitted 23 March, 2012; v1 submitted 3 March, 2012;
originally announced March 2012.
-
A standardisation proof for algebraic pattern calculi
Authors:
Delia Kesner,
Carlos Lombardi,
Alejandro Ríos
Abstract:
This work gives some insights and results on standardisation for call-by-name pattern calculi. More precisely, we define standard reductions for a pattern calculus with constructor-based data terms and patterns. This notion is based on reduction steps that are needed to match an argument with respect to a given pattern. We prove the Standardisation Theorem by using the technique developed by Taka…
▽ More
This work gives some insights and results on standardisation for call-by-name pattern calculi. More precisely, we define standard reductions for a pattern calculus with constructor-based data terms and patterns. This notion is based on reduction steps that are needed to match an argument with respect to a given pattern. We prove the Standardisation Theorem by using the technique developed by Takahashi and Crary for lambda-calculus. The proof is based on the fact that any development can be specified as a sequence of head steps followed by internal reductions, i.e. reductions in which no head steps are involved.
△ Less
Submitted 17 February, 2011;
originally announced February 2011.
-
A Theory of Explicit Substitutions with Safe and Full Composition
Authors:
Delia Kesner
Abstract:
Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda…
▽ More
Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda-calculus which enjoys a whole set of useful properties such as full composition, simulation of one-step beta-reduction, preservation of beta-strong normalisation, strong normalisation of typed terms and confluence on metaterms. Normalisation of related calculi is also discussed.
△ Less
Submitted 15 July, 2009; v1 submitted 15 May, 2009;
originally announced May 2009.
