ManTa 3 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 Tactic-Based 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:

• An specification with constructors spec=(sig,C,R) is a tuple, where sig is a signature, C is a set of constructors and R a set of conditional equations.
• A signature is a tuple, sig =( S,F,), where S is a set of sort names, F is a set of function symbols and  is an arity function.  i.e. A function whose domain is F and whose codomain is S+ (the nonempty strings with alphabet S)
• The constructors are functions symbols, and for each sort there should be at least one constructor.
• A conditional equation is a clause, l=r  1,...,n, where each i is one of the following (or it's negation):
• t1=t2
• def(t)
Definition 2 : Given an specification with constructors spec=(sig,C,R)
• A sig-algebra A (an algebra where the signature is interpreted) is called a model of spec if the interpretation of each conditional equation of R is valid in A. The class of all models of spec is denoted Mod(spec)
• We say that a model A of spec is a data model of spec, if for all constructor ground terms t1,t2 whose interpretations in A are equal, we have that t1=t2 is valid in every model of spec. DMod(spec) denotes the class of all data models of spec.
In [Kuhler98] there are two kinds of variables, constructor variables (VC) and general variables (VG). Term(sig,VG) denotes the set of terms constructed with the symbols in the signature sig and using general variables.

Definition 3: Given a specification with constructors spec=(sig,C,R), sig =( S,F,) with CF:

• A constructor rule is a rewrite rule l=r u1=v1,...,un=vn such that:
• l,r is composed with constructors and variables, and ui,vi is composed with constructors and constructor variables VC
• Var(l)Var(r), and Var(ui)Var(vi)Var(l) for i=1,2,...n
• A defining rule is a rewrite rule l=r   satisfying
• l is not composed only of constructors
• doesn't contain any literal of the form def(t)
Definition 4: Let spec=(sig,C,R) be a specification with constructors and R=RCRD where RC is a set of constructor rules and RD a set of defining rules
i) Let the sequence (RC,i)iN of realtions on Term(sig,VG) be defined by
a) RC,0=
b) t1RC,i+1t2 if there is a rewrite rule l=ru1=v1,...,un=vn, in RC , a position p in t and an inductive substitution  such that (1) t1/p=  (2) t2=t1[r]pand  (3)  ukRC,ivkfor k=1,2,..n
Then RCiNRC,i
ii) Let the sequence (R,i)iN of relations on Term(sig,VG) be defined by
a) R,0=RC
b) t1R,i+1t2 if t1RCt2 or there is a rewrite rule l=r in RD , a position p in t1 and an inductive substitution  such that (1) t1/p=  (2) t2=t1[r]p   (3) for each u=v in uR,iv  (4) for each def(u) in  there is a ground term u' such that uR,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 uR,i* u', vR,i* v' and  u'RCv'
Then RiNR,i
Definition 5: An specification with constructors spec=(sig,C,R) is admissible if it satisfies:
a) R=RCRD, where RC is a set of constructors rules and RD is a set of defining rules
b) R is confluent
c) For each l=r1,...,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).
Proposition 1: Let spec=(sig,C,R) be an admissible specification. Then Term(sig,VG)/*R is a data model of spec.

Theorem 1: Let  spec=(sig,C,R) be an admissible specification, and let t1,t2Term(sig,VG).  Then t1R,i* t2 if and only if DMod(spec)t1=t2.

 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) {A1,A2,...An}, let S be the set of names of ADTs {name(A1),name(A2),...,name(An)], F is the set that contains the name of all functions F=functions(A1 functions(A2) ....  functions(An) 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(A1 axioms(A1)...axioms(A1).
To translate an axiom we must use the following rules:
• 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 {v1,v2...,vk} and def(Var(L)) donotes def(v1),def(v2),...def(vk).
• 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)
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)
A theorem to prove of the form l=r must be interpreted as
l=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.
The arity function : FS+ is given by
(TRUE)=BOOL
(FALSE)=BOOL
(AND)=BOOL BOOL BOOL
...
(ZERO)=NAT
(SUC)=NAT NAT
(ISZERO)=NAT BOOL
...
With the previous definitions the signature has been constructed sig=(S,F,).
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)
...
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)
then ERROR
else if GE(N1,N2)
then SUC(DIV(SUBS(N1,N2),N2))
else ZERO
fi
fi
Applying the rules for if we obtain
```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)=FALSE```
The 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)=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)```
Proposition 2: A set of ADTs in ManTa is an admissible specification with constructors
To see this, we must verify each condition of definition 5:
a) R=RCRD, where RC is a set of constructors rules and RD is a set of defining rules
In 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 confluent
We already proved that our rewriting system is confluent, we must verify that it is in accordance with the definition of R
We don't have rewriting rules for constructors, so we only must verify the condition ii.b of definition 4.  .
(1) t1/p=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 uR,iv.  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 uR,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 uR,i* u', vR,i* v' and  u'RCv'.  In our case this never happens since the axioms and theorems are not translated to conditional equations with inequalities.
c) For each l=r1,...,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 literals with negations.

Proposition 3.  Extensions to a set of ADTs are conservative or constructor-consistent
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.