Page 1 of 2

Universal Quantification

Posted: 10 Sep 2015 11:45
by Martin Meyer
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:

Code: Select all

forall Gen do     DetermBody end forall

Code: Select all

foreach Gen trydo     DetermBody end foreach
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:

Code: Select all

not     ((         Gen,             not(DetermBody)     ))
Regards
Martin

Posted: 10 Sep 2015 17:51
by Peter Muraya
Hi Martin,
It was not clear to me (from Wikipedia) what universal quantification is? Could could you explain it in layman's terms, and why it is important?

Posted: 11 Sep 2015 0:04
by Martin Meyer
Hi Peter,

universal quantification is a construct in mathematical logic, in programming and as well in natural languages. In short, it means "for all".
Likewise I could say: Logical conjunction is a construct in mathematical logic, programming and natural languages. In short, it means "and".

For an example of universal quantification in VIP consider the fact database declared by

Code: Select all

class facts     patientSymptom : (         string Patient,         symptom Symptom)         nondeterm.
Suppose we have a certain patient, say Patient1, and a function getSymptom : () -> symptom nondeterm.

Now we want to code a proposition, which says, that
for all symptoms, which function getSymptom outputs nondeterministically, Patient1 has the particular symptom.
The code-fragment shall be determ, i.e. it succeeds when the proposition holds and fails otherwise.

One way to code it would be

Code: Select all

SymptomList = [Symptom || Symptom = getSymptom()], list::all(SymptomList, { (Symptom) :- patientSymptom(Patient1, Symptom), ! }),
So you see, predicate list::all/2 stands for universal quantification over elements of a list.

Regards
Martin

Posted: 11 Sep 2015 5:03
by Peter Muraya
Martin,
Its clear. Now to clarify your request .... so you want a (special) construct that is similar to the current version

Code: Select all

foreach X=f1() do f2(X) end foreach,
but one which can fail if f2(X) fails, in which case f2(X) has to be deterministic? That sounds reasonable to me.

Posted: 11 Sep 2015 8:49
by Martin Meyer
Yes, Peter,

that's what I suggest.

Regards
Martin

Posted: 11 Sep 2015 8:58
by Thomas Linder Puls
The construction is reasonable/sensible, especially from the logical point of view of the language.

However, the syntax would have to be something different. The phrasing "for all/each <something> do" is imperative and indicates that something will be done for all/each <something>, not just for some of them.

Using "trydo" will not help that just indicates that we will accept failure, but still go through the rest of the cases and finally succeed.

I doubt that my colleagues will think this is a necessary construction, so for now you will have to do without it.

Maybe if you come up with a really convincing syntax :-).

Posted: 11 Sep 2015 12:46
by Martin Meyer
Of course colleagues are right, that it's not a necessary 1st level construction of the language. But it would be one, which could make code more readable.

Indeed it isn't easy to find a short syntax, which expresses all aspects intuitively. Can one of these convince?

Code: Select all

foreach Gen while  DetermBody end foreach

Code: Select all

forall Gen while  DetermBody end forall

Code: Select all

tryall Gen while  DetermBody end tryall

Code: Select all

forall Gen holds  DetermBody end forall
Regards
Martin

Posted: 14 Sep 2015 18:37
by Peter Muraya
Hi Martin and Thomas,
How about...

Code: Select all

foreach Gen do  DetermBody end foreach
- keeping the same syntax as the present;
- checking to ensure that the body is deterministic
- documenting that the whole foreach construct fails if the body fails.

Posted: 14 Sep 2015 21:08
by Martin Meyer
Hi again, Peter,

the original foreach syntax was my 1st suggestion. But Thomas objected, that it does not express well enough, what the predicate does: It indicates that something will be done for each, but not for just some.

The problem of a phrase with while is, that it does not express, that the iteration does not only stop but fail, when the body fails.

My favorite -so far- is the forall <Gen> holds <something> phrase. Because it goes analogous to the syntax of and: Both are rather declarative than imperative phrases, but their execution plan is quite obvious. Moreover I suppose, in mathematics "forall .. holds .." is the most often used way to read the universal quantifier.

Regards
Martin

Posted: 15 Sep 2015 9:33
by Thomas Linder Puls
I don't find any of the proposals very good.

It is true that "holds" is used in that context, but always in the opposite order: <something> holds never holds <something>.

