^@ semantics

[SweeWarman]

Could someone kindly let me know where I can find the semantics for the "^@" symbol used in the KeYmaeraX language?

[nrfulton]

The ^@ symbol is KeYmaera X's concrete syntax for the "dual" operator in hybrid grams. I.e., "^@" in KeYmaera X is the "^d" in Definition 2 of https://lfcps.org/pub/dGL-usubst.pdf.

The semantics are defined in Section 2.2 of that paper and, in particular, Definition 5.

See also:

• Pages 421-508 of André's textbook: https://www.springer.com/gp/book/9783319635873
• lectures 16-18 at https://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx?#folderID=%22099e76b8-5dfa-4029-bd7b-94c24b860943%22&folderSets=15

The textbook and lectures might be the best starting point if you're not familiar with hybrid grams. https://lfcps.org/pub/dGI.pdf is another reference.

It's admittedly not an amazing choice of syntax, but much less confusing that making "the character sequence ^d appearing as a suffix on a program" a reserved keyword.

I think that differential game logic is still an experimental feature (@smitsch / @aplatzer can correct me if this has changed).

[aplatzer]

Differential game logic and hybrid games are stable just less-well tested than hybrid systems. Let us know if you run into any issues.