首页/论文/quant-ph/0501150

arXiv quant-ph/05011502005-01-25quant-ph

Linear-algebraic lambda-calculus

Pablo Arrighi, Gilles Dowek

备注：: LaTeX, 23 pages, 10 figures and the LINEAL language interpreter/simulator file (see "other formats"). See the more recent arXiv:quant-ph/0612199
发表信息：: Quantum Programming Languages 2004, satellite of LICS, Turku Centre for Computer Science General Publication, Vol. 33, (2004)

英文摘要：

With a view towards models of quantum computation and/or the interpretation of linear logic, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an interpreter/simulator) is provided for this language in the form of a term rewrite system. The linear-algebraic lambda-calculus hereby constructed is linear in a different (yet related) sense to that, say, of the linear lambda-calculus. These various notions of linearity are discussed in the context of quantum programming languages. KEYWORDS: quantum lambda-calculus, linear lambda-calculus, $λ$-calculus, quantum logics.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

The lambda-q calculus can efficiently simulate quantum computers

We show that the lambda-q calculus can efficiently simulate quantum Turing machines by showing how the lambda-q calculus can efficiently simulate a class of quantum cellular automaton that are equivalent to quantum Turing machines. We conclude by noting that the lambda-q calculus may be strictly stronger than quantum computers because NP-complete problems such as satisfiability are efficiently solvable in the lambda-q calculus but there is a widespread doubt that they are efficiently solvable by quantum computers.

1997-02-26quant-ph

Extending the Lambda Calculus to Express Randomized and Quantumized Algorithms

This paper introduces a formal metalanguage called the lambda-q calculus for the specification of quantum programming languages. This metalanguage is an extension of the lambda calculus, which provides a formal setting for the specification of classical programming languages. As an intermediary step, we introduce a formal metalanguage called the lambda-p calculus for the specification of programming languages that allow true random number generation. We demonstrate how selected randomized algorithms can be programmed directly in the lambda-p calculus. We also demonstrate how satisfiability can…

1997-01-09quant-ph

Von Neumann Algebras form a Model for the Quantum Lambda Calculus

We present a model of Selinger and Valiron's quantum lambda calculus based on von Neumann algebras, and show that the model is adequate with respect to the operational semantics.

2016-03-07cs.LOmath.OAquant-ph

具有多重测量基的量子控制λ演算

A Quantum-Control Lambda-Calculus with Multiple Measurement Bases

Lambda-SX是一种支持多种测量基的量子λ演算，通过类型系统实现对测量的灵活控制和组合推理，展示了在量子编程语言中整合多种基的可行性。

2025-08-21cs.LOquant-ph

A Lambda Calculus for Quantum Computation

The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine, and continues to be of enormous benefit in the classical theory of computation. We propose that quantum computation, like its classical counterpart, may benefit from a version of the lambda calculus suitable for expressing and reasoning about quantum algorithms. In this paper we develop a quantum lambda calculus as an alternative model of quantum computation, which combines some of the …

2004-04-03cs.LOhep-thquant-ph

Completeness of algebraic CPS simulations

The algebraic lambda calculus and the linear algebraic lambda calculus are two extensions of the classical lambda calculus with linear combinations of terms. They arise independently in distinct contexts: the former is a fragment of the differential lambda calculus, the latter is a candidate lambda calculus for quantum computation. They differ in the handling of application arguments and algebraic rules. The two languages can simulate each other using an algebraic extension of the well-known call-by-value and call-by-name CPS translations. These simulations are sound, in that they preserve red…

2012-07-31cs.LOquant-ph

更多相关论文收起更多论文

The dagger lambda calculus

We present a novel lambda calculus that casts the categorical approach to the study of quantum protocols into the rich and well established tradition of type theory. Our construction extends the linear typed lambda calculus with a linear negation of "trivialised" De Morgan duality. Reduction is realised through explicit substitution, based on a symmetric notion of binding of global scope, with rules acting on the entire typing judgement instead of on a specific subterm. Proofs of subject reduction, confluence, strong normalisation and consistency are provided, and the language is shown to be a…

2014-12-30cs.LOcs.PLmath.CT

Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams

Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment that we show soundly models a LNL lambda calculus for string diagrams, introduced by Rios and Selinger (with primary application in quantum computing). Our abstract treatment of this language leads to simpler concrete models compared to those presented so far. We also extend the language with general recursion and prove soundness. Finally, we present an adequacy result for the diagram-free fragmen…

2018-04-25cs.LOcs.PLmath.CT

Lineal: A linear-algebraic Lambda-calculus

We provide a computational definition of the notions of vector space and bilinear functions. We use this result to introduce a minimal language combining higher-order computation and linear algebra. This language extends the Lambda-calculus with the possibility to make arbitrary linear combinations of terms alpha.t + beta.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in the field of …

2017-03-21cs.LOcs.PLquant-ph

A System F accounting for scalars

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 mor…

2012-02-28cs.LOcs.PLquant-ph

Higher-order semantics for quantum programming languages with classical control

This thesis studies the categorical formalisation of quantum computing, through the prism of type theory, in a three-tier process. The first stage of our investigation involves the creation of the dagger lambda calculus, a lambda calculus for dagger compact categories. Our second contribution lifts the expressive power of the dagger lambda calculus, to that of a quantum programming language, by adding classical control in the form of complementary classical structures and dualisers. Finally, our third contribution demonstrates how our lambda calculus can be applied to various well known proble…

2013-11-26cs.LOcs.PLmath.CT