boolean `all` operator applied to empty sets is in conflict with its usage in mathematics

[eh-adblockplus-org]

In the documentation for the all operator (Rascal/Expressions/Values/Boolean/All), it states the following pitfall (paraphrased slightly)

When one of the expressions enumerates the elements of an empty list, all always returns false

The parallel construct in mathematics is a conjunction over a set, written with a big-wedge symbol, analogous to capital-sigma notation for sums. The conjunction over an empty set is, by definition, true. Rascal has this wrong.

Now why this is the definition is worth explaining. Let's start by analogy with other such operators over empty sets. The sum of an empty set is zero, the additive identity. The product of an empty set is one, the multiplicative identity. The disjunction of an empty set is false, the disjunctive identity, by the tautology (a || false) <==> a. And the conjunction of an empty set is true, the conjunctive identity.

The choice of an identity is not arbitrary. The reason is to allow the composite big-operators to interplay nicely with their small-size originals. Given a set S and a disjoint decomposition S = T_1 + T_2, we want to have the identity Op(S) == Op(T_1) op Op(T_2) no matter what T_1 and T_2 are, and this includes the case where one is the entire set and the other is empty. This consistency requirement mandates that the value is the operational identity.

For boolean logic, there's a further consequence. There's a standard identity that the negation of a conjunction is the disjunction of the negations: !all( b <- S ) == any( b <- { !x | bool x <- S } ). (And vice-versa.) The current values of all and any on empty sets are both false, breaking this identity.

[eh-adblockplus-org]

This topic came up elsewhere, somewhat as a tangent, and somewhat in disguise. It's more relevant here. In this comment, @jurgenvinju said:

void is a strict sub-type of int in Rascal's type system, for example to ensure that set[int] x = {}; is type-correct.

In order for set assignment to well-formed, every member of the rvalue set must be of the type as that of the lvalue set. As matter of formal logic, this is a statement quantified by a universal quantifier. For finite sets, a universal quantifier over a set is the same as a conjunction over it. (Dually, an existential quantifier expands as a disjunction.) An empty set is certainly finite, and a conjunction over an empty set is always true. Going back to the compatibility condition, because the rvalue in the example is empty, the compatibility condition is true irrespective of the type system. Considering this as an algorithm, the type-compatibility predicate function never executes because there are no elements in the rvalue set.

I'm not disputing anything about Rascal's type system, but the necessity that's implied in the second part of the quotation is wrong. While it's true that you can define type compatibility purely in terms of set[&T] predicates, it requires the arbitrary choice of assigning a type of set[void] to the literal for the empty set. The alternative, however, is to observe that the empty set is actually an element of all set[&T] types. As a universal member of all set types, it is an expression with a fundamentally ambiguous type, although that that doesn't matter in practice, because it's also universally compatible. (It's also worth noting that the empty set is the identity for the union operator for every set type.)

All this hinges on the fact that an empty conjunction is true by definition.

[PaulKlint]

You are completely right that the behavior of all is incorrect. This is one of the few cases where the Rascal compiler (still work in progress) differs from the Rascal interpreter. It is probably also necessary to impose restrictions on the arguments of all to let it completely behave as a universal quantifier.

[jurgenvinju]

This is a duplicate; we've got this design error of all and any reported a number of times. Will Have to find the others later.