An algebraic signature describes the structure of a set of terms. A signature introduces one or more AlgebraicSorts, i.e., collections of terms. Sorts are inhabited by declaring TermConstructors. A constructor has a name and zero or more subterms. A constructor is declared by stating its name, the list of sorts of its direc subterms and the sort of the constructed term. Constructor names may be overloaded. The sorts String and Int are predefined.

A typical example of a signature is the following description of LambdaCalculus^? expressions.

signature
  sorts Exp 
  constructors
    Var : String -> Exp
    App : Exp * Exp -> Exp
    Abs : String * Exp -> Exp

Term Injections

A term injection is a constructor-less constructor in a signature.

Example:

signature
  sorts Var Exp
  constructors
    Var : String -> Var
        : Var -> Exp
    Abs : Var * Exp -> Exp

Issues

• FixedLengthTuple
• TermAnnotation
• PolymorphicTypes^?

-- EelcoVisser - 09 Dec 2001

---

CategoryGlossary