Showing 1–37 of 37 results for author: Díaz-Caro, A

A feasible and unitary quantum programming language

Authors: Alejandro Díaz-Caro, Emmanuel Hainry, Romain Péchoux, Mário Silva

Abstract: We introduce a novel quantum programming language featuring higher-order programs and quantum controlflow which ensures that all qubit transformations are unitary. Our language boasts a type system guaranteeingboth unitarity and polynomial-time normalization. Unitarity is achieved by using a special modality forsuperpositions while requiring orthogonality among superposed terms. Polynomial-time no… ▽ More We introduce a novel quantum programming language featuring higher-order programs and quantum controlflow which ensures that all qubit transformations are unitary. Our language boasts a type system guaranteeingboth unitarity and polynomial-time normalization. Unitarity is achieved by using a special modality forsuperpositions while requiring orthogonality among superposed terms. Polynomial-time normalization isachieved using a linear-logic-based type discipline employing Barber and Plotkin duality along with a specificmodality to account for potential duplications. This type discipline also guarantees that derived values havepolynomial size. Our language seamlessly combines the two modalities: quantum circuit programs upholdunitarity, and all programs are evaluated in polynomial time, ensuring their feasibility. △ Less

Submitted 5 March, 2024; v1 submitted 2 November, 2023; originally announced November 2023.

A linear proof language for second-order intuitionistic linear logic

Authors: Alejandro Díaz-Caro, Gilles Dowek, Malena Ivnisky, Octavio Malherbe

Abstract: We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level. We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level. △ Less

Submitted 25 January, 2024; v1 submitted 12 October, 2023; originally announced October 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:2201.11221

Journal ref: (WoLLIC 2024) - LNCS 14672:18-35, 2024

A General Probabilistic Framework in IMALL: A Concrete Categorical Perspective

Authors: Alejandro Díaz-Caro, Octavio Malherbe

Abstract: We consider the linear lambda-calculus extended with the sup type constructor, which provides an additive conjunction along with a non-deterministic destructor. The sup type constructor has been introduced in the context of quantum computing. In this paper, we study this type constructor within a simple linear logic categorical model, employing the category of semimodules over a commutative semiri… ▽ More We consider the linear lambda-calculus extended with the sup type constructor, which provides an additive conjunction along with a non-deterministic destructor. The sup type constructor has been introduced in the context of quantum computing. In this paper, we study this type constructor within a simple linear logic categorical model, employing the category of semimodules over a commutative semiring. We demonstrate that the non-deterministic destructor, either weighted or not, finds a suitable model in a weighted codiagonal map. Our approach offers a valid and insightful alternative to interpreting non-determinism and probability calculi, in instances where the conventional Moggi's Powerset Monad interpretation does not align with the category's structure, as is the case with the category of semimodules. The validity of this alternative relies on the presence of biproducts within the category. △ Less

Submitted 12 April, 2024; v1 submitted 8 September, 2023; originally announced September 2023.

Comments: There is a mistake in the adequacy proof for the first language. The other languages have been integrated into arXiv:2205.02142, making this paper merely a concrete example

The Sup Connective in IMALL: A Categorical Semantics

Authors: Alejandro Díaz-Caro, Octavio Malherbe

Abstract: We explore a proof language for intuitionistic multiplicative additive linear logic, incorporating the sup connective that introduces additive pairs with a probabilistic elimination, and sum and scalar products within the proof-terms. We provide an abstract characterization of the language, revealing that any symmetric monoidal closed category with biproducts and a monomorphism from the semiring o… ▽ More We explore a proof language for intuitionistic multiplicative additive linear logic, incorporating the sup connective that introduces additive pairs with a probabilistic elimination, and sum and scalar products within the proof-terms. We provide an abstract characterization of the language, revealing that any symmetric monoidal closed category with biproducts and a monomorphism from the semiring of scalars to the semiring Hom(I,I) is suitable for the job. Leveraging the binary biproducts, we define a weighted codiagonal map at the heart of the sup connective. △ Less

Submitted 10 April, 2024; v1 submitted 4 May, 2022; originally announced May 2022.

MSC Class: 18M45 03F52 03B70

A Quick Overview on the Quantum Control Approach to the Lambda Calculus

Authors: Alejandro Díaz-Caro

