Algebraic Signature

Stratego -- Strategies for Program Transformation
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.

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

Term Injections

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


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


-- EelcoVisser - 09 Dec 2001