Recursive countable

[banishedKnight1999]

Hi. I'm a independent researcher and i'm very interested in your work. Thank you for your contributions! However, I found some issues during my research and have made the following modifications:
Why I'm sending this
I wanted to model recursive quantum procedures (like RUS) and reason about them in SQIR, but the core language and logic don’t really cover recursion or countable assertions.(Consider that a while loop can lead to an infinite conjunction.) So I added a small RC layer to fill that gap.
What’s in this patch
CCall for recursive procedures
IConj for countable deterministic assertions
fixed‑point semantics for recursion
a WP calculus + soundness statement (with explicit assumptions)
New files
SQIR/RC_Syntax.v — extended commands + countable assertions
SQIR/RC_Semantics.v — denotational semantics with fixed points
SQIR/RC_Logic.v — WP + Hoare rules + soundness
examples/examples/RUSExample.v — RUS gate example
examples/examples/QFTExample.v — recursive QFT example
examples/examples/QuantumRandomWalkExample.v — QRW example with CWhile
Updated files
SQIR/UnitarySem.v, SQIR/UnitaryOps.v — import style tweak for -Q paths
Notes
This is additive and shouldn’t change existing SQIR behavior.
Soundness relies on a few clearly stated semantic assumptions in RC_Logic.v.
I hope this will be helpful to you.

[rnrand]

Interesting! This sounds very much like Deng et al's iSQIR work, described here:

https://dl.acm.org/doi/10.1145/3632901

Have you looked at that? (I can't find a Rocq implementation online, but that doesn't mean it doesn't exist.)

[banishedKnight1999]

Interesting! This sounds very much like Deng et al's iSQIR work, described here:

https://dl.acm.org/doi/10.1145/3632901

Have you looked at that? (I can't find a Rocq implementation online, but that doesn't mean it doesn't exist.)

Thank you for your recommendation. This paper seems to have done a lot of excellent work. I'm more focused on the mathematical and logical parts. It still makes for an interesting brunch.