Universal Quantification
Posted: 10 Sep 2015 11:45
Hello Thomas,
the body of a foreach-term must be procedure. If it would need to be only determ, then the foreach-term could be used for expressing universal quantification. For that the semantics of the foreach-term could be extended, to let it fail, as soon as one of the executions of the body fails.
I suggest, to allow the body being determ or else to invent some additional syntax for determ bodies, maybe one of:
Of course universal quantification can also be coded in current VIP, however it's not that elegant as it would be with the above change. Currently a way to code it is:
Regards
Martin
the body of a foreach-term must be procedure. If it would need to be only determ, then the foreach-term could be used for expressing universal quantification. For that the semantics of the foreach-term could be extended, to let it fail, as soon as one of the executions of the body fails.
I suggest, to allow the body being determ or else to invent some additional syntax for determ bodies, maybe one of:
Code: Select all
forall Gen do
DetermBody
end forall
Code: Select all
foreach Gen trydo
DetermBody
end foreach
Code: Select all
not
((
Gen,
not(DetermBody)
))
Martin