Foundations of Quantum Programming Foundations of Quantum Programming Mingsheng Ying UniversityofTechnologySydneyandTsinghuaUniversity AMSTERDAM (cid:129) BOSTON (cid:129) HEIDELBERG (cid:129) LONDON NEW YORK (cid:129) OXFORD (cid:129) PARIS (cid:129) SAN DIEGO SAN FRANCISCO (cid:129) SINGAPORE (cid:129) SYDNEY (cid:129) TOKYO Morgan Kaufmann is an imprint of Elsevier MorganKaufmannisanimprintofElsevier 50HampshireStreet,5thFloor,Cambridge,MA02139,USA Copyright©2016ElsevierInc.Allrightsreserved. Nopartofthispublicationmaybereproducedortransmittedinanyformorbyanymeans,electronicor mechanical,includingphotocopying,recording,oranyinformationstorageandretrievalsystem,without permissioninwritingfromthepublisher.Detailsonhowtoseekpermission,furtherinformationabout thePublisher’spermissionspoliciesandourarrangementswithorganizationssuchastheCopyright ClearanceCenterandtheCopyrightLicensingAgency,canbefoundatourwebsite: www.elsevier.com/permissions. ThisbookandtheindividualcontributionscontainedinitareprotectedundercopyrightbythePublisher (otherthanasmaybenotedherein). Notices Knowledgeandbestpracticeinthisfieldareconstantlychanging.Asnewresearchandexperience broadenourunderstanding,changesinresearchmethods,professionalpractices,ormedicaltreatment maybecomenecessary. Practitionersandresearchersmustalwaysrelyontheirownexperienceandknowledgeinevaluatingand usinganyinformation,methods,compounds,orexperimentsdescribedherein.Inusingsuchinformation ormethodstheyshouldbemindfuloftheirownsafetyandthesafetyofothers,includingpartiesfor whomtheyhaveaprofessionalresponsibility. Tothefullestextentofthelaw,neitherthePublishernortheauthors,contributors,oreditors,assumeany liabilityforanyinjuryand/ordamagetopersonsorpropertyasamatterofproductsliability,negligence orotherwise,orfromanyuseoroperationofanymethods,products,instructions,orideascontainedin thematerialherein. BritishLibraryCataloguinginPublicationData AcataloguerecordforthisbookisavailablefromtheBritishLibrary LibraryofCongressCataloging-in-PublicationData AcatalogrecordforthisbookisavailablefromtheLibraryofCongress ISBN:978-0-12-802306-8 ForinformationonallMorganKaufmannpublications, visitourwebsiteathttps://www.elsevier.com/ Publisher:ToddGreen AcquisitionEditor:ToddGreen EditorialProjectManager:LindsayLawrence ProductionProjectManager:PunithavathyGovindaradjane Designer:GregHarris TypesetbySPiGlobal,India Preface “Perhapsthequantumcomputerwillchangeoureverydaylivesinthiscentury inthesameradicalwayastheclassicalcomputerdidinthelastcentury.” —excerptfrompressrelease,NobelPrizeinPhysics2012. Quantum computers promise dramatic advantages over current computers. Governments and industries around the globe are now investing large amounts of money with the expectation of building practical quantum computers. Recent rapid physical experimental progress has made people widely expect that large- scalableandfunctionalquantumcomputerhardwarewillbebuiltwithin10–20years. However, to realize the super-power of quantum computing, quantum hardware is obviouslynotenough,andquantumsoftwaremustalsoplayakeyrole.Thesoftware development techniques used today cannot be applied to quantum computers. Essentialdifferencesbetweenthenatureoftheclassicalworldandthatofthequan- tumworldmeanthatnewtechnologiesarerequiredtoprogramquantumcomputers. Research on quantum programming started as early as 1996, and rich results have been presented at various conferences or reported in various journals in the last20years.Ontheotherhand,quantumprogrammingisstillaprematuresubject, with its knowledge base being highly fragmentary and disconnected. This book is intendedto providea systematic and detailed expositionof the subjectof quantum programming. Sincequantumprogrammingisstillanareaunderdevelopment,thebookdoesnot focus on specific quantum programming languages or techniques, which I believe will undergo major changes in the future. Instead, the emphasis is placed on the foundational concepts, methods and mathematical tools that can be widely used forvariouslanguagesandtechniques.Startingfroma basic knowledgeof quantum mechanicsandquantumcomputation,thebookcarefullyintroducesvariousquantum programconstructsandachainofquantumprogrammingmodelsthatcaneffectively exploit the unique power of quantum computers. Furthermore, semantics, logics, and verification and analysis techniques of quantum programs are systematically discussed. Withthehugeinvestmentandrapidprogressinquantumcomputingtechnology, Ibelievethatwithin10yearsmoreandmoreresearcherswillentertheexcitingfield of quantumprogramming.Theywill need a referencebookas the starting pointof theirresearch.Also,a courseonquantumprogrammingwillbe taughtatmoreand moreuniversities.Teachersandstudentswillneedatextbook.So,Idecidedtowrite thisbookwiththetwo-foldaim: (i) providingabasisforfurtherresearchinthearea;and (ii) servingasatextbookforagraduateoradvancedundergraduatelevelcourse. ix x Preface Quantum programming is a highly interdisciplinary subject. A newcomer and, in particular, a student is usually frustrated with the requisite knowledge from many different subjects. I have tried to keep the book as self-contained as possible, with details being explicitly presented so that it is accessible to the programming languagescommunity. Writing this book gave me an opportunity to systemize my views on quantum programming. On the other hand, topics included in this book were selected and thematerialswereorganizedaccordingtomyownunderstandingofthissubject,and severalimportanttopicswereomittedinthemainbodyofthebookduetomylimited knowledgeaboutthem. As a remedy,some briefdiscussionsaboutthese topicsare providedintheprospectschapterattheendofthebook. Acknowledgments This book has been developed through my research in the last 15 years at the QuantumComputationandQuantumInformationGroupoftheStateKeyLaboratory of Intelligent Technology and Systems, Tsinghua University and the Quantum Computation Laboratory of the Centre for Quantum Computation and Intelligent Systems,UniversityofTechnologySydney.Ihaveenjoyedverymuchcollaborations and discussions with my colleagues and students there. I would like to thank allofthem. IamparticularlyindebtedtoIchiroHasuo(UniversityofTokyo)andYuanFeng (University of Technology Sydney) who patiently read the draft of this book and kindly provided invaluable comments and suggestions. I am very grateful to the anonymous reviewers for the book proposal; their suggestions were very helpful for the structure of the book. I also would like to sincerely thank Steve Elliot, Punithavathy Govindaradjane, Amy Invernizzi, and Lindsay Lawrence, my editors andprojectmanagersatMorganKaufmann. Special thanks go to the Centre for Quantum Computation and Intelligent Sys- tems,FacultyofEngineeringandInformationTechnology,UniversityofTechnology Sydneyforgivingmethefreedomtopursuemythoughts. My research on quantum programming has been supported by the Australian Research Council, the National Natural Science Foundation of China, and the Overseas Team Program of the Academy of Mathematics and Systems Science, ChineseAcademyofSciences.Allofthemaregratefullyacknowledged. xi CHAPTER 1 Introduction “The challenge [of quantum software engineering] is to rework and extend the wholeofclassicalsoftwareengineeringintothequantumdomainsothatprogram- merscanmanipulatequantumprogramswiththesameeaseandconfidencethat theymanipulatetoday’sclassicalprograms.” excerptfromthe2004reportGrandChallenges inComputingResearch[120]. Quantumprogrammingisthestudyofhowtoprogramfuturequantumcomput- ers.Thissubjectmainlyaddressesthefollowingtwoproblems: • Howcanprogrammingmethodologiesandtechnologiesdevelopedforcurrent computersbeextendedforquantumcomputers? (cid:129) Whatkindsofnewprogrammingmethodologiesandtechnologiescan effectivelyexploittheuniquepowerofquantumcomputing? Many technologiesthat have been very successful in traditional programmingwill be broken when used to program a quantum computer, due to the weird nature of quantumsystems(e.g.,nocloningofquantumdata,entanglementbetweenquantum processes, and non-commutativity of observables which are all assertions about program variables). Even more importantand difficult is to discover programming paradigms, models and abstractions that can properly exploit the unique power of quantumcomputing–quantumparallelism–butcannotbesourcedfromknowledge oftraditionalprogramming. 1.1 BRIEF HISTORY OF QUANTUM PROGRAMMING RESEARCH The earliest proposalfor quantumprogrammingwas made by Knillin 1996[139]. HeintroducedtheQuantumRandomAccessMachine(QRAM)modelandproposed a set of conventionsfor writing quantum pseudo-code. In the 20 years since then, researchonquantumprogramminghasbeencontinuouslyconducted,mainlyinthe followingdirections. FoundationsofQuantumProgramming.http://dx.doi.org/10.1016/B978-0-12-802306-8.00001-X 3 Copyright©2016ElsevierInc.Allrightsreserved. 4 CHAPTER 1 Introduction 1.1.1 DESIGN OF QUANTUM PROGRAMMING LANGUAGES Early research on quantum programming focused on the design of quantum pro- gramming languages. Several high-level quantum programming languages have been defined in the later 1990s and early 2000s; for example, the first quantum programminglanguage,QCL,wasdesignedbyÖmer[177],whoalsoimplemented a simulator for this language. A quantum programming language in the style of Dijkstra’s guarded-command language, qGCL, was proposed by Sanders and Zuliani[191,241].AquantumextensionofC++wasproposedbyBettellietal.[39], and implemented in the form of a C++ library. The first quantum language of the functional programming paradigm, QPL, was defined by Selinger [194] based on theideaofclassicalcontrolandquantumdata.Aquantumfunctionalprogramming language QML with quantum control flows was introduced by Altenkirch and Grattage [14]. Tafliovich and Hehner [208,209] defined a quantum extension of a predicativeprogramminglanguagethatsupportstheprogramdevelopmenttechnique inwhicheachprogrammingstepisprovencorrectwhenitismade. Recently, two general-purpose, scalable quantum programming languages, Quipper and Scaffold, with compilers, were developed by Green et al. [106] and Abhariet al. [3], respectively.A domain-specificquantum programminglanguage, QuaFL, was developed by Lapets et al. [150]. A quantum software architecture LIQUi|>, together with a quantum programming language embedded in F#, was designedandimplementedbyWeckerandSvore[215]. 1.1.2 SEMANTICS OF QUANTUM PROGRAMMINGLANGUAGES Formalsemanticsofaprogramminglanguagegivearigorousmathematicaldescrip- tion of the meaning of this language, to enable a precise and deep understanding of the essence of the language beneath its syntax. The operational or denotational semantics of some quantum programming languages were already provided when theyweredefined;forexample,qGCL,QPLandQML. Two approachesto predicate transformer semantics of quantum programshave been proposed. The first was adopted by Sanders and Zuliani [191] in designing qGCL, where quantumcomputationis reducedto probabilistic computationby the observation (measurement) procedure, and thus predicate transformer semantics developed for probabilistic programs can be applied to quantum programs. The secondwasintroducedbyD’HondtandPanangaden[70],whereaquantumpredicate is defined to be a physical observable represented by a Hermitian operator with eigenvalueswithin the unit interval. Quantum predicate transformersemantics was further developed in [225] with a special class of quantum predicates, namely projection operators. Focusing on projective predicates allows the use of rich mathematical methods developed in Birkhoff-von Neumann quantum logic [42] to establishvarioushealthinessconditionsofquantumprograms. Semantic techniques for quantum computation have also been investigated in some abstract, language-independent ways. Abramsky and Coeck [5] proposed a 1.1 Brief history ofquantumprogramming research 5 category-theoreticformulationofthebasicpostulatesofquantummechanics,which canbeusedtogiveanelegantdescriptionofquantumprogramsandcommunication protocolssuchasteleportation. Recentprogressincludes:HasuoandHoshino[115] founda semanticmodelof afunctionalquantumprogramminglanguagewithrecursionviaGirard’sGeometry of Interaction [101], categorically formulated by Abramsky, Haghverdi and Scott [7]. Pagani, Selinger and Valiron [178] discovered a denotational semantics for a functional quantum programming language with recursion and an infinite data type using constructions from quantitative semantics of linear logic. Jacobs [123] proposedacategoricalaxiomatizationofblockconstructsinquantumprogramming. Staton [206] presented an algebraic semantic framework for equational reasoning aboutquantumprograms. 1.1.3 VERIFICATION AND ANALYSIS OF QUANTUM PROGRAMS Human intuition is much better adapted to the classical world than the quantum world.Thisfactimpliesthatprogrammerswillcommitmanymorefaultsindesigning programs for quantum computers than in programmingclassical computers. Thus, it is crucial to develop verification techniques for quantum programs. Baltag and Smets [30] presented a dynamic logic formalism of information flows in quantum systems. Brunet and Jorrand [50] introduced a way of applying Birkhoff-von Neumannquantumlogicinreasoningaboutquantumprograms.Chadha,Mateusand Sernadas[52]proposedaproofsystemoftheFloyd-Hoarestyleforreasoningabout imperativequantumprogramsin whichonly boundediterationsare allowed.Some useful proof rules for reasoning about quantum programs were proposed by Feng et al. [82] for purely quantum programs. A Floyd-Hoare logic for both partial and total correctness of quantumprogramswith (relative) completenesswas developed in[221]. Program analysis techniques are very useful in the implementation and opti- mization of programs. Termination analysis of quantum programs was initiated in [227], where a measurement-based quantum loop with a unitary transformation as theloopbodywas considered.Terminationofa moregeneralquantumloopwith a quantumoperationastheloopbodywasstudiedin[234]usingthesemanticmodel of quantum Markov chains. It was also shown in [234] that the Sharir-Pnueli-Hart method for proving properties of probabilistic programs [202] can be elegantly generalizedtoquantumprogramsbyexploitingtheSchrödinger-Heisenbergduality between quantum states and observables. This line of research has been continued in [152,153,235,236,238] where termination of nondeterministic and concurrent quantum programs was investigated based on reachability analysis of quantum Markov decision processes. Another line of research in quantum program analysis was initiatedby Jorrandand Perdrix[129] who showedhowabstractinterpretation techniquescanbeusedinquantumprograms. 6 CHAPTER 1 Introduction 1.2 APPROACHES TO QUANTUM PROGRAMMING Naturally, research on quantum programming started from extending traditional programming models, methodologies and technologies into the quantum realm. As stated in Section 1.1, both imperative and functional programming have been generalizedfor quantumcomputing,and varioussemantic models, verificationand analysis techniques for classical programs have also been adapted to quantum programming. The ultimate goal of quantum programming is to fully exploit the power of quantum computers. It has been well understood that the advantage of quantum computersovercurrentcomputerscomesfromquantumparallelism–superposition of quantum states – and its derivatives such as entanglement. So, a key issue in quantum programming is how to incorporate quantum parallelism into traditional programming models. In my opinion, this issue can be properly addressed in the followingtwoparadigmsofsuperposition. 1.2.1 SUPERPOSITION-OF-DATA – QUANTUM PROGRAMS WITH CLASSICAL CONTROL The main idea of the superposition-of-data paradigm is to introduce new pro- gram constructs needed to manipulate quantum data, e.g., unitary transformations, quantum measurements. However, the control flows of quantum programs in such a paradigm are similar to those of classical programs. For example, in classical programming,abasicprogramconstructthatcanbeusedtodefinethecontrolflow ofaprogramistheconditional(if...then...else...fi)statement,ormoregenerally thecasestatement: if((cid:2)i·Gi →Pi)fi (1.1) where for each i, the subprogramP is guardedby the Boolean expressionG, and i i P willbeexecutedonlywhenG istrue.Anaturalquantumextensionofstatement i i (1.1)isthemeasurement-basedcasestatement: if((cid:2)i·M[q]=mi →Pi)fi (1.2) whereqisa quantumvariableandM a measurementperformedonqwithpossible outcomesm ,...,m ,andforeachi,P isa(quantum)subprogram.Thisstatement 1 n i selects a commandaccordingto the outcomeof measurementM: if the outcomeis m, then the corresponding command P will be executed. It can be appropriately i i called classical case statement in quantum programming because the selection of commands in it is based on classical information – the outcomes of a quantum measurement. Then other language mechanisms used to specify the control flow of quantum programs, e.g., loop and recursion, can be defined based on this case statement. The programming paradigm defined here is called the superposition-of-data paradigm because the data input to and computed by these programs are quantum