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:

• A representation for the expressions
• An algorithm of pattern matching
• An algorithm to select the next subexpression to reduce (redex )

An algorithm to rewrite the subexpression (i.e. a reduction step)

The set of terms is the set of expressions with static-meaning, 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:
  i. Every initial of arity 0
  ii. If E₁, E₂, ... E_n are ground terms and CCons is a n-ary constructor then C(E₁, E₂, ... E_n ) is ground as long as it has static-meaning  (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₁, E₂, ... E_n are terms and FConsSel{EQUAL, if-then-else},  is a n-ary function then F(E₁, E₂, ... E_n) is term as long as it has static-meaning (See Static Semantics).

VarTerm

x

• If c is constant (that is an 0-ary initial) c  = c
• If F is a n-ary function, and  E₁, E₂, ... E_n are terms  F(E₁, E₂, ... E_n)  = F(E₁ , E₂ , ... E_n )

x₁

x₂t₂

x_nt_n

in

v v

jn

 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 n-ary tree derived from the type Expr  (see Abstract Syntax Tree).

Pattern matching algorithm: Given a pattern P and a objective Q

• 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 n-ary function, P_i (1in) are terms and Q_i (1in) are also terms, there is a match between the pattern F(P₁,...P_n) and the objective F(Q₁,...Q_n) when:
  • 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₁M₂...M_n is a function.
  In that case the match is M₁M₂...M_n.
• In any other case there isn't match.

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  if-then-else-fi evaluate the condition (first argument)

If it's first argument is TRUE it rewrites in the second
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 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 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.

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:

1. Left linear
2. Not overlapping
3. Locally confluent (because it is strongly locally confluent)

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.
 
 

Static Semantics Denotational Semantics