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 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 E1, E2, ... En are ground terms and CCons is a n-ary constructor then C(E1, E2, ... En ) 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  E1, E2, ... En are terms and FConsSel{EQUAL, if-then-else},  is a n-ary function then F(E1, E2, ... En) is term as long as it has static-meaning (See Static Semantics).

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) ).
A substitution can be extended to a function with subsets of Term as domain and codomain : A substitution can be written as = {x1 t1, x2t2 ,..., xntn,} where xi (1in) is variable and if for any variable v, v  exists  1jn such that v=xj.
We call Sust the set of substitution, that is Sust={ is substitution }

 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

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

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)
Property 2: The rewriting algorithm presented preserves static semantics
Since it only tries to rewrite with terms of proper type and uses names defined by the user (that have static semantics).

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