Abstract: In this short overview, we start with the basics of quantum computing, explaining the difference between the quantum and the classical control paradigms. We give an overview of the quantum control line of research within the lambda calculus, ranging from untyped calculi up to categorical and realisability models. This is a summary of the last 10+ years of research in this area, starting from Arrig… ▽ More In this short overview, we start with the basics of quantum computing, explaining the difference between the quantum and the classical control paradigms. We give an overview of the quantum control line of research within the lambda calculus, ranging from untyped calculi up to categorical and realisability models. This is a summary of the last 10+ years of research in this area, starting from Arrighi and Dowek's seminal work until today. △ Less

Submitted 8 April, 2022; originally announced April 2022.

Comments: In Proceedings LSFA 2021, arXiv:2204.03415

Journal ref: EPTCS 357, 2022, pp. 1-17

A linear linear lambda-calculus

Authors: Alejandro Díaz-Caro, Gilles Dowek

Abstract: We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part of a broader research program aiming to define a logic with a proof language that forms a quantum programming language. We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part of a broader research program aiming to define a logic with a proof language that forms a quantum programming language. △ Less

Submitted 9 April, 2024; v1 submitted 26 January, 2022; originally announced January 2022.

Comments: This is the full revised journal version of the FSCD 2022 paper published at LIPIcs 228:21, 2022

A Note on Confluence in Typed Probabilistic Lambda Calculi

Authors: Rafael Romero, Alejandro Díaz-Caro

Abstract: On the topic of probabilistic rewriting, there are several works studying both termination and confluence of different systems. While working with a lambda calculus modelling quantum computation, we found a system with probabilistic rewriting rules and strongly normalizing terms. We examine the effect of small modifications in probabilistic rewriting, affine variables, and strategies on the overal… ▽ More On the topic of probabilistic rewriting, there are several works studying both termination and confluence of different systems. While working with a lambda calculus modelling quantum computation, we found a system with probabilistic rewriting rules and strongly normalizing terms. We examine the effect of small modifications in probabilistic rewriting, affine variables, and strategies on the overall confluence in this strongly normalizing probabilistic calculus. △ Less

Submitted 8 April, 2022; v1 submitted 11 June, 2021; originally announced June 2021.

Comments: In Proceedings LSFA 2021, arXiv:2204.03415

Journal ref: EPTCS 357, 2022, pp. 18-24

Polymorphic System I

Authors: Cristian F. Sottile, Alejandro Díaz-Caro, Pablo E. Martínez López

Abstract: System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an extension of System I to polymorphic types, adding the corresponding isomorphisms. We provide non-standard proofs of subject reduction and strong normalisation, extending those of System I. System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an extension of System I to polymorphic types, adding the corresponding isomorphisms. We provide non-standard proofs of subject reduction and strong normalisation, extending those of System I. △ Less

Submitted 19 May, 2021; v1 submitted 8 January, 2021; originally announced January 2021.

Comments: 20 pages plus appendix

Journal ref: In IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages (IFL 2020). Association for Computing Machinery, New York, NY, USA, 127-137

A New Connective in Natural Deduction, and its Application to Quantum Computing

Authors: Alejandro Díaz-Caro, Gilles Dowek

Abstract: We investigate an unsuspected connection between logical connectives with non-harmonious deduction rules, such as Prior's tonk, and quantum computing. We argue that these connectives model the information-erasure, the non-reversibility, and the non-determinism that occur, among other places, in quantum measurement. We introduce an intuitionistic propositional logic with a non-harmonious logical co… ▽ More We investigate an unsuspected connection between logical connectives with non-harmonious deduction rules, such as Prior's tonk, and quantum computing. We argue that these connectives model the information-erasure, the non-reversibility, and the non-determinism that occur, among other places, in quantum measurement. We introduce an intuitionistic propositional logic with a non-harmonious logical connective sup and two interstitial rules, and show that the proof language of this logic forms the core of a quantum programming language. △ Less

Submitted 21 March, 2023; v1 submitted 16 December, 2020; originally announced December 2020.

Comments: Accepted at TCS

Journal ref: Theoretical Computer Science 957:113840, 2023

Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model

Authors: Alejandro Díaz-Caro, Octavio Malherbe

Abstract: In a recent paper, a realizability technique has been used to give a semantics of a quantum lambda calculus. Such a technique gives rise to an infinite number of valid ty** rules, without giving preference to any subset of those. In this paper, we introduce a valid subset of ty** rules, defining an expressive enough quantum calculus. Then, we propose a categorical semantics for it. Such a sema… ▽ More In a recent paper, a realizability technique has been used to give a semantics of a quantum lambda calculus. Such a technique gives rise to an infinite number of valid ty** rules, without giving preference to any subset of those. In this paper, we introduce a valid subset of ty** rules, defining an expressive enough quantum calculus. Then, we propose a categorical semantics for it. Such a semantics consists of an adjunction between the category of distributive-action spaces of value distributions (that is, linear combinations of values in the lambda calculus), and the category of sets of value distributions. △ Less

