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  ₁,...,_n, where each _i is one of the following (or it's negation):
• t₁=t₂
• def(t)

• 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 t₁,t₂ whose interpretations in A are equal, we have that t₁=t₂ is valid in every model of spec. DMod(spec) denotes the class of all data models of spec.

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 u₁=v₁,...,u_n=v_n such that:
• l,r is composed with constructors and variables, and u_i,v_i is composed with constructors and constructor variables V^C
• Var(l)Var(r), and Var(u_i)Var(v_i)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)

R^CR^D

i) Let the sequence (_R^C,i)_iN of realtions on Term(sig,V^G) be defined by

a) _R^C,0=
b) t1_R^C,i+1t2 if there is a rewrite rule l=ru₁=v₁,...,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]_pand  (3)  u_kR^C,iv_kfor k=1,2,..n

Then _R^C = _iNR^C,i
ii) Let the sequence (_R,i)_iN of relations on Term(sig,V^G) be defined by

a) _R,0=_R^C
b) t1_R,i+1t2 if t1_R^Ct2 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,iv  (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'_R^Cv'

Then _R = _iNR,i

a) R=R^CR^D, where R^C is a set of constructors rules and R^D is a set of defining rules
b) _R is confluent
c) For each l=r₁,...,_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₁,t₂Term(sig,V^G).  Then t_1R,i* t₂ if and only if DMod(spec)t₁=t₂.
 
 

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₁,A₂,...A_n}, let S be the set of names of ADTs {name(A₁),name(A₂),...,name(A_n)], F is the set that contains the name of all functions F=functions(A₁)  functions(A₂) ....  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₁)  axioms(A₁)...axioms(A₁).
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 {v₁,v₂...,v_k} and def(Var(L)) donotes def(v₁),def(v₂),...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)

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
(ADD)=NAT 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)
...
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)
                  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)

a) R=R^CR^D, where R^C is a set of constructors rules and R^D 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=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,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 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'_R^Cv'.  In our case this never happens since the axioms and theorems are not translated to conditional equations with inequalities.

c) For each l=r₁,...,_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.
 
 

Operational Semantics Translational Semanticst