There are three predefined modules involving truth values, namely, TRUTH-VALUE, TRUTH, and BOOL. The most basic one is TRUTH-VALUE, which has the following definition.
fmod TRUTH-VALUE is
sort Bool .
op true : -> Bool [special (id-hook SystemTrue)] .
op false : -> Bool [special (id-hook SystemFalse)] .
endfm
That is, the module just declares two constants, true and false.
The key thing to note is the special attribute associated to each of
the operator declarations for these constants. This states that the constants
are treated as built-in operators, so that instead of having the
standard treatment of any user-defined operator they are instead associated to
appropriate C++ code by "hooks" as stated next to the special
attribute. This is important, because certain basic constructs of the language
such as conditions in a conditional equation, membership axiom, or rule,
and also sort predicates associated to membership assertions evaluate to these
built-in truth values.
In general, many operators in predefined modules are special operators. In what follows, to lighten the exposition, we will omit the details about such hooks in special operators writing [special (...)] instead. The full definitions can be found in Appendix D.
The module TRUTH adds a number of important operators to TRUTH-VALUE.
fmod TRUTH is
protecting TRUTH-VALUE .
op if_then_else_fi : Bool Universal Universal -> Universal
[special ( ... )] .
op _==_ : Universal Universal -> Bool
[prec 51 special ( ... )] .
op _=/=_ : Universal Universal -> Bool
[prec 51 special ( ... )] .
endfm
The prec attribute in the last two operators gives a precedence to the
operator for parsing purposes (see Section 2.7.4). The operators
are, respectively, if_then_else_fi, and the built-in
equality and inequality predicates. These operators are special in a number
of ways. Firstly, they are automatically added to every module. 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. In fact, Universal is not a normal sort, but should instead
be understood as a polymorphic sort whose concrete effect is the instantiation
of the corresponding operators in each connected component. These operators
have the same semantics as their OBJ3 counterparts except that if if_then_else_fi fails to rewrite at the top, it then evaluates its then and else arguments. In particular, the equality and inequality
predicates are evaluated by reducing two ground terms to their normal form and
comparing the results for equality, modulo the equational axioms in the
attributes of the operators in the module.
Note that the equality and inequality predicates that the module TRUTH adds to each connected component of a user-defined module in a built-in and efficient way could in principle have been defined in a more cumbersome and inefficient way by the user. In fact, assuming as we usually do that the equations and membership axioms in the user module are Church-Rosser and terminating modulo the axioms in operator attributes, the corresponding initial algebra is a computable algebraic data type, for which equality and inequality are also computable functions. Therefore, by a well-known metaresult of Bergstra and Tucker [1], such equality and inequality 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 equality and inequality, by providing them in a built-in way.
Note also that, by the above metaargument, the use of inequality predicates in equations, membership axioms, or conditions, does not involve any real introduction of negation 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 without any use of negation.
The module BOOL imports TRUTH and adds the usual conjunction, disjunction, exclusive or, negation, and implication operators. Such 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
By default, the BOOL module is included as a submodule of any other module defined by the user. This is accomplished by the command
set include BOOL on .which can mention any module we wish to include--in this case BOOL--and is set when the standard library is entered. However, this default inclusion can be disabled. For example, if the user wished to have the polymorphic equality and if_then_else_fi operators automatically added to modules, but wanted to exclude the usual Boolean connectives for the built-in truth values, he/she could write
set include BOOL off . set include TRUTH on .
The last module involving truth values is the IDENTICAL module. It is not included by default in other modules. That is, it has to be imported explicitly if it is needed. When imported into a module, it adds to each of its connected components polymorphic operators for syntactic equality and inequality. That is, two ground terms are compared for syntactic equality--modulo the equational axioms in the attributes of the operators in the module--without performing any reduction of the terms by the equations in the module.
Note that what this module provides in a built-in way would require a considerably more cumbersome, and subtle, explicit definition at the user level. In fact, given that equality in a functional module is always semantic equality using the equations, to explicitly define the above operators the entire signature of the module would have to be duplicated in a disjoint copy, for which no equations would be given, except for the equational axioms in operator attributes. Then, the above syntactic operators would reduce to the standard semantic equality and inequality operators on that equationless disjoint copy of the signature.
fmod IDENTICAL is
op _===_ : Universal Universal -> Bool
[prec 51 strat (0) special ( ... )] .
op _=/==_ : Universal Universal -> Bool
[prec 51 strat (0) special ( ... )] .
endfm