Submitted 9 September, 2022; v1 submitted 10 December, 2020; originally announced December 2020.

MSC Class: 18C50; 03B40

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 3 (September 12, 2022) lmcs:7408

The Vectorial Lambda Calculus Revisited

Authors: Francisco Noriega, Alejandro Díaz-Caro

Abstract: We revisit the Vectorial Lambda Calculus, a typed version of Lineal. Vectorial (as well as Lineal) has been originally designed for quantum computing, as an extension to System F where linear combinations of lambda terms are also terms and linear combinations of types are also types. In its first presentation, Vectorial only provides a weakened version of the Subject Reduction property. We prove t… ▽ More We revisit the Vectorial Lambda Calculus, a typed version of Lineal. Vectorial (as well as Lineal) has been originally designed for quantum computing, as an extension to System F where linear combinations of lambda terms are also terms and linear combinations of types are also types. In its first presentation, Vectorial only provides a weakened version of the Subject Reduction property. We prove that our revised Vectorial Lambda Calculus supports the standard version of said property, answering a long standing issue. In addition we also introduce the concept of weight of types and terms, and prove a relation between the weight of terms and of its types. △ Less

Submitted 14 May, 2021; v1 submitted 7 July, 2020; originally announced July 2020.

Comments: Long version with detailed proofs

Functional Pearl: The Distributive $λ$-Calculus

Authors: Beniamino Accattoli, Alejandro Díaz-Caro

Abstract: We introduce a simple extension of the $λ$-calculus with pairs---called the distributive $λ$-calculus---obtained by adding a computational interpretation of the valid distributivity isomorphism $A \Rightarrow (B\wedge C)\ \ \equiv\ \ (A\Rightarrow B) \wedge (A\Rightarrow C)$ of simple types. We study the calculus both as an untyped and as a simply typed setting. Key features of the untyped calculu… ▽ More We introduce a simple extension of the $λ$-calculus with pairs---called the distributive $λ$-calculus---obtained by adding a computational interpretation of the valid distributivity isomorphism $A \Rightarrow (B\wedge C)\ \ \equiv\ \ (A\Rightarrow B) \wedge (A\Rightarrow C)$ of simple types. We study the calculus both as an untyped and as a simply typed setting. Key features of the untyped calculus are confluence, the absence of clashes of constructs, that is, evaluation never gets stuck, and a leftmost-outermost normalization theorem, obtained with straightforward proofs. With respect to simple types, we show that the new rules satisfy subject reduction if types are considered up to the distributivity isomorphism. The main result is strong normalization for simple types up to distributivity. The proof is a smooth variation over the one for the $λ$-calculus with pairs and simple types. △ Less

Submitted 29 July, 2020; v1 submitted 18 February, 2020; originally announced February 2020.

Comments: 17 pages. Accepted at FLOPS 2020

Journal ref: LNCS 12073:13-32, 2020

Extensional proofs in a propositional logic modulo isomorphisms

Authors: Alejandro Díaz-Caro, Gilles Dowek

