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 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:

 4.2 Domains

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(E1E2...En)=T for a selector  S:T1T2...TnTn+1 has static-meaning if:
2. The set of axioms for a selector cover completely the domain of the selector
 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(Ai1,..Aik)=Ti, where Aij is a variable or a generator.  Let R be the se of k-tuples of left sides, that is R={<Ai1,..Aik> | 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 {<Ai2,..Aik> | Ai1 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

  4. (b) The union of the sets {<P1,...Pn,Ai2,..Aik> | Ai1=G( P1,...Pn) with G generator }and {<x1,..., xn,Ai2,..Aik> | Ai1 is variable } is complete for the generators.  (Here x1,..., xn are new variables).
3. The set of axioms is strongly locally confluent
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 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[]
  no: NAT * NoElem->NoElem

Abstract Syntax Tree

Operational Semantics