Blog sobre computación cuántica y fundamentos de las ciencias de la computación. En general cubrimos los temas de investigación a los que nosotros nos dedicamos, los cuales comenzaron siendo computación cuántica, y con el tiempo van evolucionando, cambiando, agregando nuevas áreas, etc.
Mañana, luego de casi 8 años, finamente nos vamos a conocer personalmente dos de los autores de este blog: Marcos Villagra, de la Universidad Nacional de Asunción (Paraguay) me visita en la Universidad Nacional de Quilmes (Argentina).
Marcos comenzó a colaborar en el blog en 2009, cuando era estudiante de doctorado en Japón y yo estudiante de doctorado en Francia. Luego de estos años compartiendo el blog, y con ambos haciendo ciencia desde nuestros países de origen, se nos da esta oportunidad de juntarnos a buscar cómo colaborar científicamente y no sólo con la divulgación desde este blog.
Después les contaremos qué sale del encuentro.
We propose a way to unify two approaches of non-cloning in quantum lambda-calculi. 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.
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 unicity 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. Lastly, we show how distribution confluence implies unicity even for distributions that are only reached asymptotically.
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, λρ°, 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.
Density matrices describe quantum systems in mixed state, that is, a statistical set of several quantum states. All the postulates of quantum mechanics can be described in such a formalism, and hence, also quantum computing can be done using density matrices. One advantage of this formalism is that it gives a natural way to reason about the probabilistic outputs of an algorithm. In this talk we present an extension to lambda calculus for density matrices with a linear type system. Its denotational semantics is the set of density matrices and functions upon them, and so, it is possible to equate programs producing the same density matrices. For example the process of tossing a coin, and according to its result, apply Z or not to a balanced superposition, and the process of tossing a coin and not looking at its result, may look quite different in most quantum programming languages. Yet both processes output the same density matrices thus have the same denotation in our calculus.
En esta charla vamos a dar una rápida introducción al cálculo lambda, un modelo de computación equivalente a las Máquinas de Turing, y su relación con la lógica intuicionista. Luego presentaremos diferentes extensiones al cálculo lambda para computación cuántica, en sus dos paradigmas: el paradigma de control clásico y datos cuánticos, orientado principalmente a estudiar propiedades en los lenguajes de programación para la computadora cuántica, y el paradigma de control y datos cuánticos, orientado a estudiar las consecuencias lógicas de la computación cuántica desde un punto de vista computacional.