2007 | OriginalPaper | Chapter
Taming Non-compositionality Using New Binders
Author : Frédéric Prost
Published in: Unconventional Computation
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We propose an extension of the traditional
λ
-calculus in which terms are used to control an outside computing device (quantum computer, DNA computer...). We introduce two new binders:
ν
and
ρ
. In
νx
.
M
,
x
denotes an abstract resource of the outside computing device, whereas in
ρx
.
M
,
x
denotes a concrete resource. These two binders have different properties (in terms of
α
-conversion, scope extrusion, convertibility) than the ones of standard
λ
-binder. We illustrate the potential benefits of our approach with a study of a quantum computing language in which these new binders prove meaningful. We introduce a typing system for this quantum computing framework in which linearity is only required for concrete quantum bits offering a greater expressiveness than previous propositions.