Paul, a quantifier-toolbox can be coded in the way:
Code: Select all
class quantification
open core
predicates
forAll : (
function_nd{Type} GetItem,
predicate_dt{Type} CheckItem)
determ (i, i).
% @short Succeeds iff all items, which #GetItem enumerates nondeterministically, satisfy #CheckItem.
% @end
predicates
exists : (
function_nd{Type} GetItem,
predicate_dt{Type} CheckItem)
-> Type Item
determ (i, i).
% @short Succeeds iff at least one of the items, which #GetItem enumerates nondeterministically, satisfies #CheckItem.
% @end
predicates
existsExactlyOne : (
function_nd{Type} GetItem,
predicate_dt{Type} CheckItem)
-> Type Item
determ (i, i).
% @short Succeeds iff exactly one of the items, which #GetItem enumerates nondeterministically, satisfies #CheckItem.
% @end
end class quantification
%---
implement quantification
open core
clauses
forAll(GetItem, CheckItem):-
not
((
Item = GetItem(),
not(CheckItem(Item))
)).
clauses
exists(GetItem, CheckItem) = Item:-
Item = GetItem(),
CheckItem(Item),
!.
clauses
existsExactlyOne(GetItem, CheckItem) = OptResultM:tryGet() :-
OptResultM = varM_optional::new(),
foreach
Item = GetItem(),
CheckItem(Item),
if OptResultM:value <> none then
!,
OptResultM:unset(),
fail
end if do
OptResultM:set(Item)
end foreach.
end implement quantification
But of course a toolbox module cannot provide the ease of use, which comes with a 1st level construction of the language.
Thomas, please have a look at this
mathematical scriptum and search it for the word "holds". You will find the phrase "for all .. holds .." being used many times.
You may be right, that the syntax version with a pause or a comma instead of the word "holds" is overall used more often in mathematics. But I suppose, a space or comma in that place would not fit to VIP's syntax anyway.
The word "holds" has the advantage, that it takes the imperative sense away from the "for all". I don't feel, that "for all .. holds .." would be too misleading. But it's of course a matter of taste.
More verbose instead of only "holds" is "it holds that". But in my opinion that would be annoying lengthy in VIP. Shorter than "holds" would be ":", however I am not sure, whether the existing usage of ":" would permit to use it there too.
If a satisfactory syntax cannot be found instantly, please keep universal quantification in mind and maybe a decision for some syntax will evolve by the time.
Regards
Martin