[FOM] Relative Completeness

[José Manuel Rodríguez Caballero]

Dear FOM members,
  Recently, I was in a lecture about the paper [1] and some experts were
skeptical of the proof of relative completeness of a proof system known as
aQHL (applied Quantum Hoare Logic). More precisely, according to [1], aQHL
satisfies a property known as relative completeness, which is defined as
follows:  if we assume an oracle to decide the validity of assertions, then
we can decide the validity of partial correctness specifications, i.e., the
given formal system is no more incomplete than our language of assertions.

In [1], the relative completeness of aQHL (Theorem 3.4) is claimed (without
proof) to be a consequence of the following three results (for precise
statements, see [1]):

- Theorem 2.1. The proof systems qPD (Figure 2 in [1]) and qTD (Figure 3 in
[1]) are relatively complete and sound (for an explicit description, see
[1]).

- Theorem 3.2.  Correctness in aQHL can be lifted to QHL (Quantum Hoare
Logic).

- Theorem 3.3.  QHL can be partially reduced to aQHL.

I would like to ask the FOM members for their opinions concerning whether
or not the proof of Theorem 3.4 is valid (even if the theorem is true, the
proof may be fallacious).

Also, I would like to notice that one of the authors of [1], Mingsheng
Ying, was also part of a formalization of QHL in Isabelle/HOL [2].
Nevertheless, Theorem 3.4 has not been formalized yet in this library of
Isabelle/HOL.

Sincerely yours,
José M.

References:
[1] Zhou, Li, Nengkun Yu, and Mingsheng Ying. "An applied quantum Hoare
logic." *Proceedings of the 40th ACM SIGPLAN Conference on Programming
Language Design and Implementation*. ACM, 2019.
https://urldefense.proofpoint.com/v2/url?u=https-3A__dl.acm.org_citation.cfm-3Fid-3D3314584&d=DwIFaQ&c=slrrB7dE8n7gBJbeO0g-IQ&r=xXZM6ZrkjVxXknjzIxhAvQ&m=RW_rEx_qG54bIxMypwFYonS1yWneZ3A3oyBBjJSBhzs&s=wU52VHJ225GwfETh27JgdoJlv3SQmYqMl5fscuZx3xE&e= 

[2] Library in Isabelle/HOL: @article{QHLProver-AFP,
  author  = {Junyi Liu and Bohua Zhan and Shuling Wang and Shenggang Ying
and Tao Liu and Yangjia Li and Mingsheng Ying and Naijun Zhan},
  title   = {Quantum Hoare Logic},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2019,
  note    = {\url{https://urldefense.proofpoint.com/v2/url?u=http-3A__isa-2Dafp.org_entries_QHLProver.html&d=DwIFaQ&c=slrrB7dE8n7gBJbeO0g-IQ&r=xXZM6ZrkjVxXknjzIxhAvQ&m=RW_rEx_qG54bIxMypwFYonS1yWneZ3A3oyBBjJSBhzs&s=KNvJckWzLulP4htsaDDKb7HXcEgq_xrOHLE5Cg9kPP0&e= },
            Formal proof development},
  ISSN    = {2150-914x},
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190921/a03788bc/attachment.html>