arXiv subjects

Andre Kornell

Publications and source records attributed to Andre Kornell.

27 records · Page 2Linked to original sources

arXiv2021

Quantum CPOs

We introduce the monoidal closed category qCPO of quantum cpos, whose objects are "quantized" analogs of omega-complete partial orders (cpos). The category qCPO is enriched over the category CPO of cpos, and contains both CPO, and the opposite of the category FdAlg of finite-dimensional von Neumann algebras as monoidal subcategories. We use qCPO to construct a sound model for the quantum programming language Proto-Quipper-M (PQM) extended with term recursion, as well as a sound and computationally adequate model for the Linear/Non-Linear Fixpoint Calculus (LNL-FPC), which is both an extension of the Fixpoint Calculus (FPC) with linear types, and an extension of a circuit-free fragment of PQM that includes recursive types.

cs.PL↗

arXiv2021

Semantics for Variational Quantum Programming

We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The classical subsystem of the language is the Probabilistic FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. The quantum subsystem is a first-order linear type system that can manipulate quantum information. The two subsystems are related by mixed classical/quantum terms that specify how classical probabilistic effects are induced by quantum measurements, and conversely, how classical (probabilistic) programs can influence the quantum dynamics. We also describe a sound and computationally adequate denotational semantics for the language. Classical probabilistic effects are interpreted using a recently-described commutative probabilistic monad on DCPO. Quantum effects and resources are interpreted in a category of von Neumann algebras that we show is enriched over (continuous) domains. This strong sense of enrichment allows us to develop novel semantic methods that we use to interpret the relationship between the quantum and classical probabilistic effects. By doing so we provide the first denotational analysis that relates models of classical probabilistic programming to models of quantum programming.

cs.LO↗

arXiv2020

The transfinite mean

We define a generalization of the arithmetic mean to bounded transfinite sequences of real numbers. We show that every probability space admits a transfinite sequences of points such that the measure of each measurable subset is equal to the frequency with which the sequence is in this subset. We include an argument suggested by Woodin that the club filter on $ω_1$ does not admit such a sequence of order type $ω_1$.

math.LO↗

arXiv2018

A complete system of deduction for Sigma formulas

The Sigma formulas of the language of arithmetic express semidecidable relations on the natural numbers. More generally, whenever a totality of objects is regarded as incomplete, the Sigma formulas express relations that are witnessed in a completed portion of that totality when they hold. In this sense, the Sigma formulas are more concrete semantically than other first-order formulas. We describe a system of deduction that uses only Sigma formulas. Each axiom, an implication between two Sigma formulas, is implemented as a rewriting rule for subformulas. We exhibit a complete class of logical axioms for this system, and we observe that a distributive law distinguishes classical reasoning from intuitionistic reasoning in this setting. Skolem's theory PRA of primitive recursive arithmetic can be formulated in our deductive system. In Skolem's system, free variables are universally quantified implicitly, but in our formulation, free variables act as parameters to the deduction. In this sense, our formulation is more explicitly finitistic. Furthermore, most of our results are themselves finistic, being theorems of PRA. In particular, appending our main theorem to a celebrated chain of reductions from reverse mathematics, we find that an implication of Sigma formulas is derivable in WKL_0 if and only if there is a deduction from the antecedent to the consequent in our formulation of PRA.

math.LO↗

arXiv2018

Quantum extensions of ordinary maps

We define a loop to be quantum nullhomotopic if and only if it admits a nonempty quantum set of extensions to the unit disk. We show that the canonical loop in the unit circle is not quantum nullhomotopic, but that every loop in the real projective plane is quantum nullhomotopic. Furthermore, we apply Kuiper's theorem to show that the canonical loop admits a continuous family of extensions to the unit disk that is indexed by an infinite quantum space. We obtain these results using a purely topological condition that we show to be equivalent to the existence of a quantum family of extensions of a given map.

math.OA↗

arXiv2017

On sequents of $Σ$ formulas

We investigate the position that foundational theories should be modelled on ordinary computability. In this context, we investigate the metamathematics of $Σ$ formulas. We consider theories whose axioms are implications between $Σ$ formulas, and we show that arbitrarily strong such theories prove their own correctness. We also show that a natural extension of such a theory proves the validity of intuitionistic reasoning for that theory. Finally, we show the equivalence of two completeness principles appropriate to a potentialist conception of the universe of sets.

math.LO↗

arXiv2016

Quantum Collections

We develop the viewpoint that the opposite of the category of W*-algebras and unital normal *-homomorphisms is analogous to the category of sets and functions. For each pair of W*-algebras, we construct their free exponential, which in the context of this analogy corresponds to the collection of functions from one of these W*-algebras to the other. We also show that every unital normal completely positive map between W*-algebras arises naturally from a normal state on their free exponential.

math.OA↗

arXiv2016

V*-algebras

What is the correct noncommutative generalization of the functor $C_0(X) \mapsto \ell^\infty(X)$ for locally compact Hausdorff $X$ having a countable basis? Making the ansatz $K(\ell^2) \mapsto B(\ell^2)$, we expect that every unital $*$-homomorphism $C(\mathbb T) \rightarrow B(\ell^2)$ extend canonically to a unital $*$-homomorphism $\ell^\infty(\mathbb T) \rightarrow B(\ell^2)$. Thus, we expect to extend the continuous functional calculus for a unitary operator on $\ell^2$ to all bounded complex-valued functions. Therefore, we work in a model of set theory where every set of real numbers is Lebesgue measurable; we must assume the consistency of an inaccessible cardinal in order to do so. The axiom of choice necessarily fails in such a model, but our model is carefully chosen to enable the verification of many familiar theorems via a scrutinization of their statements rather than their proofs. This technique significantly lowers the cost of doing interesting mathematics in this unfamiliar setting, and it is explained in detail. By analogy with the ultraweak topology, we define the continuum-weak topology on bounded operators to be the topology given by functionals of the form $x \mapsto \int_0^1 <η_t| x ξ_t>\, dt$. We then define a V*-algebra to be a C*-algebra of bounded operators that is closed in the continuum-weak topology. Every C*-algebra $A$ has an enveloping V*-algebra $V^*(A)$, and if $X$ is a locally compact Hausdorff space with a countable basis, then $V^*(C_0(X)) \cong \ell^\infty(X)$. More generally, if $A$ is any separable C*-algebra of type I, then $V^*(A)$ is canonically isomorphic to an $\ell^\infty$-direct sum of type I factors, with one summand for each irreducible representation of $A$. The self-adjoint part of any unital separable C*-algebra is isomorphic to the Banach space of strongly affine real-valued functions on its state space.

math.OA↗

arXiv2015

Quantum Functions

Weaver has recently defined the notion of a quantum relation on a von Neumann algebra. We demonstrate that the corresponding notion of a quantum function between two von Neumann algebras coincides with that of a normal unital $*$-homomorphism in the opposite direction. This is essentially a reformulation of a previously known result from the theory of Hilbert von Neumann modules.

math.OA↗