Abstract: System I is a proof language for a fragment of propositional logic where isomorphic propositions, such as $A\wedge B$ and $B\wedge A$, or $A\Rightarrow(B\wedge C)$ and $(A\Rightarrow B)\wedge(A\Rightarrow C)$ are made equal. System I enjoys the strong normalization property. This is sufficient to prove the existence of empty types, but not to prove the introduction property (every closed term in n… ▽ More System I is a proof language for a fragment of propositional logic where isomorphic propositions, such as $A\wedge B$ and $B\wedge A$, or $A\Rightarrow(B\wedge C)$ and $(A\Rightarrow B)\wedge(A\Rightarrow C)$ are made equal. System I enjoys the strong normalization property. This is sufficient to prove the existence of empty types, but not to prove the introduction property (every closed term in normal form is an introduction). Moreover, a severe restriction had to be made on the types of the variables in order to obtain the existence of empty types. We show here that adding $η$-expansion rules to System I permits to drop this restriction, and yields a strongly normalizing calculus which enjoys the full introduction property. △ Less

Submitted 30 August, 2023; v1 submitted 10 February, 2020; originally announced February 2020.

Comments: 29 pages

MSC Class: 03F05; 03B40; 03B38

Journal ref: Theoretical Computer Science 977:114172, 2023

Runtime Analysis of Quantum Programs: A Formal Approach

Authors: Federico Olmedo, Alejandro Díaz-Caro

Abstract: In this abstract we study the resource consumption of quantum programs. Specifically, we focus on the expected runtime of programs and, inspired by recent methods for probabilistic programs, we develop a calculus à la weakest precondition to formally and systematically derive the (exact) expected runtime of quantum programs. Notably, the calculus admits a notion of loop runtime invariant that can… ▽ More In this abstract we study the resource consumption of quantum programs. Specifically, we focus on the expected runtime of programs and, inspired by recent methods for probabilistic programs, we develop a calculus à la weakest precondition to formally and systematically derive the (exact) expected runtime of quantum programs. Notably, the calculus admits a notion of loop runtime invariant that can be readily used to derive upper bounds of their runtime. Finally, we show the applicability of our calculus analyzing the runtime of (a simplified version of) the BB84 quantum key distribution protocol. △ Less

Submitted 27 December, 2019; v1 submitted 25 November, 2019; originally announced November 2019.

Comments: Accepted at PLanQC 2020

A categorical construction for the computational definition of vector spaces

Authors: Alejandro Díaz-Caro, Octavio Malherbe

Abstract: Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other is to consider all lambda-terms as algebraic linear functions. The type system of Lambda-S has a constructor S such that a type A is considered as the base of a vector space while S(A) is its span. Lambda-S can also be… ▽ More Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other is to consider all lambda-terms as algebraic linear functions. The type system of Lambda-S has a constructor S such that a type A is considered as the base of a vector space while S(A) is its span. Lambda-S can also be seen as a language for the computational manipulation of vector spaces: The vector spaces axioms are given as a rewrite system, describing the computational steps to be performed. In this paper we give an abstract categorical semantics of Lambda-S* (a fragment of Lambda-S), showing that S can be interpreted as the composition of two functors in an adjunction relation between a Cartesian category and an additive symmetric monoidal category. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning. △ Less

Submitted 11 April, 2020; v1 submitted 4 May, 2019; originally announced May 2019.

Comments: 39 pages. Applied Categorical Structures (2020). arXiv admin note: text overlap with arXiv:1806.09236

Journal ref: Applied Categorical Structures 28(5):807-844, 2020

Realizability in the Unitary Sphere

Authors: Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel, Benoît Valiron

Abstract: In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a long standing issue. We derive from the semantics a set of ty** rules for a simply-typed linear algebraic lambda-calculus, and show how it extends both to classical and quantum lambda-calculi. In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a long standing issue. We derive from the semantics a set of ty** rules for a simply-typed linear algebraic lambda-calculus, and show how it extends both to classical and quantum lambda-calculi. △ Less

Submitted 18 April, 2019; originally announced April 2019.

Comments: 28 pages

Journal ref: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019)

Classically Time-Controlled Quantum Automata: Definition and Properties

Authors: Alejandro Díaz-Caro, Marcos Villagra

Abstract: In this paper, we introduce classically time-controlled quantum automata or CTQA, which is a reasonable modification of Moore-Crutchfield quantum finite automata that uses time-dependent evolution and a "scheduler" defining how long each Hamiltonian will run. Surprisingly enough, time-dependent evolution provides a significant change in the computational power of quantum automata with respect to a… ▽ More In this paper, we introduce classically time-controlled quantum automata or CTQA, which is a reasonable modification of Moore-Crutchfield quantum finite automata that uses time-dependent evolution and a "scheduler" defining how long each Hamiltonian will run. Surprisingly enough, time-dependent evolution provides a significant change in the computational power of quantum automata with respect to a discrete quantum model. Indeed, we show that if a scheduler is not computationally restricted, then a CTQA can decide the Halting problem. In order to unearth the computational capabilities of CTQAs we study the case of a computationally restricted scheduler. In particular, we showed that depending on the type of restriction imposed on the scheduler, a CTQA can (i) recognize non-regular languages with cut-point, even in the presence of Karp-Lipton advice, and (ii) recognize non-regular promise languages with bounded-error. Furthermore, we study the cutpoint-union of cutpoint languages by introducing a new model of Moore-Crutchfield quantum finite automata with a rotating tape head. CTQA presents itself as a new model of computation that provides a different approach to a formal study of "classical control, quantum data" schemes in quantum computing. △ Less

Submitted 29 September, 2022; v1 submitted 14 July, 2018; originally announced July 2018.

