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


Revision: r1.3 - 28 Apr 2005 - 22:24 -
Stratego > StrategoGlossary > AlgebraicSignature
Copyright © 1999-2020 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback