Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Линейные типы и кванты (мемо, нередакченое, почти для себя)

Меня опять просили объяснить на пальцах, в чем связь гомотопически-нетривиальных линейных типов и квантовой механики. Общая идея такая: по следам фон Неймана мы хотим оперировать квантовомеханическими объектами синтетически, на уровне логики. Кроме того, это необходимо для формализации квантовых вычислений. Состояния квантовых систем объявляются "точками" описывающих квантовые системы типов. Т.к. состояние нельзя просто так склонировать, типы эти являются линейными или по меньшей мере афинными (афинные допускают молчаливое уничтожение).

Фундаментальная особенность квантовых систем состоит в том, что их состояние не может быть измерено точно: всякое измерение разрушает исходное состояние измеряемого объекта, и приводит его в другое фиксированное состояние (состояние объекта-эталона, с которым сверяют, если результат сравнения оказался положителен). Это говорит о том, что для квантовых типов T тип равенств Id_T весьма нетривиален. Кроме того, у квантовых объектов бывают ещё и калибровочные симметрии Aut_T, как минимум U(1) симметрия фазового поворота. Так что, квантовые системы должны кодироваться гомотопически-нетривиальными типам.

Базовый среди них — состояние локализованной в точке частицы полуцелого спина, Spin или кубитовая ячейка. Она обладает типом внутренних симметрий Aut_Spin = U(1). Этот тип можно комбинировать с самим собой разными способами: можно увеличивать количество локализованных электронов, можно допускать разную локализацию. Состояние регистра из трёх кубитов (т.е. три ионные ловушки с тремя локализованными частицами) — Spin ⊗ Spin ⊗ Spin. При этом имеет место когезия внутренних симметрий, то есть не так что у каждого их трех элементов остаётся степень свободы по своей внутренней симметрии U(1), а они "слипаются": Aut_(Spin ⊗ Spin ⊗ Spin) всё ещё U(1).

С другой стороны, мы можем разрешить нашей частице быть в трёх разных состояниях по ортогональному параметру (например, местоположению). Например есть три ионных ловушки и одна частица, которая может быть одной из них (или их квантовой суперпозиции): Spin ⅋ Spin ⅋ Spin. Тут тоже имеет место когезия внутренних симметрий. Каким-то образом наличие внутренней симметрии U(1) у каждого из отдельных элементов и такой же симметрии у конечного типа приводит к тому, что в этом типе живут нормированные линейные комбинации исходных типов.

Зависимые (от нелинейных) суммы и произведения нужны для получения бесконечных обобщений этих типов. Например, если наша частица живёт уже не в конечном числе точек, а во всём объеме, то тип её линейных функций должен описываться (наивное описание) как Real3 ⅋=> Spin. Интересным образом, делокализация по месту приводит к тому, что на втором месте конструктора ⅋=> может стоять тривиальный тип QUnit (U(1)/U(1)), так волновая функция спин0-частицы Real3 ⅋=> QUnit. Тип состояний простейшего гармонического осциллятора Nat ⅋=> QUnit. С другой стороны, если у осциллятора с повышением энергитического уровня повышается спин, то (n: Nat) ⅋=> Spin[n], реальный зависимый тип.

Зависимые произведения возникают при необходимости ввести квантовое поле. Рассмотрим, например, поле фотонов в одномерном металлическом ящике. Это поле состоит совершенно независимых между собой из стоячих волн для каждого числа (n: Nat) узлов. Каждая стоячая волна сама по себе представляет из себя квантовых гармонический осциллятор Oszi := Nat ⅋=> QUnit. Состояние всего поле целиком будет описываться типом (n: Nat) ⊗=> Oszi.

Тип поля частиц можно также породить из типа волновой функции отдельной частицы порождая пространство фока, это соответствует экспоненциальной модальности. Тут тоже нетривиальную роль начинает играть внутренняя степень свободы: U(1)-типы можно комбинировать в пространство фока либо как бозоны, либо как фермионы.
Dirac-Field := !(Real3 ⅋=> Spin)

Но самое интересное, что на этом пути должны как-то получаться поля с калибровочными симметриями. Тогда должно выходить что-то вроде Aut_(Charged-Field) = Electromagnetic-Field. Гомотопическая нетривиальность должна тут давать возможность писать нетипичные для линейных типов выражения, соответствующие вершинам фейнмановских диаграм порядка три, то есть тип Aut_(T) должен быть подтипом T ⅋ T. Вершины большего порядка, как известно, получаются в случаях когда Aut_(T) является составной частью T, как в случае слабого и сильного взаимодействия. Для определения таких типов потребуется некоторое обобщение зависимого произведения типов до скрещенного.

На мой взгляд, самое главное сейчас понять что такое Id[T] и Aut[T] для линейных типов. Основополагающее свойство квантовых состояний, что их нельзя точно сличить, не разрушив одно из них, должно проявляться уже на уровне типа Id[T], который в случае КМ направлен: при сравнении состояния не эквивалентны, одно их них берётся за эталон (a), а другое (b) с ним сверяется, "факт равенства" e: (a = b) означает операционно, что мы съели a и b и получили две копии a. Возможно плодотворнее для линейных типов рассматривать apparntess type, а не identity type.
Subscribe

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments