Boolean Values

This section deals with logical values ("Booleans").

Booleans are primarily of importance as (return) values for (intrinsic) predicates. It is important to know that the truth-value of the operators and and or is always evaluated left to right, that is, the left-most clause is evaluated first, and if that determines the value of the operator evaluation is aborted; if not, the next clause is evaluated, etc. So, for example, if x is a boolean, it is safe (albeit silly) to type: 

> if x eq true or x eq false or x/0 eq 1 then
>    "fine";
> else
>    "error";
> end if;
even though x/0 would cause an error ("Bad arguments", not "Division by zero"!) upon evaluation, because the truth value will have been determined before the evaluation of x/0 takes place.

Contents

Creation of Booleans

Booleans() : -> Bool
The Boolean structure.
# B : Bool -> RngIntElt
Cardinality of Boolean structure (2).
true
false
The Boolean elements.
Random(B) : Bool -> BoolElt
Return a random Boolean.

Boolean Operators

x and y : BoolElt, BoolElt -> BoolElt
Returns true if both x and y are true, false otherwise. If x is false, the expression for y is not evaluated.
x or y: BoolElt, BoolElt -> BoolElt
Returns true if at least one of x and y is true, false otherwise. If x is true, the expression for y is not evaluated.
x xor y: BoolElt, BoolElt -> BoolElt
Returns true if either x or y is true, but not both, false otherwise.
not x : BoolElt -> BoolElt
Negate the truth value of x.

Equality Operators

Magma provides two equality operators: eq for strong (comparable) equality testing, and cmpeq for weak equality testing. The operators depend on the concept of comparability. Objects x and y in Magma are said to be comparable if both of the following points hold:

(a)
x and y are both elements of a structure S or there is a structure S such x and y will be coerced into S by automatic coercion;
(b)
There is an equality test for elements of S defined within Magma.

The possible automatic coercions are listed in the descriptions of the various Magma modules. For instance, the table in the introductory chapter on rings shows that integers can be coerced automatically into the rational field so an integer and a rational are comparable.

x eq y : Any, Any -> BoolElt
If x and y are comparable, return true if x equals y (which will always work by the second rule above). If x and y are not comparable, an error results.
x ne y : Any, Any -> BoolElt
If x and y are comparable, return true if x does not equal y. If x and y are not comparable, an error results.
x cmpeq y : Any, Any -> BoolElt
If x and y are comparable, return whether x equals y. Otherwise, return false. Thus this operator always returns a value and an error never results. It is useful when comparing two objects of completely different types where it is desired that no error should occur. However, it is strongly recommended that eq is usually used to allow Magma to pick up common unintentional type errors.
x cmpne y : Any, Any -> BoolElt
If x and y are comparable, return whether x does not equal y. Otherwise, return true. Thus this operator always returns a value and an error never results. It is useful when comparing two objects of completely different types where it is desired that no error can happen. However, it is strongly recommended that ne is usually used to allow Magma to pick up common unintentional type errors.

Example State_Equality (H1E7)

We illustrate the different semantics of eq and cmpeq. 
> 1 eq 2/2;
true
> 1 cmpeq 2/2;
true
> 1 eq "x";
Runtime error in 'eq': Bad argument types
> 1 cmpeq "x";
false
> [1] eq ["x"];
Runtime error in 'eq': Incompatible sequences
> [1] cmpeq ["x"];
false

Iteration

A Boolean structure B may be used for enumeration: for x in B do, and x in B in set and sequence constructors.

Example State_Booleans (H1E8)

The following program checks that the functions ne and xor coincide. 
> P := Booleans();
> for x, y in P do
>      (x ne y) eq (x xor y);
> end for;
true
true
true
true
Similarly, we can test whether for any pair of Booleans x, y it is true that x = y iff (x ^ y) v (not x ^ not y). 
> equal := true;
> for x, y in P do
>     if (x eq y) and not ((x and y) or (not x and not y)) then
>         equal := false;
>     end if;
> end for;
> equal;
true
V2.28, 13 July 2023