quantified expression with empty array?

quantified expression with empty array?

[Stephen Leake]

I ran across this question recently:

If I have a quantified expression:

  (for some Child of Children => Predicate (Child))

what is the value if Children'Length = 0?

ARM 2012 4.5.8 8/4, 9/4 talk about evaluating the predicates, but in this case there are no predicates to evaluate.

I wrapped this piece of code in "if Children'Length = 0 then" to be safe.

-- Stephe

Re: quantified expression with empty array?

[Jeffrey R. Carter]

On 03/09/2018 06:15 PM, Stephen Leake wrote:
> I ran across this question recently:
> 
> If I have a quantified expression:
> 
>    (for some Child of Children => Predicate (Child))
> 
> what is the value if Children'Length = 0?

4.5.8(9) reads, "If the quantifier is some, the expression is True if the 
evaluation of any predicate yields True; evaluation of the quantified_expression 
stops at that point. Otherwise (every predicate has been evaluated and yielded 
False), the expression is False." As we all learned in school, a parenthetical 
expression can be discarded without changing the meaning, so this is equivalent 
to "If the quantifier is some, the expression is True if the evaluation of any 
predicate yields True; evaluation of the quantified_expression stops at that 
point. Otherwise, the expression is False."

Since no predicate evaluated to True, the expression is False.

-- 
Jeff Carter
"To Err is human, to really screw up, you need C++!"
Stéphane Richard
63

Re: quantified expression with empty array?

[Niklas Holsti]

On 18-03-09 19:15 , Stephen Leake wrote:
> I ran across this question recently:
>
> If I have a quantified expression:
>
> (for some Child of Children => Predicate (Child))
>
> what is the value if Children'Length = 0?
>
> ARM 2012 4.5.8 8/4, 9/4 talk about evaluating the predicates, but in
> this case there are no predicates to evaluate.

AARM 4.5.8 adds, for a "some" expression:

9.a/3  Ramification: The expression is False if the domain contains no 
values.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: quantified expression with empty array?

[Shark8]

On Friday, March 9, 2018 at 10:15:12 AM UTC-7, Stephen Leake wrote:
> I ran across this question recently:
> 
> If I have a quantified expression:
> 
>   (for some Child of Children => Predicate (Child))
> 
> what is the value if Children'Length = 0?
> 
> ARM 2012 4.5.8 8/4, 9/4 talk about evaluating the predicates, but in this case there are no predicates to evaluate.
> 
> I wrapped this piece of code in "if Children'Length = 0 then" to be safe.

(FOR SOME ...) is exactly equivalent to a "THERE EXISTS" in logic, therefore if the domain for the ∃x is the null-set, then the evaluation is False because the thing didn't exists.

OTOH, the (FOR ALL ...) construct is exactly equivalent to the "FOR ALL" in logic and all 0 objects of ∀x {NULL} satisfy that, the expression evaluates to True.

So just remember that FOR ALL and FOR SOME are, respectively, ∀ and ∃.