I believe the most common usual mathematical/logical reading of the universal quantifier is for all X <something> with a pause between X and <something>. When people are uncomfortable with the pause they may substitute a long phase like "it will be the case that", or "it is true that". Or perhaps when <something> is short: for all X <something> holds.

All in all, I still find all the proposals either misleading or awkward (or both).

Posted: 15 Sep 2015 12:32
by Paul Cerkez
before the for... capabilities were added to VIP (back when we only had to worry about Determ -NonDeterm and Succeed/Fail) I simply created my own predicate with a set of clauses that checked each condition and then executed <something>. There was almost always a 'graceful fail' at the end to go back up to the parent clause which in turn would succeed and allow processing to continue

I still do this today (old habits die hard :-) sometimes). The only time I use the for... actions is when I am executing something pretty simple (e.g., summing the weighted inputs to an ANN and calculating the output value) and I know it will never fail. (It also took me a while to incorporate if..then and if..then..else into my code once it became available. I like it but only use it sparingly.)

This discussion is interesting from a theoretical standpoint but personally I don't see the need for the UQ being implemented into the language when the language gives you the ability to implement the functionality. My other thought is 'how often would t be used" so is it worth the effort to implement it into the language as a generic functionality.

That said, it would be interesting to see someone create/implement a class (module) that can be used as a UQ, maybe as a toolbox item.

Posted: 15 Sep 2015 15:24
by Martin Meyer
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

Workaround of deterministic boy of foreach...end foreach

Posted: 15 Sep 2015 17:26
by Ferenc Nagy
Hi,
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

You can write more deterministic an nondeterm predicates separated by comma after foreach
like this.

Code: Select all

foreach Gen(X),    DetermPredicate1(X),    DetermPredicate2(X)  DetermPredicate3(X) /* empty body */ end foreach.

Posted: 16 Sep 2015 0:42
by Martin Meyer
Yes, Frank. In foreach Gen do Body end foreach, the placeholder Gen stands for a Term.
The manual teaches: A Term can be (amongst others) a PredicateCall or Term Operator Term.
The Operator in turn can be a comma (,).
Thus (provided there are predicates Gen/1, DetermPredicate1/1, ..) Gen can be expanded to

Code: Select all

Gen(X), DetermPredicate1(X), DetermPredicate2(X), DetermPredicate3(X)
The Body of a foreach term can be empty. Hence a legal foreach term is

Code: Select all

foreach Gen(X),      DetermPredicate1(X),      DetermPredicate2(X),      DetermPredicate3(X) do end foreach
However that construct does not model universal quantification.

Regards
Martin

Posted: 16 Sep 2015 7:15
by Peter Muraya
Hi all,
Frank's bodyless foreach construct, used as follows, ..

Code: Select all

..., foreach gen(X), determ_body(X) do end foreach, ...,
... is equivalent to the following usage...

Code: Select all

..., foreach_(),    %Note the leadig underbar to avoid the keyword ...,
... where foreach_() predicate is defined and implemented using traditional Prolog as follows...

Code: Select all

predicates     foreach_() procedure. clauses     foreach_():-          programControl::cutBackTrack()=Btop,          gen(X),          determ_body(Btop, X),          fail.     foreach_().         determ_body(_, X):-determ_body(X),!.     determ_body(Btop, _):-programControl::cutBackTrack(Btop).



This is not what I understand from Martin's request for universal quatification. The way I
understand it is that the usage is as follows ...

Code: Select all

..., forall gen(X) hold determ_body(X) end forall, %Now forall and hold are keywords ...,  
... and is equivalent to the ...

Code: Select all

..., programControl::cutBackTrack()=Btop, forall_(Btop),    %Note the leading underbar to avoid the (new) keyword forall ...,

... where the forall_() predicate is defined and implemented using traditional Prolog as follows...

Code: Select all

predicates     forall_(programControl::stackMark) determ. clauses     forall_(Btop):-          gen(X),          determ_body(Btop, X),          fail.     forall_(_).                  determ_body(_, X):-determ_body(X),!.      determ_body(Btop, _):-programControl::cutBackTrack(Btop).


Note that the main difference between the 2 constructs is the position of the stack mark being cut; in the first case it is immediately after the foreach_(); in the second case, it just before forall_().