[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Semantics of free datatype in presence of subsorting.
Dear all,
we (Anne and Maura) need some help/clarification in order to complete the
semantics of subsorting, as we have a doubt about the intended semantics of
free datatypes in presence of subsorting.
Indeed, the axioms given to impose the "freeness" (ie dijointness for the
image of distinct constructors, including the embedding of subsorts used as
alternative) are somehow incompatible with the treatment of overloaded
functions on sub/supersorts.
A first attempt at producing a rule for the free datatype, is to modify the
rule by Don adding
- the condition about no common subsorts
- the axioms requiring images of distinct embedding (or embedding
and constructors) to be disjoint:
Sigma |- DATATYPE-ITEMS |> (Delta,Delta',Psi)
S'' = S \cup S'
(S,TF,PF,P,<,==) = Sigma
(S',TF',emptyset,P',<',==') = Delta
s' RT(< U <') s1 and s1 <' s |
and | ==> s1=s2
s' RT(< U <') s2 and s2 <' s |
-------------------------------------------------------------------
\Sigma |- free-datatype DATATYPE-ITEMS |>
(Delta U Delta',
Psi
U {injective{f_{w,s}} |
w in S''*,
s in S'',
f in TF'_{w,s}
U A U B U C
U {(S',complete{TF' U INJ})} (for INJ the family of
all the embedding.)
where
A = {disjoint{f_{w,s}}{g_{w',s}} |
w,w' in S''*,
s in S'',
f in TF'_{w,s},
g in TF'_{w',s},
f_{w,s}=/=g_{w',s}\}
B = {disjoint{f_{w,s'}}{Emb(s->s')} |
w in S''*,
s,s' in S'',
f in TF'_{w,s},
s RT(<') s'}
C = {disjoint{Emb(s0->s)}{Emb(s1->s)} \\
w in S''*,
s,s0=/=s1 in S'',
s0 RT(<') s,s1 RT(<') s}
With this semantics, that is the immediate adaptation of the "flat" case, we
can see 3 problematic cases, producing syntactically correct, but unexpectedly
inconsistent (or simply weird), specifications:
(do not mind the concrete syntax, that's probably incorrect, but hopefully understandable)
1 Overloaded constructors
free datatype s = f(s1)|f(s2)
where s1 and s2 have a common subsort s0
2 Interaction between embedding
free datatype s = s1 | s2
where s1 and s2 have no common subsort, but for which a term t
exists with both sorts. The simplest (and most useless) case
is if a constant k exists for both sorts (but in general it applies
to functions f:w --> s1, f: w' --> s2 with a common w0<w and w0<w')
3 Interaction of embedding and constructor
free datatype s = f(s1) | s2
where there is also the declaration
total function f: s1 --> s2;
(or f:s0 --> s3 with s0<s1 and s3<s2....)
In all the above cases the disjointness axioms together with the implicit
axioms for overloading, make the specification inconsistent (or introduces
unexected identifications, see the example below).
In our opinion this is not intended.
Thus the first doubt is "what exactly do we want to have as semantics in this case?"
In case your answer is "we expect that the axioms for disjointness apply to
all cases *but* those identifications forced by the overloading", there is a
second problem. How can we express this intuition.
Let us distinguish the problems (same numeration as before)
1 Overloaded constructors
- a first possibility is to forbidd overloading of constructors (at
least with a commond subsort for their domains)
- otherwise we can distinguish two cases for constructors:
a. when two constructors are *not* in overloading relation:
the disjointness axiom should hold
b. when two constructors are in overloading relation: they must only give
the same for values which can be embedded from the same value
Therefore instead of the set of axioms A, we give A1 U A2, with
A1 = {disjoint{f_{w,s}}{g_{w',s}} |
w,w' in S''*,
s in S'',
f in TF'_{w,s},
g in TF'_{w',s},
f_{w,s}~/~g_{w',s}} (~ is the overloading rel)
A2 = {relaxed-disjoint{f_{w,s}}{f_{w',s}} |
w,w' in S''*,
s in S'',
f in TF'_{w,s},
g in TF'_{w',s},
f_{w,s}~f_{w',s}}
where relaxed-disjoint is something like the following
for all x1: s1...xn: sn...y1: s'1..yn: s'n
if f(x1,...xn)=g(y1...yn)
then there exist s"i< si' and s"i<si and zi:s"i s.t.
xi=Emb(s"i->si)(zi) and yi=Emb(s"i->s'i)(zi)
(for the problem with quantifications over sorts and functions,
see at the end, marked by a ***)
2 Interaction between embedding
Replace in the set C disjoint by disjoint-as-much-as-possible,
where disjoint-as-much-as-possible for embedding s'<'s
and s"<'s with s'<>s" is something like the following
for all x:s', y:s"
if Emb(s'->s)(x) = Emb(s"->s)(y)
then there exist f: s'1...s'n -->k' and f: s"1..s"n -->k",
with k'<s' and k"< s", and si<s'i, si<s"i in the overall signature s.t
there exist zi:si s.t.
x=Emb(k'->s')(f(Emb(s1->s'1)(z1)...Emb(sn->s'n)(zn)) and
y=Emb(k"->s")(f(Emb(s1->s"1)(z1)...Emb(sn->s"n)(zn))
3 Interaction of embedding and constructor
Replace in the set B disjoint by distinct-as-much-as-possible,
where distinct-as-much-as-possible for each embedding s'<'s and
each constructor f: s1..sn -->s in TF' is something like the following
for all x1: s1...xn: sn, x:s'
if Emb(s'->s)(x) = f(x1,...xn)
then there exist f: s'1...s'n -->k', with k'<s', and
s"i< si' and s"i<si and zi:s"i s.t.
there exist zi:si s.t.
x=Emb(k'->s')(f(Emb(s"1->s'1)(z1)...Emb(s"n->s'n)(zn))
*** Quantification over sorts and function is a meta-shortcut for the
disjunction of all the functions in the signature with the correct name/profile...
Thus, for instance for the fragment
sorts s1, s2, s3, s0 <s1, s0< s2
function f: s0 --> s2
f: s1 --> s0
f: s3 --> s0
const a:s1
a:s2
free datatype s=s1 |s2
disjoint-as-much-as-possible(Emb(s1,s),Emb(s2,s)) is
for all x:s1, y:s2
if Emb(s1,s)(x) = Emb(s2,s)(y)
then
(there exist z:s0 s.t.
x=Emb(s0->s1)(f_{s1,s0}(Emb(s0->s1)(z)) and
y=Emb(s0->s2)(f_{s1,s0}(Emb(s0->s1)(z))))
or (there exist z:s0 s.t.
x=Emb(s0->s1)(f_{s1,s0}(Emb(s0->s1)(z)) and
y=f_{s0,s2}(z))
or (x=a and y=a)
That's to give a rough idea of how to covert the meat-axioms from a readable
to a correct form.
BUT
---
Since we have linear visibility, if I change the order of the elements of the
fragment in
function f: s0 --> s2
f: s1 --> s0
f: s3 --> s0
free datatype s=s1 |s2
const a:s1
a:s2
Then
disjoint-as-much-as-possible(Emb(s1,s),Emb(s2,s)) is
for all x:s1, y:s2
if Emb(s1,s)(x) = Emb(s2,s)(y)
then
(there exist z:s0 s.t.
x=Emb(s0->s1)(f_{s1,s0}(Emb(s0->s1)(z)) and
y=Emb(s0->s2)(f_{s1,s0}(Emb(s0->s1)(z))))
or (there exist z:s0 s.t.
x=Emb(s0->s1)(f_{s1,s0}(Emb(s0->s1)(z)) and
y=f_{s0,s2}(z))
and the axiom Emb(s1,s)(a:s1) = Emb(s2,s)(a:s2), introduced by the double
declaration of the constant a, entails
there exist z:s0 s.t.
a:s1=Emb(s0->s1)(f_{s1,s0}(Emb(s0->s1)(z)) and
a:s2=Emb(s0->s2)(f_{s1,s0}(Emb(s0->s1)(z)))
or (there exist z:s0 s.t.
a:s1=Emb(s0->s1)(f_{s1,s0}(Emb(s0->s1)(z)) and
a:s2=f_{s0,s2}(z))
that's weird
(if the functions f do not exist at all, then the spec becomes inconsistent)
This last problem could be avoided going back to the non-linar visibility
semantics (but we do not want to change yet another time, we suppose) or using
a two steps approach (in the first we collect the elements of the signature,
in the second one the axioms).
Conclusion
----------
Please let us know what's your intuition about the "expected" semantics and we
will do our best to implement it ;-)
Best Regards
Anne and Maura
(PS I'm sending this message now, as we are late, though Anne didn't have the
possibility to check the last example. So any error in it is my complete
responsability. Maura)