ManTa 3 
An ADT in ManTa is just a declaration, it can be used only when the user evaluates a selector, hence, the operational semantics is specified by showing how to evaluate an expression.
In the same way other functional and equational languages do, ManTa evaluates expressions by rewriting. The rewriting rules for a set of axioms is given by the axioms of the selectors, the static semantics ensures some properties of these rules: Left linear and strong local confluence.
We will begin by defining the notation and following [O'Donell85] recommendations we will describe:
5.1
Basical definitios

The set of terms is the set of expressions with staticmeaning, although they can be viewed in a constructive way:
Definition: Given a set of ADTs, let Cons be the set of all constructors (initials and constructors), Sel the set of the selectors of every type and Var a set of variables.
The set of ground terms is composed of:Definition : A substitution is a function :VarTerm such that (x)x only for finite variables. To express function application, the notation x is preferred (opposed to the traditional (x) ).
i. Every initial of arity 0
ii. If E_{1}, E_{2}, ... E_{n} are ground terms and CCons is a nary constructor then C(E_{1}, E_{2}, ... E_{n} ) is ground as long as it has staticmeaning (See Static Semantics).
The set of terms (Term) is composed of:
i. Every variable vVar
ii. Symbol ERROR
ii. Every ground term
iii. If E_{1}, E_{2}, ... E_{n} are terms and FConsSel{EQUAL, ifthenelse}, is a nary function then F(E_{1}, E_{2}, ... E_{n}) is term as long as it has staticmeaning (See Static Semantics).
Definition: Given P,QTerm,
the substitution is
called a match between the pattern P and the objective Q
if and only if P=
Q.
5.2
Expression representation and pattern matching algorithm

To ease the description each expression is represented as a nary tree derived from the type Expr (see Abstract Syntax Tree).
Pattern matching algorithm: Given a pattern P and a objective Q
Regarding the conditions for a match between two functions instantiated, as it will be presented later, the rewriting steps of ManTa only look for a match between the left side of an axiom as pattern and an expression as objective. Since the axioms are left linear (see static semantics), there are no repeated variables at left side and the union of the matches for the parameters is always a function.
 If P is variable and Q is a ground term and it isn't ERROR there is match {P Q }
 If P is a constant and Q is the same constant there is match and it's {}
 If F is a nary function, P_{i} (1in) are terms and Q_{i} (1in) are also terms, there is a match between the pattern F(P_{1},...P_{n}) and the objective F(Q_{1},...Q_{n}) when:
In that case the match is M_{1}M_{2}...M_{n}.
 for all i (1in) there is a match M_{i} between the pattern P_{i} and the objective Q_{i}
 and the set of pairs M_{1}M_{2}...M_{n} is a function.
 In any other case there isn't match.
5.3
Rewriting rule and Rewriting Algorithm

The version 3.0 of ManTa had a functional rewriting strategy (a list of axioms of which it was taken the first that could be applied). Now we apply a more traditional rule whose properties are better understood, it is an innermost rule.
Given an expression to rewrite the rewriting rule first rewrites the arguments and then the root.
Some programming languages use this strategy and in the case of imperative languages this rule correspond to the idea of function invocation (first the arguments are evaluated and then the function is invocated). One of the objectives of ManTa is to implement the ADTs in several programming languages (including imperative languages like C and Java). This reason has moved us to choose this rewriting rule (in this way we ensure equal behavior of translated ADT in any language).
It's known that this is the less terminating rule
[O'Donell77]. But that is the reason to choose it.
If a rewriting finishes with this rule, it will finish with any other rewriting
rule and the result will be the same.
5.4
Rewriting Step

A rewriting step (made for each node of the expression tree) looks for the top symbol and:
If it's a variable or the ERROR it is already in normal form
If it's a conditional ifthenelsefi evaluate the condition (first argument)If it's first argument is TRUE it rewrites in the secondIf it's the EQUAL symbol and the type of its arguments can be determined, let's say T, it rewrites to the equality of type T (i.e. EQ_T), with the same arguments. (For example the expression EQUAL(X,Y) can not be rewritten since its type can not be determined)
If it's first argument is FALSE it rewrites in the third
Otherwise it doesn't rewrite (The second and third arguments should be skipped, since the conditional is not strict)
If it's a generator evaluate its arguments
If it's a selector S (including an equality EQ_T), evaluate the arguments. Check the axioms for S, if there is match (the pattern is the left side of an axiom and the objective is S), rewrite with the right side of the axiom after applying the match.
5.5
Properties

Definition: Let's call system of rewriting rules for a set of ADTs the rules defined by the axioms for each selector of each ADT (given by the user) along with the rules:
IF TRUE THEN E1 ELSE E2 FI E1
IF FALSE THEN E1 ELSE E2 FI E2
EQUAL(E1,E2) EQ_T(E1,E2) if E1 has type T and E2 has type T
Property 1: The system of rewriting rules for a set of ADTs
is:
Theorem 1: Every terminating system of rewriting rules for a
set of ADTs in ManTa is confluent
This happens, because every Left Linear and locally confluent system
is confluent even with an innermost rule [Toyama88]
The rewriting algorithm shown has not any special considerations for the ERROR symbol neither for not defined terms. Hence the normal form for many terms that include the ERROR symbol is the same term. (e.g. SUC(ERROR), ADD(ERROR,ERROR), NOT(ERROR), etc.).
Another important property of a rewriting system is termination.
However we have not work on that topic, and by now it is a user responsibility.