Comments: Long revisited version of LNCS 11324:266-278, 2018 (TPNC 2018)

MSC Class: 68Q05; 68Q45; 81P68 ACM Class: F.1.1

A concrete model for a typed linear algebraic lambda calculus

Authors: Alejandro Díaz-Caro, Octavio Malherbe

Abstract: We give an adequate, concrete, categorical-based model for Lambda-S, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables, and to consider all lambda-terms as algebraic linear functions. The type system o… ▽ More We give an adequate, concrete, categorical-based model for Lambda-S, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables, and to consider all lambda-terms as algebraic linear functions. The type system of Lambda-S have a superposition constructor S such that a type A is considered as the base of a vector space while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over C. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning. △ Less

Submitted 11 October, 2023; v1 submitted 24 June, 2018; originally announced June 2018.

Comments: Extended revisited version of ENTCS 344:83-100, 2018

Journal ref: Mathematical Structures in Computer Science 34(1):1-44, 2023

Confluence in Probabilistic Rewriting

Authors: Alejandro Díaz-Caro, Guido Martínez

Abstract: Driven by the interest of reasoning about probabilistic programming languages, we set out to study a notion of unicity of normal forms for them. To provide a tractable proof method for it, we define a property of distribution confluence which is shown to imply the desired uniqueness (even for infinite sequences of reduction) and further properties. We then carry over several criteria from the clas… ▽ More Driven by the interest of reasoning about probabilistic programming languages, we set out to study a notion of unicity of normal forms for them. To provide a tractable proof method for it, we define a property of distribution confluence which is shown to imply the desired uniqueness (even for infinite sequences of reduction) and further properties. We then carry over several criteria from the classical case, such as Newman's lemma, to simplify proving confluence in concrete languages. Using these criteria, we obtain simple proofs of confluence for $λ_1$, an affine probabilistic $λ$-calculus, and for Q$^*$, a quantum programming language for which a related property has already been proven in the literature. △ Less

Submitted 30 April, 2018; v1 submitted 11 August, 2017; originally announced August 2017.

Comments: LSFA 2017 Final version

Journal ref: ENTCS 338:115-131, 2018

A lambda calculus for density matrices with classical and probabilistic controls

Authors: Alejandro Díaz-Caro

Abstract: In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, $λ_ρ$, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, $λ_ρ^\circ$, take advantage of the density matrices presentation in order to… ▽ More In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, $λ_ρ$, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, $λ_ρ^\circ$, take advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach. △ Less

Submitted 20 November, 2017; v1 submitted 28 April, 2017; originally announced May 2017.

Comments: This version includes a 11-pages appendix with proofs, and a small fix in the definition of property P(b,A)

Journal ref: LNCS 10695:448-467 (APLAS 2017)

Retractions in Intersection Types

Authors: Mario Coppo, Mariangiola Dezani-Ciancaglini, Alejandro Díaz-Caro, Ines Margaria, Maddalena Zacchi

Abstract: This paper deals with retraction - intended as isomorphic embedding - in intersection types building left and right inverses as terms of a lambda calculus with a bottom constant. The main result is a necessary and sufficient condition two strict intersection types must satisfy in order to assure the existence of two terms showing the first type to be a retract of the second one. Moreover, the… ▽ More This paper deals with retraction - intended as isomorphic embedding - in intersection types building left and right inverses as terms of a lambda calculus with a bottom constant. The main result is a necessary and sufficient condition two strict intersection types must satisfy in order to assure the existence of two terms showing the first type to be a retract of the second one. Moreover, the characterisation of retraction in the standard intersection types is discussed. △ Less

Submitted 7 February, 2017; originally announced February 2017.

Comments: In Proceedings ITRS 2016, arXiv:1702.01874

ACM Class: F.4.1, Lambda calculus and related systems, D.3.3, Polymorphism

Journal ref: EPTCS 242, 2017, pp. 31-47

Affine computation and affine automaton

Authors: Alejandro Díaz-Caro, Abuzer Yakaryılmaz

Abstract: We introduce a quantum-like classical computational model, called affine computation, as a generalization of probabilistic computation. After giving the basics of affine computation, we define affine finite automata (AfA) and compare it with quantum and probabilistic finite automata (QFA and PFA, respectively) with respect to three basic language recognition modes. We show that, in the cases of bo… ▽ More We introduce a quantum-like classical computational model, called affine computation, as a generalization of probabilistic computation. After giving the basics of affine computation, we define affine finite automata (AfA) and compare it with quantum and probabilistic finite automata (QFA and PFA, respectively) with respect to three basic language recognition modes. We show that, in the cases of bounded and unbounded error, AfAs are more powerful than QFAs and PFAs, and, in the case of nondeterministic computation, AfAs are more powerful than PFAs but equivalent to QFAs. △ Less

