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.
<verbatim>
signature
  sorts Exp 
  constructors
	 Var : String -> Exp
	 App : Exp * Exp -> Exp
	 Abs : String * Exp -> Exp
</verbatim>

---+++ Term Injections

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

Example:
<verbatim>
signature
  sorts Var Exp
  constructors
	 Var : String -> Var
		  : Var -> Exp
	 Abs : Var * Exp -> Exp
</verbatim>

Issues
	* FixedLengthTuple
	* TermAnnotation
	* PolymorphicTypes

-- Main.EelcoVisser - 09 Dec 2001 <br />
-----
CategoryGlossary