Unless
p unless q ? ??S: S in F :: {p ? ?q} S {p ? q}?
ak p je true a q nie je true v nasledujúcom kroku, p ostáva true alebo q sa stane true
ak v nejakom mieste výpoctu F platí p, tak
- q nebude nikdy platit a p bude stále platit
- q bude urcite raz (eventually) platit a p platí aspon pokial q zacne platit
(p ? ?q)[Rj] ? (p ? q)[Rj+!]
Z “p unless q” mozno odvodit: p[Rj] ?
? ?k: k ? j :: (p ? ?q)[Rk] ? ? /* p ??q platí vzdy */
[ ? ?m: m ? j :: q[Rm] ? ? /* q nakoniec platí */
? ?k: j ? k < m :: (p ? ?q)[Rk] ? ] /* dovtedy platí p ??q */
Príklady
1. x neklesne
- x = k unless x > k
- x ? k unless x > k
- x ? k unless false
2. Správa je v kanáli az kým nie je prijatá a potom je odstránená z kanálu
- inch ? ?rcvd unless ?inch ? rcvd