DENOTATIONAL SEMANTICS 
We give semantics to every set of ADTs, defining it as an specification
with constructors as described in the thesis of Ulrich Kuhler
"A TacticBased Inductive Theorem Prover for Data Types with Partial Operations"
[Kuhler98].
In this section we present the notation, some definitions and results
of that work and then we define ADTs of ManTa..
6.1
Notation and basical definitios

Definition 1:
Definition 3: Given a specification with constructors spec=(sig,C,R), sig =( S,F,) with CF:
i) Let the sequence (_{RC,i})_{iN} of realtions on Term(sig,V^{G}) be defined byDefinition 5: An specification with constructors spec=(sig,C,R) is admissible if it satisfies:a) _{RC,0}=Then _{RC} = _{iNRC,i}
b) t1_{RC,i+1}t2 if there is a rewrite rule l=ru_{1}=v_{1},...,u_{n}=v_{n}, in R^{C} , a position p in t and an inductive substitution such that (1) t1/p=l (2) t2=t1[r]_{p}and (3) u_{kRC,i}v_{k}for k=1,2,..n
ii) Let the sequence (_{R,i})_{iN} of relations on Term(sig,V^{G}) be defined bya) _{R,0}=_{RC}Then _{R} = _{iNR,i}
b) t1_{R,i+1}t2 if t1_{RC}t2 or there is a rewrite rule l=r in R^{D} , a position p in t1 and an inductive substitution such that (1) t1/p=l (2) t2=t1[r]_{p } (3) for each u=v in , u_{R,i}v (4) for each def(u) in there is a ground term u' such that u_{R,i}* u' (_{R,i}* is the transitive, reflexive closure of _{R,i}) and (5) for each uv in there are ground terms u',v' such that u_{R,i}* u', v_{R,i}* v' and u'_{RC}v'
a) R=R^{C}R^{D}, where R^{C} is a set of constructors rules and R^{D} is a set of defining rulesProposition 1: Let spec=(sig,C,R) be an admissible specification. Then Term(sig,V^{G})/^{*}_{R} is a data model of spec.
b) _{R} is confluent
c) For each l=r_{1},...,_{n} and for each term t (not only composed of constructors), ocurring with a negation in a literal _{i} there is another literal _{j}=def(t).
Theorem 1: Let spec=(sig,C,R)
be an admissible specification, and let t_{1},t_{2}Term(sig,V^{G}).
Then t_{1}_{R,i}*
t_{2}
if and only if DMod(spec)t_{1}=t_{2}.
6.2 An interpretation
for a set of ADTs in ManTa

