TRIV

As already described in Section 6.3.1, the simplest non-empty theory is called TRIV and consists of a single sort. A model of this theory is just a set of any cardinality (finite or infinite). The intuition behind this simple theory is that the minimum requirement possible on a parameterized data type construction is having a data type as a set of basic elements to build more data on top of it. For example, in the LIST{X :: TRIV} parameterized data type construction we need a data type (set) of basic elements satisfying TRIV to then build lists of such elements.

  fth TRIV is
    sort Elt .
  endfth

The file prelude.maude includes many views out of TRIV that select the main sort of the built-in modules that we have already described in the previous sections. All these views are named in the same way: by the sort they select; for example, the standard view from TRIV into RAT selecting the sort Rat is also named Rat.

  view Bool from TRIV to BOOL is
    sort Elt to Bool .
  endv

  view Nat from TRIV to NAT is
    sort Elt to Nat .
  endv

  view Int from TRIV to INT is
    sort Elt to Int .
  endv

  view Rat from TRIV to RAT is
    sort Elt to Rat .
  endv

  view Float from TRIV to FLOAT is
    sort Elt to Float .
  endv

  view String from TRIV to STRING is
    sort Elt to String .
  endv

  view Qid from TRIV to QID is
    sort Elt to Qid .
  endv