rel p(s, x)
if(s = ‘a’) //this is sugar for [(s=’a’ and x=0) or x=2]
x = 0
else
x = 2
Why does it transform to [(s=’a’ and x=0) or x=2]
and not [(s=’a’ and x=0) or (s!=’a’ and x=2)]
(or whatever "not equals" is in Cosmos)?In any language I know, "else" means "do this when the guard was _not_ true", and not "nondeterministically maybe do this other thing instead, if you want". Did I simply misunderstand it? (note that I got lost at the "soft cut" part, but did I get it right that "choose ... else" is closer to what I'd expect "if .. else" to do?)
Given that accessibility to people used to imperative languages is a core goal, I'm not sure that the choice of making "else" mean "yeah whatever" is the best one. Maybe it's better to replace it by a different keyword entirely ("if.. or.." maybe). On a related note, just in case you're not familiar with it, I believe that maybe the "if.. fi" construct in Dijkstra's Guarded Command Language[0] is an easy way to get imperative-thinking people to embrace nondeterminism. It feels a lot like normal imperative "if", except there is no "else". If you want "else", you need to add another guard explicitly, with the negation of your first guard. This way, it's easy for people to grasp that the order of the guarded commands have no meaning. It also makes introducing nondeterminism very explicit.
[0] http://en.wikipedia.org/wiki/Guarded_Command_Language#Select...