Showing 1–10 of 10 results for author: Bucciarelli, A

Exploring New Topologies for the Theory of Clones

Authors: Antonio Bucciarelli, Antonino Salibra

Abstract: Clones of operations of arity omega (referred to as omega-operations) have been employed by Neumann to represent varieties of infinitary algebras defined by operations of at most arity omega. More recently, clone algebras have been introduced to study clones of functions, including omega-operations, within the framework of one-sorted universal algebra. Additionally, polymorphisms of arity omega, w… ▽ More Clones of operations of arity omega (referred to as omega-operations) have been employed by Neumann to represent varieties of infinitary algebras defined by operations of at most arity omega. More recently, clone algebras have been introduced to study clones of functions, including omega-operations, within the framework of one-sorted universal algebra. Additionally, polymorphisms of arity omega, which are omega-operations preserving the relations of a given first-order structure, have recently been used to establish model theory results with applications in the field of complexity of CSP problems. In this paper, we undertake a topological and algebraic study of polymorphisms of arity omega and their corresponding invariant relations. Given a set A and a Boolean ideal X on the set of omega-sequences of elements of A, we propose a method to endow the set of omega-operations on A with a topology, which we refer to as X-topology. Notably, the topology of pointwise convergence can be retrieved as a special case of this approach. Polymorphisms and invariant relations are then defined parametrically, with respect to the X-topology. We characterise the X-closed clones of omega-operations in terms of polymorphisms and invariant relations of arity omega, and present a method to relate those infinitary invariant relation and polymorphisms to the classical (finitary) Inv-Pol. △ Less

Submitted 11 September, 2024; v1 submitted 9 March, 2023; originally announced March 2023.

The higher dimensional propositional calculus

Authors: Antonio Bucciarelli, Pierre-Louis Curien, Antonio Ledda, Francesco Paoli, Antonino Salibra

Abstract: In recent research, some of the present authors introduced the concept of an n-dimensional Boolean algebra and its corresponding propositional logic nCL, generalising the Boolean propositional calculus to n>= 2 perfectly symmetric truth values. This paper presents a sound and complete sequent calculus for nCL, named nLK. We provide two proofs of completeness: one syntactic and one semantic. The fo… ▽ More In recent research, some of the present authors introduced the concept of an n-dimensional Boolean algebra and its corresponding propositional logic nCL, generalising the Boolean propositional calculus to n>= 2 perfectly symmetric truth values. This paper presents a sound and complete sequent calculus for nCL, named nLK. We provide two proofs of completeness: one syntactic and one semantic. The former implies as a corollary that nLK enjoys the cut admissibility property. The latter relies on the generalisation to the n-ary case of the classical proof based on the Lindenbaum algebra of formulas and Boolean ultrafilters. △ Less

Submitted 7 May, 2024; v1 submitted 1 April, 2022; originally announced April 2022.

Comments: arXiv admin note: text overlap with arXiv:1806.06537

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.

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.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 1 (January 29, 2021) lmcs:5041

Boolean-like algebras of finite dimension

Authors: Antonio Bucciarelli, Antonio Ledda, Francesco Paoli, Antonino Salibra

Abstract: We continue the investigation of Boolean-like algebras of dimension n (nBA) having n constants e1,...,en, and an (n+1)-ary operation q (a "generalised if-then-else") that induces a decomposition of the algebra into n factors through the so-called n-central elements. Varieties of nBAs share many remarkable properties with the variety of Boolean algebras and with primal varieties. Exploiting the con… ▽ More We continue the investigation of Boolean-like algebras of dimension n (nBA) having n constants e1,...,en, and an (n+1)-ary operation q (a "generalised if-then-else") that induces a decomposition of the algebra into n factors through the so-called n-central elements. Varieties of nBAs share many remarkable properties with the variety of Boolean algebras and with primal varieties. Exploiting the concept of central element, we extend the notion of Boolean power to that of semiring power and we prove two representation theorems: (i) Any pure nBA is isomorphic to the algebra of n-central elements of a Boolean vector space; (ii) Any member of a variety of nBAs with one generator is isomorphic to a Boolean power of this generator. This gives a new proof of Foster's theorem on primal varieties. △ Less

