-
Sharing and Linear Logic with Restricted Access (Extended Version)
Authors:
Pablo Barenbaum,
Eduardo Bonelli
Abstract:
The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping A -> B respectively to !A -o B and !(A -o B), have been shown to correspond respectively to call-by-name and call-by-value. In this work, we split the of-course modality of linear logic in…
▽ More
The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping A -> B respectively to !A -o B and !(A -o B), have been shown to correspond respectively to call-by-name and call-by-value. In this work, we split the of-course modality of linear logic into two modalities, written "!" and "$\bullet$". Intuitively, the modality "!" specifies a subproof that can be duplicated and erased, but may not necessarily be "accessed", i.e. interacted with, while the combined modality "$!\bullet$" specifies a subproof that can moreover be accessed. The resulting system, called MSCLL, enjoys cut-elimination and is conservative over MELL. We study how restricting access to subproofs provides ways to control sharing in evaluation strategies. For this, we introduce a term-assignment for an intuitionistic fragment of MSCLL, called the $λ!\bullet$-calculus, which we show to enjoy subject reduction, confluence, and strong normalization of the simply typed fragment. We propose three sound and complete translations that respectively simulate call-by-name, call-by-value, and a variant of call-by-name that shares the evaluation of its arguments (similarly as in call-by-need). The translations are extended to simulate the Bang-calculus, as well as weak reduction strategies.
△ Less
Submitted 27 January, 2025;
originally announced January 2025.
-
Reductions in Higher-Order Rewriting and Their Equivalence
Authors:
Pablo Barenbaum,
Eduardo Bonelli
Abstract:
Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with…
▽ More
Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink's, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (\b{eta}-equivalence). This led Bruggink to reject "nested" composition, other than at the outermost level. In this paper, we propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide. We also propose a standardization procedure, that computes a canonical representative of the permutation equivalence class of a rewrite.
△ Less
Submitted 15 August, 2023; v1 submitted 27 October, 2022;
originally announced October 2022.
-
Proceedings 16th Logical and Semantic Frameworks with Applications
Authors:
Mauricio Ayala-Rincon,
Eduardo Bonelli
Abstract:
This volume contains the post-proceedings of the Sixteenth Logical and Semantic Frameworks with Applications (LSFA 2021). The meeting was held online on July 23-24, 2021, organised by the Universidad de Buenos Aires, Argentina. LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics i…
▽ More
This volume contains the post-proceedings of the Sixteenth Logical and Semantic Frameworks with Applications (LSFA 2021). The meeting was held online on July 23-24, 2021, organised by the Universidad de Buenos Aires, Argentina. LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include proof theory, type theory and rewriting theory, specification and deduction languages, and formal semantics of languages and systems.
△ Less
Submitted 7 April, 2022;
originally announced April 2022.
-
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.
-
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.
-
Efficient Type Checking for Path Polymorphism
Authors:
Juan Edi,
Andrés Viso,
Eduardo Bonelli
Abstract:
A type system combining type application, constants as types, union types (associative, commutative and idempotent) and recursive types has recently been proposed for statically typing path polymorphism, the ability to define functions that can operate uniformly over recursively specified applicative data structures. A typical pattern such functions resort to is $x\,y$ which decomposes a compound,…
▽ More
A type system combining type application, constants as types, union types (associative, commutative and idempotent) and recursive types has recently been proposed for statically typing path polymorphism, the ability to define functions that can operate uniformly over recursively specified applicative data structures. A typical pattern such functions resort to is $x\,y$ which decomposes a compound, in other words any applicative tree structure, into its parts. We study type-checking for this type system in two stages. First we propose algorithms for checking type equivalence and subtyping based on coinductive characterizations of those relations. We then formulate a syntax-directed presentation and prove its equivalence with the original one. This yields a type-checking algorithm which unfortunately has exponential time complexity in the worst case. A second algorithm is then proposed, based on automata techniques, which yields a polynomial-time type-checking algorithm.
△ Less
Submitted 28 April, 2017;
originally announced April 2017.
-
Type Soundness for Path Polymorphism
Authors:
Andrés Viso,
Eduardo Bonelli,
Mauricio Ayala-Rincón
Abstract:
Path polymorphism is the ability to define functions that can operate uniformly over arbitrary recursively specified data structures. Its essence is captured by patterns of the form $x\,y$ which decompose a compound data structure into its parts. Typing these kinds of patterns is challenging since the type of a compound should determine the type of its components. We propose a static type system (…
▽ More
Path polymorphism is the ability to define functions that can operate uniformly over arbitrary recursively specified data structures. Its essence is captured by patterns of the form $x\,y$ which decompose a compound data structure into its parts. Typing these kinds of patterns is challenging since the type of a compound should determine the type of its components. We propose a static type system (i.e. no run-time analysis) for a pattern calculus that captures this feature. Our solution combines type application, constants as types, union types and recursive types. We address the fundamental properties of Subject Reduction and Progress that guarantee a well-behaved dynamics. Both these results rely crucially on a notion of pattern compatibility and also on a coinductive characterisation of subtyping.
△ Less
Submitted 28 April, 2016; v1 submitted 13 January, 2016;
originally announced January 2016.
-
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-gripping sets of redexes at a time are normalising in any ARS. Gripping 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 9th International Workshop on Developments in Computational Models
Authors:
Mauricio Ayala-Rincón,
Eduardo Bonelli,
Ian Mackie
Abstract:
This volume contains a selection of the papers presented at the Ninth International Workshop on Developments in Computational Models (DCM 2013) held in Buenos Aires, Argentina on 26th August 2013, as a satellite event of CONCUR 2013. Several new models of computation have emerged in the last years, and many developments of traditional computational models have been proposed with the aim of taking…
▽ More
This volume contains a selection of the papers presented at the Ninth International Workshop on Developments in Computational Models (DCM 2013) held in Buenos Aires, Argentina on 26th August 2013, as a satellite event of CONCUR 2013. Several new models of computation have emerged in the last years, and many developments of traditional computational models have been proposed with the aim of taking into account the new demands of computer systems users and the new capabilities of computation engines. A new computational model, or a new feature in a traditional one, usually is reflected in a new family of programming languages, and new paradigms of software development. The aim of this workshop is to bring together researchers who are currently developing new computational models or new features for traditional computational models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area.
△ Less
Submitted 29 March, 2014;
originally announced March 2014.
-
Proceedings 5th International Workshop on Higher-Order Rewriting
Authors:
Eduardo Bonelli
Abstract:
HOR 2010 is a forum to present work concerning all aspects of higher-order rewriting. The aim is to provide an informal and friendly setting to discuss recent work and work in progress. Previous editions of HOR were held in Copenhagen - Denmark (HOR 2002), Aachen - Germany (HOR 2004), Seattle - USA (HOR 2006) and Paris - France (HOR 2007).
HOR 2010 is a forum to present work concerning all aspects of higher-order rewriting. The aim is to provide an informal and friendly setting to discuss recent work and work in progress. Previous editions of HOR were held in Copenhagen - Denmark (HOR 2002), Aachen - Germany (HOR 2004), Seattle - USA (HOR 2006) and Paris - France (HOR 2007).
△ Less
Submitted 16 February, 2011;
originally announced February 2011.
-
Superdevelopments for Weak Reduction
Authors:
Eduardo Bonelli,
Pablo Barenbaum
Abstract:
We study superdevelopments in the weak lambda calculus of Cagman and Hindley, a confluent variant of the standard weak lambda calculus in which reduction below lambdas is forbidden. In contrast to developments, a superdevelopment from a term M allows not only residuals of redexes in M to be reduced but also some newly created ones. In the lambda calculus there are three ways new redexes may be c…
▽ More
We study superdevelopments in the weak lambda calculus of Cagman and Hindley, a confluent variant of the standard weak lambda calculus in which reduction below lambdas is forbidden. In contrast to developments, a superdevelopment from a term M allows not only residuals of redexes in M to be reduced but also some newly created ones. In the lambda calculus there are three ways new redexes may be created; in the weak lambda calculus a new form of redex creation is possible. We present labeled and simultaneous reduction formulations of superdevelopments for the weak lambda calculus and prove them equivalent.
△ Less
Submitted 25 January, 2010;
originally announced January 2010.
