ManTa 3 
The static semantics checks: (1) nomenclature rules (2) type of expressions (3) restrictions on axioms to ensure rewriting properties. In order to acomplihs this, we use a predicate staticmeaning that is acomplished by the elements of the AST whit static semantics.
The semantics of any component of an AST, depends of the defined ADTs.
The set of defined ADT is called here the environment.
4.1
Expressions

An expression has staticmeaning if:
4.2 Domains

A cartesian product of ADT may conform the domain of a function (generator
or selector) in a type a. It has staticmeaning if each ADT
in product belongs to the environmente or is a. Besides each
ADT in product should be basic (as an exception, to offer a little of polymorphism
a
can appear)
4.3 Generators

A generator has staticmeaning if its name is not the name of any other
function in environment and if its domain has meaning. Besides the
codomain muest be the defined ADT and the name can not be a reserved keyword
nor begin with EQ_ (those names are reserved for equality
selectors)
A set of generators has staticmeaning if each generator has staticmeaning.
4.4 Axioms

A set of axioms for a selector has staticmeaning if it has all of the
following properties:
1. Each axioms must have staticmeaning
An axiom S(E_{1}E_{2}...E_{n})=T for a selector S:T_{1}T_{2}...T_{n}T_{n+1} has staticmeaning if:
Huet proposes in [Huet82] a property and an algorithm to verify this (it's called complete set of axioms):3. The set of axioms is strongly locally confluent
Definition. Suppose a selector S of arity k, defined by p axioms, each one as S(A_{i}^{1},..A_{i}^{k})=T_{i}, where A_{i}^{j} is a variable or a generator. Let R be the se of ktuples of left sides, that is R={<A_{i}^{1},..A_{i}^{k}>  1ip}, the set of axioms is complete for the generators if and only if R is complete. A tuple of variables and generators (e.g. R) is complete for the generators if it verifies only one of the following conditions:
 k=0 and R={<>}
 The set of k1 tuples {<A_{i}^{2},..A_{i}^{k}>  A_{i}^{1} is variable } is complete for the generators
 (a) For every generator G of the type of the first parameter, there is at least one axiom beginning with the symbol G
(b) The union of the sets {<P_{1},...P_{n},A_{i}^{2},..A_{i}^{k}>  A_{i}^{1}=G( P_{1},...P_{n}) with G generator }and {<x_{1},..., x_{n},A_{i}^{2},..A_{i}^{k}>  A_{i}^{1} is variable } is complete for the generators. (Here x_{1},..., x_{n} are new variables).
A set of axioms is strongly locally confluent if given two axioms whose left sides unify with mgu (most general unifier) , their right sides are identical after applying .4. If the selector is an equality for type T, (i.e EQ_T:T*T>BOOL where T is the name of an ADT) the axioms must define a congruence:
4.5 Selectors

A selector has staticmeaning if its name is not the name of any other
function in environment, if its domain has staticmeaning and its axioms
have staticmeaning. The name of a selector can not be a reserved
keyword, and if it is
EQ_T,
T
should be the name of the defined ADT (and as it was said before, its axioms
must define a congruence).
A set of selectors has meaning if each selector has meaning.
4.6
Parameters

A list of parameters for a type has staticmeaning if there are no repeated
parameters and none of them has the name of a type name. As mentioned
earlier the parameters are not treated in this document since they are
not fully supported in ManTa 3.1. They will not be explained in the
following sections.
4.7 Abstract
Data Types

An ADT has staticmeaning if its name is not the name of any other ADT nor the name of the parameter of other ADT. The parameters, the generators and the selectors must be valid. If it's an initial ADT it should have at least one inital funciton (it ensures a non empty ADT).
e.g. The following declaration doesn't define an ADT since it would not have elements:
ADT NoElem[]
INITIALS
CONSTRUCTORS
no: NAT * NoElem>NoElem
SELECTORS