Submitted 25 October, 2022; v1 submitted 18 June, 2018; originally announced June 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.

Journal ref: Logical Methods in Computer Science, Volume 14, Issue 3 (August 3, 2018) lmcs:4139

Minimal lambda-theories by ultraproducts

Authors: Antonio Bucciarelli, Alberto Carraro, Antonino Salibra

Abstract: A longstanding open problem in lambda calculus is whether there exist continuous models of the untyped lambda calculus whose theory is exactly the least lambda-theory lambda-beta or the least sensible lambda-theory H (generated by equating all the unsolvable terms). A related question is whether, given a class of lambda models, there is a minimal lambda-theory represented by it. In this paper, we… ▽ More A longstanding open problem in lambda calculus is whether there exist continuous models of the untyped lambda calculus whose theory is exactly the least lambda-theory lambda-beta or the least sensible lambda-theory H (generated by equating all the unsolvable terms). A related question is whether, given a class of lambda models, there is a minimal lambda-theory represented by it. In this paper, we give a general tool to answer positively to this question and we apply it to a wide class of webbed models: the i-models. The method then applies also to graph models, Krivine models, coherent models and filter models. In particular, we build an i-model whose theory is the set of equations satisfied in all i-models. △ Less

Submitted 29 March, 2013; originally announced March 2013.

Comments: In Proceedings LSFA 2012, arXiv:1303.7136

ACM Class: F.4.1; F.3.2

Journal ref: EPTCS 113, 2013, pp. 61-76

Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion

Authors: Thomas Ehrhard, Antonio Bucciarelli, Alberto Carraro, Giulio Manzonetto

Abstract: We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend… ▽ More We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a "must" parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula. As an intermediate result we prove that the exception mechanism is not essential in the finite sub-calculus. △ Less

Submitted 8 October, 2012; v1 submitted 13 September, 2012; originally announced September 2012.

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 4 (October 10, 2012) lmcs:1047

Extensional Collapse Situations I: non-termination and unrecoverable errors

Authors: Antonio Bucciarelli

Abstract: We consider a simple model of higher order, functional computation over the booleans. Then, we enrich the model in order to encompass non-termination and unrecoverable errors, taken separately or jointly. We show that the models so defined form a lattice when ordered by the extensional collapse situation relation, introduced in order to compare models with respect to the amount of "intensional inf… ▽ More We consider a simple model of higher order, functional computation over the booleans. Then, we enrich the model in order to encompass non-termination and unrecoverable errors, taken separately or jointly. We show that the models so defined form a lattice when ordered by the extensional collapse situation relation, introduced in order to compare models with respect to the amount of "intensional information" that they provide on computation. The proofs are carried out by exhibiting suitable applied λ-calculi, and by exploiting the fundamental lemma of logical relations. △ Less

Submitted 24 January, 2011; originally announced January 2011.

On Linear Information Systems

Authors: A. Bucciarelli, A. Carraro, T. Ehrhard, A. Salibra

Abstract: Scott's information systems provide a categorically equivalent, intensional description of Scott domains and continuous functions. Following a well established pattern in denotational semantics, we define a linear version of information systems, providing a model of intuitionistic linear logic (a new-Seely category), with a "set-theoretic" interpretation of exponentials that recovers Scott continu… ▽ More Scott's information systems provide a categorically equivalent, intensional description of Scott domains and continuous functions. Following a well established pattern in denotational semantics, we define a linear version of information systems, providing a model of intuitionistic linear logic (a new-Seely category), with a "set-theoretic" interpretation of exponentials that recovers Scott continuous functions via the co-Kleisli construction. From a domain theoretic point of view, linear information systems are equivalent to prime algebraic Scott domains, which in turn generalize prime algebraic lattices, already known to provide a model of classical linear logic. △ Less

Submitted 29 March, 2010; originally announced March 2010.

Journal ref: EPTCS 22, 2010, pp. 38-48