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 static-meaning 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 static-meaning if:

• It is the ERROR symbol
• It is a variable whose name is not a function name (generator or selector) in any ADT, nor a reserved keyword., and if a variable appears in different subexpression, the ocurrences must agree in type.
• It is a generator g(E₁,...,E_n) defined in some ADT of environment with signature g:T₁T₂...T_nT_n+1.  Each argument E_i  must be an expression with static-meaning, and have type T_i.
• It is a selector s(E₁,...,E_n) defined in some ADT of environment with signature s:T₁T₂...T_nT_n+1.  Each argument E_i must be an expression with static-meaning, and have type T_i.
• It is an equality expression EQUAL(E₁,E₂), the expressions E₁ and E₂ have static-meaning and the same type.
• It is a conditional if E₁ then E₂ else E₃ fi, E₁ has meaning and type BOOL, E₂ and E₃ have static-meaning and the same type.

A cartesian product of ADT may conform the domain of a function (generator or selector) in a type a.  It has static-meaning 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 static-meaning 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 static-meaning if each generator has static-meaning.
 
 

4.4 Axioms

A set of axioms for a selector has static-meaning if it has all of the following properties:
 1. Each axioms must have static-meaning

An axiom S(E₁E₂...E_n)=T for a selector  S:T₁T₂...T_nT_n+1 has static-meaning if:

• Each E_i has type  T_i and T has type T_n+1.
• Each E_i is a variable or a generator of type T_i, instanced in generators and variables
• There are not repeated variables at left side
• Every variable at right side appears at left side (this condition and the two before it, ensure left linearity and not overlapping)
• If the ERROR symbol appears in T it should be the top symbol or it must be the second or third argument of an if-then-else-fi clause.

 Huet proposes in [Huet82] a property and an algorithm to verify this  (it's called complete set of axioms):
Definition.  Suppose a selector S of arity k, defined by p axioms, each one as S(A_i¹,..A_i^k)=T_i, where A_i^j is a variable or a generator.  Let R be the se of k-tuples of left sides, that is R={<A_i¹,..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:

1. k=0 and R={<>}
2. The set of k-1 tuples {<A_i²,..A_i^k> | A_i¹ is variable } is complete for the generators
3. (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₁,...P_n,A_i²,..A_i^k> | A_i¹=G( P₁,...P_n) with G generator }and {<x₁,..., x_n,A_i²,..A_i^k> | A_i¹ is variable } is complete for the generators.  (Here x₁,..., 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 .

• Reflexive: If E is term of type T composed of generators then EQ_T(E,E) must rewrite to TRUE
• Symmetric: If E₁ and E₂ are terms of type T composed of generators then EQ_T(E₁,E₂) and EQ_T(E₁,E₂) must rewrite to same term
• Transitive: If E₁, E₂ and E₃ are terms of type T composed of generators, and EQ_T(E₁,E₂) rewrites to TRUE, EQ_T(E₂,E₃) rewrites to TRUE then EQ_T(E₁,E₃) must rewrite to TRUE
• Preserve functions: If F is a selector with signature F:T₁T₂...T_nT, and E₁:T₁,E₂:T₂...,E_1n:T_n, D₁:T₁,D₂:T₂,...D_n:T_n are terms composed of generators and EQ_T₁(E₁,D₁) rewrites to TRUE, ...EQ_T_n(E_n,D_n) rewrites to TRUE then EQ_T(F(E₁,E₂,...E_n),F(D₁,D₂,...D_n)) must rewrite to TRUE

A selector has static-meaning if its name is not the name of any other function in environment, if its domain has static-meaning and its axioms have static-meaning.  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 static-meaning 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 static-meaning 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

Abstract Syntax Tree Operational Semantics