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.
•Introducing a propositional logic with non-harmonious rules and the ⊙ (read “sup”) connective.•The proof language of this logic forms core of a quantum programming language.•Non-harmonious rules of ⊙ model quantum properties of measurement: info-erasure, non-reversibility, non-determinism.
System I is a proof language for a fragment of propositional logic where isomorphic propositions, such as A∧B and B∧A, or A⇒(B∧C) and (A⇒B)∧(A⇒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.
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.
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.
The vectorial λ-calculus Arrighi, Pablo; Díaz-Caro, Alejandro; Valiron, Benoît
Information and computation,
June 2017, 2017-06-00, 2017-06, Volume:
254, Issue:
1
Journal Article
Peer reviewed
Open access
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.
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 typing rules, without giving ...preference to any subset
of those. In this paper, we introduce a valid subset of typing 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.
PDF
