glbSorts

The operation glbSorts takes as arguments the metarepresentation of a module $\mathcal{R}$ and the metarepresentations of two types, that is, either sorts or kinds.

  op glbSorts : Module Type Type ~> TypeSet [special (...)] .

According to whether the types passed to glbSorts as arguments are metarepresented sorts or kinds, we can distinguish the following cases:

• If both types given as arguments are sorts in $\mathcal{R}$, then glbSorts returns the metarepresentation of the set (which can be empty) consisting of the largest sorts that are common subsorts of the two given sorts, that is, the set of maximal lower bounds of the two sorts; when this set is a singleton set $\{s\}$, then $s$ will be the greatest lower bound of the two sorts, thus the operation name glbSorts.

  For example, we have the following reductions concerning sorts in the module NUMBERS.

    Maude> reduce in META-LEVEL :
             glbSorts(upModule('NUMBERS, false), 'Zero, 'Nat) .
    result Sort: 'Zero
  

    Maude> reduce in META-LEVEL :
             glbSorts(upModule('NUMBERS, false), 'NatSet, 'NatSeq) .
    result Sort: 'Nat
  

    Maude> reduce in META-LEVEL :
             glbSorts(upModule('NUMBERS, false), 'NzNat, 'NzNat) .
    result Sort: 'NzNat
  

    Maude> reduce in META-LEVEL :
             glbSorts(upModule('NUMBERS, false), 'Zero, 'NzNat) .
    result EmptyTypeSet: (none).EmptyTypeSet
  

    Maude> reduce in META-LEVEL :
             glbSorts(upModule('NUMBERS, false), 'NzNat, 'Bool) .
    result EmptyTypeSet: (none).EmptyTypeSet
  

• If both types given as arguments are kinds in $\mathcal{R}$, then glbSorts returns the empty set when both kinds are different, and the metarepresentation of the kind (using the corresponding complete name) when both kinds are equal. For example,

    Maude> reduce in META-LEVEL :
           glbSorts(upModule('NUMBERS, false), '`[Nat`], '`[Bool`]) .
    result EmptyTypeSet: (none).EmptyTypeSet
  

    Maude> reduce in META-LEVEL :
           glbSorts(upModule('NUMBERS, false),'`[Nat`],'`[NatSeq`]) .
    result Kind: '`[NatSeq`,NatSet`]
  

• If one type is one sort in $\mathcal{R}$ and the other one is a kind in $\mathcal{R}$, then glbSorts returns the metarepresentation of the sort when the sort belongs to the kind, and the empty set otherwise. For example,

    Maude> reduce in META-LEVEL :
             glbSorts(upModule('NUMBERS, false), '`[Nat`], 'Bool) .
    result EmptyTypeSet: (none).EmptyTypeSet
  

    Maude> reduce in META-LEVEL :
             glbSorts(upModule('NUMBERS, false), '`[NatSeq`], 'Zero) .
    result Sort: 'Zero
  

    Maude> reduce in META-LEVEL :
            glbSorts(upModule('NUMBERS, false), 'NzNat, '`[NatSet`]) .
    result Sort: 'NzNat