Definition 6: A set of ADTs without parameters that includes BOOL is a specification with constructors.
Given a finite set of basical ADTs in Manta (BOOL must be included) {A_{1},A_{2},...A_{n}}, let S be the set of names of ADTs {name(A_{1}),name(A_{2}),...,name(A_{n})], F is the set that contains the name of all functions F=functions(A_{1}) functions(A_{2}) .... functions(A_{n}) and is an arity function defined over F as (f)=domain(f) codomain(f). These three elements conform the signature of the set of ADTs sig=(S,F,).
Let C be the set of all constructors, and R the set of conditional equations obtained by translating each axiom of the set axioms(A_{1}) axioms(A_{1})...axioms(A_{1}).
To translate an axiom we must use the following rules:To manage nested if and ERROR in if clauses, the last two steps can be iterated. (The static semantics ensure that every expression that includes ERROR can be translated with those)Every variable in a ManTa specification is a constructor variable Every ocurrence of EQUAL must be substitued by EQ_T where T is the type of the arguments. (The EQUAL symbol is only syntactic sugar) Axioms not including if or ERROR, let's say L=R, are interpreted as:
L=Rdef(Var(L)),def(R) Where Var(L) denotes the set of variables in expression L {v_{1},v_{2}...,v_{k}} and def(Var(L)) donotes def(v_{1}),def(v_{2}),...def(v_{k}).Axioms whose right side is ERROR are not translated (since represents terms where the function is undefined) Axioms of the form L=if E1 then E2 else E3 fi, can be interpreted as:
L=E2def(Var(L)),def(E1),E1=TRUE,def(E2)
L=E3def(Var(L)),def(E1),E1=FALSE,def(E3)
A theorem to prove of the form l=r must be interpreted asl=rdef(Var(l)),def(Var(r)),def(l),def(r)with the same conversion rules exposed for axioms (variables are constructor variables, EQUAL replaced by EQ_T,etc.)
The previous definition doesn't include the case of extensions (ADTs without constructors), we can extend it by including the functions of the extension in the set of functions F, in the arity function and the translation of axioms as part of the set of conditional equations.
Example 1: Given the set of ADT {BOOL,
NAT}
we will translate it to an specification with constructors.
S={BOOL,NAT}, F={TRUE,FALSE,AND,OR,...,ZERO,SUC,ADD,ISZERO,DIV...} are the names of the functions of BOOL together with the functions of NAT.Proposition 2: A set of ADTs in ManTa is an admissible specification with constructors
The arity function : FS+ is given by(TRUE)=BOOLWith the previous definitions the signature has been constructed sig=(S,F,).
(FALSE)=BOOL
(AND)=BOOL BOOL BOOL
...
(ZERO)=NAT
(SUC)=NAT NAT
(ADD)=NAT NAT NAT
(ISZERO)=NAT BOOL
...
Define C as the set of constructors C={TRUE,FALSE,ZERO,SUC} and the set of conditional equations can be obtained:AND(B1,TRUE)=B1 def(B1)...
AND(B1,FALSE)=FALSE def(B1),,def(FALSE)
...
ADD(N1,ZERO)=N1 def(N1)
ADD(N1,SUC(N2))=SUC(ADD(N1,N2)) def(N1),def(N2),def(SUC(ADD(N1,N2)))
ISZERO(ZERO)=TRUE
ISZERO(SUC(N1))=FALSE def(N1)
As an example of nested if and ERROR we will present the translation of the axiom for DIV(N1,N2). The original axiom is:DIV(N1,N2) = if ISZERO(N2)Applying the rules for if we obtain
then ERROR
else if GE(N1,N2)
then SUC(DIV(SUBS(N1,N2),N2))
else ZERO
fi
fiThe first conditional equation can be removed (since ERROR is a symbol to specify where the function is undefined). The second one can be translated, by translating the equality with the rules for if, and adding the conditions already stated:DIV(N1,N2)=ERROR def(N1),def(N2),def(ISZERO(N2)),ISZERO(N2)=TRUE DIV(N1,N2)=if GE(N1,N2) then SUC(DIV(SUBS(N1,N2),N2)) else ZERO fi def(N1),def(N2),def(ISZERO(N2)),ISZERO(N2)=FALSEDIV(N1,N2)=SUC(DIV(SUBS(N1,N2))) def(N1),def(N2),def(ISZERO(N2)),ISZERO(N2)=FALSE,def(GE(N1,N2)), GE(N1,N2)=TRUE,def(SUC(DIV(SUBS(N1,N2)))) DIV(N1,N2)=ZERO < def(N1),def(N2),def(ISZERO(N2)),ISZERO(N2)=FALSE,def(GE(N1,N2)), GE(N1,N2)=FALSE,def(ZERO)
a) R=R^{C}R^{D}, where R^{C} is a set of constructors rules and R^{D} is a set of defining rulesIn ManTa there are not rules for constructors, since every axiom is translated to a defining rule that doesn't contain literals of the form def(t).b) _{R} is confluentWe already proved that our rewriting system is confluent, we must verify that it is in accordance with the definition of _{R}c) For each l=r_{1},...,_{n} and for each term t (not only composed of constructors), ocurring with a negation in a literal _{i} there is another literal _{j}=def(t).
We don't have rewriting rules for constructors, so we only must verify the condition ii.b of definition 4. .
(1) t1/p=l states that exists a redex
(2) t2=t1[r]_{p } states the rewriting of a redex by using an axiom
(3) for each u=v in , u_{R,i}v. We only have this case in traslations of if statements (E1=TRUE o E1=FALSE), and the rewriting algorithm doesn't rewrite an if unless its condition be rewritten to TRUE or FALSE .
(4) for each def(u) in there is a ground term u' such that u_{R,i}* u' . The innermost rewriting rule ensures that the components of an expression are evaluated to ground terms before rewritting the entire expression.
(5) for each uv in there are ground terms u',v' such that u_{R,i}* u', v_{R,i}* v' and u'_{RC}v'. In our case this never happens since the axioms and theorems are not translated to conditional equations with inequalities.We don't have literals with negations.
Proposition 3. Extensions to a set of ADTs are conservative
or constructorconsistent
This is so since, we don't allow conditions for the constructors and
the axioms for the functions can't damage the underlying types. The
static semantics ensures this, because the constructors can't be the outer
symbol of the left side in axioms and the strong confluence ensures that
there are not contradictions.
Proposition 4 Any set of ADTs in ManTa has a data model.
Since any set of ADT is and admissible specification, by proposition
1 it must have a data model.
Proposition 5. Proofs of equalities by rewriting are meaningfull
for any set of ADTs.
This is so, since the Theorem 1 states that equality by rewriting represents
the situation of equality in any data model.
Proposition 6. Proofs of equalities by induction are meaningfull
for any set of ADTs.
When we make proofs by induction we must introduce new axioms (induction
hypothesis), and try to prove a result by using the hypothesis.
In ManTa we only don't allow to state induction hypothesis for constructors,
only for selectors, hence the specification with the introduced hypothesis
is a conservative extension.
