There are four modules involving Boolean values, namely, TRUTH-VALUE, TRUTH, BOOL, and EXT-BOOL. The most basic one is TRUTH-VALUE, which has the following definition.
fmod TRUTH-VALUE is
sort Bool .
op true : -> Bool [ctor special (...)] .
op false : -> Bool [ctor special (...)] .
endfm
This module just declares the two Boolean values true and false as constants of sort Bool. The key thing to note is the special attribute associated with each of the operator declarations for these constants. In the case of Boolean values this is especially important, because certain basic constructs of the language such as conditions in a conditional equation, membership axiom, or rule, and also sort predicates associated with membership assertions evaluate to these built-in truth values.
The module TRUTH adds three important operators to TRUTH-VALUE.
fmod TRUTH is
protecting TRUTH-VALUE .
op if_then_else_fi : Bool Universal Universal -> Universal
[poly (2 3 0) special (...)] .
op _==_ : Universal Universal -> Bool
[poly (1 2) prec 51 special (...)] .
op _=/=_ : Universal Universal -> Bool
[poly (1 2) prec 51 special (...)] .
endfm
The operators are, respectively, if_then_else_fi, and the built-in
operators for equality and inequality predicates.7.1 These operators are special
in a number of ways. Firstly, they are, by default, automatically added to
every module (see Section 3.9.3). Secondly, they are
polymorphic, so that, for each module, they can be considered to be
normal operators that are ad-hoc overloaded for each connected component in the
module. This is done by means of the polymorphic (or poly)
attribute, as discussed in Section 4.4.4, and the symbol Universal,
that should not be considered a common sort, as explained at the end of this
section. For example, in the declaration of the if_then_else_fi operator,
the attribute poly (2 3 0) means that if_then_else_fi
is polymorphic in its second and third arguments as well as in its result.
The if_then_else_fi operator first rewrites its first argument,
the test. If the result is of sort Bool, the then or else argument is
selected, according to whether the test evaluated to true or false, and
rewritten. If the test result is not of sort Bool the then and
else arguments are rewritten. For example, working in the INT module
(see Section 7.4) we get the following reductions:
Maude> red in INT : if 4 - 2 == 2 then 0 else 1 fi . result Zero: 0
Maude> red if 4 - 2 =/= 2 then 0 else 1 fi . result NzNat: 1
The built-in Boolean predicates _==_ and _=/=_ have a
straightforward operational meaning: given an expression u == v with
u and v ground terms (i.e., terms without variables), then both
u and v are simplified by the equations in the module (which
are assumed to be Church-Rosser and terminating) to their canonical forms
(perhaps modulo some axioms such as assoc, etc., see Section
4.4.1) and these canonical forms are compared for equality. If they
are equal, the value of u == v is true; if they are
different, it is false. The predicate u =/= v is just the
negation of u == v.
Similar in spirit to the built-in operators for equality predicates,
there are built-in operators for membership predicates:
_:: S for each sort S.
These do not need to be explicitly declared, because they are part of the
extended signature associated with each module,
as described in
Section 3.9.3.
The operational meaning for membership operators
is analogous to that of the equality operators. Namely, given a
term u and a sort S in its kind, the built-in predicate
u :: S is evaluated by reducing u to its canonical form,
computing its least sort (under the preregularity, Church-Rosser, and
termination assumptions), and checking that it is smaller than or equal
to S.
But what about the mathematical meaning of these built-in predicates? That is, do they really correspond to ordinary equations (and not to negations or other Boolean combinations of such equations)? The point is that these built-in and efficiently implemented equality and inequality predicates could in principle have been defined in a more cumbersome and inefficient way by the user. In fact, assuming that the equations and membership axioms in the user's module are Church-Rosser and terminating modulo the equational axioms in the operator attributes (see Section 4.4.1) and that the operators satisfy the preregularity requirement, the corresponding initial algebra is a computable algebraic data type, for which equality, inequality, and membership in a sort are also computable functions. Therefore, by a well-known theorem of Bergstra and Tucker [4], such predicates can themselves be equationally defined by Church-Rosser and terminating equations. It is of course very convenient, and much more efficient, to unburden the user from having to give those explicit equational definitions of the equality, inequality, and membership predicates by providing them in a built-in way.
Note also that, by the above meta-argument, the use of inequality predicates, negations of membership predicates, or any Boolean combination of such predicates in abbreviated Boolean conditions does not involve any real introduction of negation (or other Boolean connectives) in the underlying membership equational logic, which remains a Horn logic. What we are really doing is adding more Boolean-valued functions to the module, but such functions, although provided in a built-in way for convenience and efficiency, could have been equationally defined by the user without any use of negation.
The module BOOL imports TRUTH and adds the usual conjunction, disjunction, exclusive or, negation, and implication operators.7.2These operators are defined entirely equationally.
fmod BOOL is
protecting TRUTH .
op _and_ : Bool Bool -> Bool [assoc comm prec 55] .
op _or_ : Bool Bool -> Bool [assoc comm prec 59] .
op _xor_ : Bool Bool -> Bool [assoc comm prec 57] .
op not_ : Bool -> Bool [prec 53] .
op _implies_ : Bool Bool -> Bool [gather (e E) prec 61] .
vars A B C : Bool .
eq true and A = A .
eq false and A = false .
eq A and A = A .
eq false xor A = A .
eq A xor A = false .
eq A and (B xor C) = A and B xor A and C .
eq not A = A xor true .
eq A or B = A and B xor A xor B .
eq A implies B = not(A xor A and B) .
endfm
As noted above the BOOL module is imported (in including mode) by default as a submodule of any other module defined by the user. This is accomplished by the command
set include BOOL on .
that appears in the standard library file prelude.maude. The
set include command can mention any module we wish to import--in
this case BOOL. However, this default importation can be disabled. For
example, if the user wished to have the polymorphic equality, inequality and
if_then_else_fi operators automatically added to modules, but wanted to
exclude the usual Boolean connectives for the built-in truth values, this
could be accomplished by writing
set include BOOL off . set include TRUTH on .
Similar commands are available for enabling and disabling implicit importation in extending and protecting modes (see Section 16.11). For example, the BOOL module can be protected by default instead of included by writing
set include BOOL off . set protect BOOL on .
The module EXT-BOOL declares short-circuit versions of the conjunction and disjunction operators such as those found in LISP and other programming languages. Like the operators declared in BOOL, these operators are defined entirely equationally. The short-circuit behavior is the result of the strategy attributes declared for the operators as discussed in Section 4.4.7.
fmod EXT-BOOL is
protecting BOOL .
op _and-then_ : Bool Bool -> Bool
[strat (1 0) gather (e E) prec 55] .
op _or-else_ : Bool Bool -> Bool
[strat (1 0) gather (e E) prec 59] .
var B : [Bool] .
eq true and-then B = B .
eq false and-then B = false .
eq true or-else B = true .
eq false or-else B = B .
endfm
When the module BOOL is imported, the system automatically adds
to the module an operator to test for membership, _:: S, for each
sort S, as mentioned above (see also Section 3.9.3).
Again, working in the NUMBERS module we have the following examples:
Maude> red in NUMBERS : sd(zero, zero) :: Zero . result Bool: true
Maude> red sd(zero, zero) :: NzNat . result Bool: false
Maude> red sd(zero, zero) :: Nat . result Bool: true
Maude> red (zero nil) :: Zero . result Bool: true
The term sd(zero, zero) reduces to zero,
which has least sort Zero but also its supersort Nat.
The term zero nil has also sort Zero because, using the
equational axioms for the assoc and id: nil attributes,
zero nil is the same as zero, which has sort Zero.
Note that these membership predicates are polymorphic on sorts, not on kinds. This is because to be syntactically well-formed the argument term must be of the right kind, namely the connected component containing the sort being tested. Thus a membership at the kind level is either trivially true or a syntactic error. Also, the presence of the system truth values is required for the predicates to be meaningful, so they are only added to modules that import the module TRUTH-VALUE (which is included by default, as part of BOOL, unless the user specifies otherwise).
Advisory. In fact, the symbol Universal does not denote a real sort: it is instead a place holder for parsing purposes that is given an interpretation by the polymorphic attribute (see Section 4.4.4). The concrete effect of the interpretation of Universal is the instantiation in each connected component of the operators with one or more Universal arguments.