Аксиоматизация логики квантовых вычислений

Аннотация

Одной из логических рекомендаций, касающихся квантовых вычислений, является идея использовать квантовый теоретический формализм для представления параллельных рассуждений. С этой целью квантовое вычисление представляется с помощью соответствующих унитарных операторов, предполагающих аргументы и значения в конкретных множествах систем кубитов. Выделив некоторые важные унитарные операторы, играющих особую роль в квантовых вычислениях (логические вентили или quregisters), мы получаем возможность построить язык квантовой вычислительной логики (QCL) (ср. [Каттанео и др. 2003; Каттанео и др., 2004; Далла Кьяра и др., 2004]). Основным понятием семантики этого языка является понятие квантовой вычислительной реализации, когда значением, ассоциированным с любым предложением, является логический вентиль. В отличие от семантики стандартной квантовой логики, QCL-конъюнкция и QCL-дизъюнкция не соответствуют решеточным операциям, так как они, как правило, не являются идемпотентными. Более того, в QCL нарушается принцип слабой дистрибутивности, и нарушаются как принцип исключенного третьего, так и принцип непротиворечия. Наконец, аксиоматизируемость QCL все еще остается открытой проблемой. В статье предлагается аксиоматизация QCL, трактующая ее как разновидность так называемой бинарной логики Гольдблатта. Доказаны некоторые металогические теоремы (паранепротиворечивость и полнота).