Submitted 26 February, 2016; v1 submitted 15 February, 2016; originally announced February 2016.

Comments: 23 pages. New results were added. Accepted to CSR2016!

Journal ref: LNCS 9691:146-160, 2016

Two linearities for quantum computing in the lambda calculus

Authors: Alejandro Díaz-Caro, Gilles Dowek, Juan Pablo Rinaldi

Abstract: We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, whi… ▽ More We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis. △ Less

Submitted 31 July, 2019; v1 submitted 17 January, 2016; originally announced January 2016.

Comments: Long journal version of TPNC'17 paper (doi:10.1007/978-3-319-71069-3_22) extended with third author's "Licenciatura"'s thesis

Journal ref: Biosystems Volume 186, December 2019, 104012. Post proceedings of TPNC'17

Isomorphisms considered as equalities: Projecting functions and enhancing partial application through and implementation of lambda+

Authors: Alejandro Díaz-Caro, Pablo E. Martínez López

Abstract: We propose an implementation of lambda+, a recently introduced simply typed lambda-calculus with pairs where isomorphic types are made equal. The rewrite system of lambda+ is a rewrite system modulo an equivalence relation, which makes its implementation non-trivial. We also extend lambda+ with natural numbers and general recursion and use Bekić's theorem to split mutual recursions. This splitting… ▽ More We propose an implementation of lambda+, a recently introduced simply typed lambda-calculus with pairs where isomorphic types are made equal. The rewrite system of lambda+ is a rewrite system modulo an equivalence relation, which makes its implementation non-trivial. We also extend lambda+ with natural numbers and general recursion and use Bekić's theorem to split mutual recursions. This splitting, together with the features of lambda+, allows for a novel way of program transformation by reduction, by projecting a function before it is applied in order to simplify it. Also, currying together with the associativity and commutativity of pairs gives an enhanced form of partial application. △ Less

Submitted 11 February, 2016; v1 submitted 30 November, 2015; originally announced November 2015.

Comments: A prototype writen in Haskell can be found at http://diaz-caro.web.unq.edu.ar/IsoAsEq-v1.0.tar.gz

ACM Class: F.4.1

Journal ref: ACM Proceedings of IFL'15(9), 2015

Proof Normalisation in a Logic Identifying Isomorphic Propositions

Authors: Alejandro Díaz-Caro, Gilles Dowek

Abstract: We define a fragment of propositional logic where isomorphic propositions, such as $A\land B$ and $B\land A$, or $A\Rightarrow (B\land C)$ and $(A\Rightarrow B)\land(A\Rightarrow C)$ are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency. We define a fragment of propositional logic where isomorphic propositions, such as $A\land B$ and $B\land A$, or $A\Rightarrow (B\land C)$ and $(A\Rightarrow B)\land(A\Rightarrow C)$ are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency. △ Less

Submitted 22 April, 2019; v1 submitted 25 January, 2015; originally announced January 2015.

Journal ref: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) - LIPIcs 131:14, 2019

The probability of non-confluent systems

Authors: Alejandro Díaz-Caro, Gilles Dowek

Abstract: We show how to provide a structure of probability space to the set of execution traces on a non-confluent abstract rewrite system, by defining a variant of a Lebesgue measure on the space of traces. Then, we show how to use this probability space to transform a non-deterministic calculus into a probabilistic one. We use as example Lambda+, a recently introduced calculus defined through type isomor… ▽ More We show how to provide a structure of probability space to the set of execution traces on a non-confluent abstract rewrite system, by defining a variant of a Lebesgue measure on the space of traces. Then, we show how to use this probability space to transform a non-deterministic calculus into a probabilistic one. We use as example Lambda+, a recently introduced calculus defined through type isomorphisms. △ Less

Submitted 31 March, 2014; originally announced April 2014.

Comments: In Proceedings DCM 2013, arXiv:1403.7685

Journal ref: EPTCS 144, 2014, pp. 1-15

Call-by-value non-determinism in a linear logic type discipline

Authors: Alejandro Díaz-Caro, Giulio Manzonetto, Michele Pagani

