- Квантовая логика Биркгофа-фон Неймана как язык утверждений для квантовых программ (arXiv)
Автор:Миншэн Ин
Аннотация: Логика первого порядка с квантовыми переменными необходима в качестве языка утверждений для определения и рассуждений о различных свойствах (например, правильности) квантовых программ. Удивительно, но такая логика отсутствует в литературе, а существующая квантовая логика Биркгофа-фон Неймана первого порядка имеет дело только с классическими переменными и квантификациями над ними. В этой статье мы заполняем этот пробел, вводя расширение первого порядка квантовой логики Биркгофа-фон Неймана с универсальными и экзистенциальными кванторами над квантовыми переменными. Представлены примеры, показывающие, что наша логика особенно подходит для определения некоторых важных свойств, изучаемых в квантовых вычислениях и квантовой информации. Далее мы включаем эту логику в квантовую логику Хоара в качестве логики утверждений, чтобы она могла играть роль, аналогичную роли логики первого порядка для классической логики Хоара и BI-логики для логики разделения. В частности, мы показываем, как его можно использовать для определения и вывода квантовых обобщений некоторых правил адаптации, которые применялись для значительного упрощения проверки классических программ. Ожидается, что логика утверждений, определенная в этой статье — квантовая логика первого порядка с квантовыми переменными — может быть объединена с различной логикой квантовых программ, чтобы служить прочной логической основой, на которой могут быть построены инструменты проверки с использованием помощников по доказательству, таких как Coq и Изабель/ХОЛ
2. MCBeth: язык квантового программирования на основе измерений (arXiv)
Автор: Эйдан Эванс, Сеун Омонийе, Роберт Суле, Роберт Рэнд
Вывод:языки квантового программирования на основе Gate широко распространены, но языки, основанные на измерениях, в настоящее время существуют только на бумаге. В этой работе представлен MCBeth, квантовый язык программирования, который позволяет программистам напрямую представлять, программировать и моделировать вычисления на основе измерений и состояний кластера, опираясь на исчисление измерений. В то время как программы MCBeth предназначены для выполнения непосредственно на оборудовании, чтобы воспользоваться преимуществами современных машин, мы также предоставляем компилятор для инструкций на основе вентилей. Мы утверждаем, что у квантовых вычислений на основе измерений есть явные преимущества по сравнению с вентильными, когда речь идет о реализации общих квантовых алгоритмов и распределенных квантовых вычислений.△ Меньше
3. Программная инженерия для квантового программирования: как далеко мы продвинулись? (arXiv)
Автор:Мануэль Де Стефано, Фабиано Пекорелли, Дарио Ди Нуччи, Фабио Паломба, Андреа Де Люсия
Аннотация:Квантовые вычисления больше не представляют только научный интерес, они быстро становятся промышленно доступными технологиями, которые потенциально могут преодолеть ограничения классических вычислений. За последние годы все крупные компании предоставили фреймворки и языки программирования, которые позволяют разработчикам создавать свои квантовые приложения. Этот сдвиг привел к определению новой дисциплины, называемой квантовой инженерией программного обеспечения, которая требуется для определения новых методов разработки крупномасштабных квантовых приложений. В то время как исследовательское сообщество успешно принимает этот вызов, мы замечаем отсутствие систематических исследований состояния практики квантового программирования. Понимание проблем, с которыми сталкиваются квантовые разработчики, жизненно важно для точного определения целей квантовой разработки программного обеспечения. Следовательно, в этой статье мы сначала анализируем все репозитории GitHub, в которых используются наиболее часто используемые платформы квантового программирования, представленные в настоящее время на рынке, а затем проводим сеансы анализа кода, чтобы составить таксономию целей, для которых используются квантовые технологии. Во-вторых, мы проводим исследование-опрос, в котором участвуют участники рассматриваемых репозиториев, целью которого является выяснить мнение разработчиков о текущем внедрении и проблемах квантового программирования. С одной стороны, результаты подчеркивают, что нынешнее внедрение квантового программирования все еще ограничено. С другой стороны, существует множество проблем, которые сообществу разработчиков программного обеспечения следует тщательно рассмотреть: они относятся не только к техническим проблемам, но и к социально-техническим вопросам.
4. Qimaera: Типобезопасное (вариационное) квантовое программирование в Idris(arXiv)
Автор : Лилиан-Джой Денди, Эммануэль Жандель, Владимир Замджиев
Аннотация:Вариационные квантовые алгоритмы — это гибридные классические и квантовые алгоритмы, в которых классические и квантовые вычисления работают в тандеме для решения вычислительных задач. Эти алгоритмы создают интересные проблемы для разработки подходящих языков программирования. В этой статье мы представляем Qimaera, набор библиотек для языка программирования Idris 2, которые позволяют программисту реализовывать (вариационные) квантовые алгоритмы, где вся мощь элегантного языка Idris работает синхронно с представленными нами примитивами квантового программирования. Двумя ключевыми компонентами Idris, которые делают это возможным, являются (1) зависимые типы, которые позволяют нам реализовывать унитарные (то есть обратимые и контролируемые) квантовые операции; и (2) линейность, которая позволяет нам осуществлять детальный контроль над выполнением квантовых операций, что обеспечивает соблюдение законов квантовой механики. Мы демонстрируем, что Qimaera подходит для вариационного квантового программирования, предоставляя реализации двух наиболее известных вариационных квантовых алгоритмов — QAOA и VQE. Насколько нам известно, это первая реализация этих алгоритмов, реализованная в фреймворке с безопасностью типов.
5.isQ: На пути к практическому программному стеку для квантового программирования (arXiv)
Автор:Цзинчжэ Го, Хуачжэ Лу, Рилин Ли, Ван Фан, Цзюньи Лю, Пейсюнь Лун, Шенган Ин, Миншэн Ин
Аннотация: мы представляем isQ, новый программный стек для квантового программирования на императивном языке программирования, также называемом isQ. Цель isQ — сделать так, чтобы программистам было максимально удобно писать квантовые программы. В частности: 1) Язык isQ и его компилятор содержат множество функций, в том числе некоторые, плохо поддерживаемые (большинством) других платформ квантового программирования, например. классический поток управления, такой как рекурсия; декомпозиция самоопределяющихся унитарных вентилей; и программирование оракула и его схемная реализация. 2) Чтобы сделать ее гибкой, программа isQ может быть скомпилирована в несколько видов промежуточного представления, включая OpenQASM 3.0, QIR и QCIS (специально разработанные для сверхпроводящего квантового оборудования в USTC). 3) Помимо взаимодействия isQ с настоящим сверхпроводящим оборудованием, также разработан симулятор QIR для демонстрации и тестирования программ isQ.
