many-sorted structure


Let L be a many-sorted language and S the set of sorts. A many-sorted structure M for L, or simply an L-structureMathworldPlanetmath consists of the following:

  1. 1.

    for each sort sS, a non-empty set As,

  2. 2.

    for each function symbol f of sort type (s1,,sn):

    • if n>1, a function fM:As1××Asn-1Asn

    • if n=1 (constant symbol), an element fMAs1

  3. 3.

    for each relation symbol r of sort type (s1,,sn), a relationMathworldPlanetmathPlanetmath (or subset)

    rMAs1××Asn.

A many-sorted algebra is a many-sorted structure without any relations.

Remark. A many-sorted structure is a special case of a more general conceptMathworldPlanetmath called a many-sorted interpretation, which consists all of items 1-3 above, as well as the following:

  • 4.

    an element xMAs for each variable x of sort s.

Examples.

  1. 1.

    A left module over a ring can be thought of as a two-sorted algebraPlanetmathPlanetmath (say, with sorts {s1,s2}), for there are

    • there are two non-empty sets M (corresponding to sort s1) and R (corresponding to sort s2), where

    • M has the structure of an abelian groupMathworldPlanetmath (equipped with three operationsMathworldPlanetmath: 0,-,+, corresponding to function symbols of sort types (s1),(s1,s1), and (s1,s1,s1))

    • R has the structure of a ring (equipped with at least four operations: 0,-,+,×, corresponding to function symbols of sort types (s2),(s2,s2) and (s2,s2,s2) for + and ×, and possibly a fifth operation 1 of sort type (s2))

    • a function :R×MM, which corresponds to a function symbol of sort type (s2,s1,s1). Clearly, is the scalar multiplication on the module M.

    For a right module over a ring, one merely replaces the sort type of the last function symbol by the sort type (s1,s2,s1).

  2. 2.

    A deterministicMathworldPlanetmath semiautomaton A=(S,Σ,δ) is a two-sorted algebra, where

    • S and Σ are non-empty sets, corresponding to sorts, say, s1 and s2,

    • δ:S×ΣS is a function corresponding to a function symbol of sort type (s1,s2,s1).

  3. 3.

    A deterministic automaton B=(S,Σ,δ,σ,F) is a two-sorted structure, where

    • (S,Σ,δ) is a semiautomaton discussed earlier,

    • σ is a constant corresponding to a nullary function symbol of sort type (s1),

    • F is a unary relation corresponding to a relation symbol of sort type (s1).

    Because F is a relation, B is not an algebra.

  4. 4.

    A complete sequential machine M=(S,Σ,Δ,δ,λ) is a three-sorted algebra, where

    • (S,Σ,δ) is a semiautomaton discussed earlier,

    • Δ is a non-empty sets, corresponding to sort, say, s3,

    • λ:S×ΣΔ is a function corresponding to a function symbol of sort type (s1,s2,s3).

References

  • 1 J. D. Monk, Mathematical Logic, Springer, New York (1976).
Title many-sorted structure
Canonical name ManysortedStructure
Date of creation 2013-03-22 17:45:17
Last modified on 2013-03-22 17:45:17
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 9
Author CWoo (3771)
Entry type Definition
Classification msc 03B70
Classification msc 03B10
Classification msc 03C07
Synonym many sorted structure
Synonym many sorted algebra
Defines many-sorted interpretation
Defines many-sorted algebra