Abstract: We consider the call-by-value lambda-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the relational semantics of linear logic and non-idempotent intersection types, we endow this calculus with a type system based on the so-called Girard's second translation of intuitionistic logic into linear logic. We prove t… ▽ More We consider the call-by-value lambda-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the relational semantics of linear logic and non-idempotent intersection types, we endow this calculus with a type system based on the so-called Girard's second translation of intuitionistic logic into linear logic. We prove that a term is typable if and only if it is converging, and that its ty** tree carries enough information to give a bound on the length of its lazy call-by-value reduction. Moreover, when the ty** tree is minimal, such a bound becomes the exact length of the reduction. △ Less

Submitted 16 December, 2013; originally announced December 2013.

Journal ref: Logical Foundations of Computer Science 7734 (2013) 164-178

The Vectorial $λ$-Calculus

Authors: Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron

Abstract: We describe a type system for the linear-algebraic $λ$-calculus. The type system accounts for the linear-algebraic aspects of this extension of $λ$-calculus: it is able to statically describe the linear combinations of terms that will be obtained when reducing the programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations.… ▽ More We describe a type system for the linear-algebraic $λ$-calculus. The type system accounts for the linear-algebraic aspects of this extension of $λ$-calculus: it is able to statically describe the linear combinations of terms that will be obtained when reducing the programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We prove that the resulting typed $λ$-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus. △ Less

Submitted 17 April, 2017; v1 submitted 5 August, 2013; originally announced August 2013.

Comments: Long and corrected version of arXiv:1012.4032 (EPTCS 88:1-15), to appear in Information and Computation

Journal ref: Information and computation 254(1):105-139, 2017

Normalisation of a Non-deterministic Type Isomorphic λ-calculus

Authors: Alejandro Díaz-Caro, Gilles Dowek

Abstract: We provide a proof of strong normalisation for lambda+, a recently introduced, explicitly typed, non-deterministic lambda-calculus where isomorphic propositions are identified. Such a proof is a non-trivial adaptation of the reducibility candidates technique. We provide a proof of strong normalisation for lambda+, a recently introduced, explicitly typed, non-deterministic lambda-calculus where isomorphic propositions are identified. Such a proof is a non-trivial adaptation of the reducibility candidates technique. △ Less

Submitted 8 January, 2014; v1 submitted 21 June, 2013; originally announced June 2013.

Comments: This paper has been withdrawn by the authors due to a crucial error in Definition 1

Non determinism through type isomorphism

Authors: Alejandro Díaz-Caro, Gilles Dowek

Abstract: We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-deterministic and algebraic lambda-calculi. We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-deterministic and algebraic lambda-calculi. △ Less

Submitted 29 March, 2013; originally announced March 2013.

Comments: In Proceedings LSFA 2012, arXiv:1303.7136

Journal ref: EPTCS 113, 2013, pp. 137-144

Confluence via strong normalisation in an algebraic λ-calculus with rewriting

Authors: Pablo Buiras, Alejandro Díaz-Caro, Mauro Jaskelioff

Abstract: The linear-algebraic lambda-calculus and the algebraic lambda-calculus are untyped lambda-calculi extended with arbitrary linear combinations of terms. The former presents the axioms of linear algebra in the form of a rewrite system, while the latter uses equalities. When given by rewrites, algebraic lambda-calculi are not confluent unless further restrictions are added. We provide a type system f… ▽ More The linear-algebraic lambda-calculus and the algebraic lambda-calculus are untyped lambda-calculi extended with arbitrary linear combinations of terms. The former presents the axioms of linear algebra in the form of a rewrite system, while the latter uses equalities. When given by rewrites, algebraic lambda-calculi are not confluent unless further restrictions are added. We provide a type system for the linear-algebraic lambda-calculus enforcing strong normalisation, which gives back confluence. The type system allows an abstract interpretation in System F. △ Less

Submitted 28 March, 2012; v1 submitted 3 February, 2011; originally announced February 2011.

Comments: In Proceedings LSFA 2011, arXiv:1203.5423

Journal ref: EPTCS 81, 2012, pp. 16-29

A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus

Authors: Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron

Abstract: We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations… ▽ More We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambda-calculus is strongly normalizing and features a weak subject-reduction. △ Less

Submitted 30 July, 2012; v1 submitted 17 December, 2010; originally announced December 2010.

Comments: In Proceedings DCM 2011, arXiv:1207.6821

Journal ref: EPTCS 88, 2012, pp. 1-15

Linearity in the non-deterministic call-by-value setting

Authors: Alejandro Díaz-Caro, Barbara Petit

Abstract: We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F w… ▽ More We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting. △ Less

Submitted 15 June, 2012; v1 submitted 15 November, 2010; originally announced November 2010.

Comments: 15 pages. To appear in WoLLIC 2012

Journal ref: Lecture Notes in Computer Science 7456, 216-231 (2012)

Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus

Authors: Ali Assaf, Alejandro Díaz-Caro, Simon Perdrix, Christine Tasson, Benoî t Valiron

Abstract: We examine the relationship between the algebraic lambda-calculus, a fragment of the differential lambda-calculus and the linear-algebraic lambda-calculus, a candidate lambda-calculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalar-multiplicative structure, and their set of terms is closed under linear combinations. However, the two languages… ▽ More We examine the relationship between the algebraic lambda-calculus, a fragment of the differential lambda-calculus and the linear-algebraic lambda-calculus, a candidate lambda-calculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalar-multiplicative structure, and their set of terms is closed under linear combinations. However, the two languages were built using different approaches: the former is a call-by-name language whereas the latter is call-by-value; the former considers algebraic equalities whereas the latter approaches them through rewrite rules. In this paper, we analyse how these different approaches relate to one another. To this end, we propose four canonical languages based on each of the possible choices: call-by-name versus call-by-value, algebraic equality versus algebraic rewriting. We show that the various languages simulate one another. Due to subtle interaction between beta-reduction and algebraic rewriting, to make the languages consistent some additional hypotheses such as confluence or normalisation might be required. We carefully devise the required properties for each proof, making them general enough to be valid for any sub-language satisfying the corresponding properties. △ Less

Submitted 9 December, 2014; v1 submitted 17 May, 2010; originally announced May 2010.

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 4 (December 9, 2014) lmcs:927

A System F accounting for scalars

Authors: Pablo Arrighi, Alejandro Diaz-Caro

Abstract: The Algebraic lambda-calculus and the Linear-Algebraic lambda-calculus extend the lambda-calculus with the possibility of making arbitrary linear combinations of terms. In this paper we provide a fine-grained, System F-like type system for the linear-algebraic lambda-calculus. We show that this "scalar" type system enjoys both the subject-reduction property and the strong-normalisation property, o… ▽ More The Algebraic lambda-calculus and the Linear-Algebraic lambda-calculus extend the lambda-calculus with the possibility of making arbitrary linear combinations of terms. In this paper we provide a fine-grained, System F-like type system for the linear-algebraic lambda-calculus. We show that this "scalar" type system enjoys both the subject-reduction property and the strong-normalisation property, our main technical results. The latter yields a significant simplification of the linear-algebraic lambda-calculus itself, by removing the need for some restrictions in its reduction rules. But the more important, original feature of this scalar type system is that it keeps track of 'the amount of a type' that is present in each term. As an example of its use, we shown that it can serve as a guarantee that the normal form of a term is barycentric, i.e that its scalars are summing to one. △ Less

Submitted 28 February, 2012; v1 submitted 22 March, 2009; originally announced March 2009.

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 1 (February 27, 2012) lmcs:846

Measurements and confluence in quantum lambda calculi with explicit qubits

Authors: Alejandro Díaz-Caro, Pablo Arrighi, Manuel Gadella, Jonathan Grattage

Abstract: This paper demonstrates how to add a measurement operator to quantum lambda-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages… ▽ More This paper demonstrates how to add a measurement operator to quantum lambda-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML or Lineal, which is the subject of further research. △ Less

Submitted 4 January, 2010; v1 submitted 15 June, 2008; originally announced June 2008.

Comments: 15 pages. Minor changes: final proceedings version. To appear ENTCS: Proceedings of QPL V - DCV IV, Reykjavik, Iceland, 2008

Journal ref: Electronic Notes in Theoretical Computer Science, 270(1):59-74, 2011. Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models (QPL/DCM 2008)

A Discussion on the Teleportation Protocol for States of N Qubits

Authors: Alejandro Diaz-Caro, Manuel Gadella

Abstract: In this paper, we want to present a simple and comprehensive method to implement teleportation of a system of N qubits and its discussion on the corresponding quantum circuit. The paper can be read for nonspecialists in quantum information. In this paper, we want to present a simple and comprehensive method to implement teleportation of a system of N qubits and its discussion on the corresponding quantum circuit. The paper can be read for nonspecialists in quantum information. △ Less

Submitted 12 October, 2005; v1 submitted 2 May, 2005; originally announced May 2005.

Comments: 17 pages, 1 figure