Re: Tentative Language Design Summary version 0.93

[till@informatik.uni-bremen.de (Till Mossakowski)]

Dear Andrzej, dear other X-people,

>well-formedness of terms and formulae must depend on the context, for
>instance, adapting an example from the note, a = b is well formed
>under the declarations:
>	sorts s1, s2 < s
>	const a: s1, b:s2
>but is no longer well-formed if we add a declaration
>	sort s' > s1, s2
>because of the possibility of ambiguous parsing, which may lead to
>different semantics.
>
>I'm afraid that examples like this bother me a bit (the need to
>consider this particular equation as ill-formed is linked to the fact
>that arbitrary injections are allowed as a semantical counterpart of
>subsorting relation, rather than for instance just inclusions --- the
>latter would lead to the identification of overloaded symbols with
>connected profiles, rather than with ordered by subsorting profiles,
>as now). Anyway, I think I am prepared to live with this (and explain
>this if necessary).

I have nothing to add to Maura's answer to a similar question:
>This is already true, even without subsorting. Indeed, consider the
>following example
>  Let SIG'1 = sorts s1, s, opns c : s1, f: s1-->s
>      SIG'2 = SIG'1 + sorts s2 opns f: s1-->s2
>Then f(c) is well formed, of sort s in Sig'1, but it is ill-formed in
>SIG'2, as it can represent both (f: s1-->s)(c:s1) and (f: s1-->s2)(c:s1)
>for instance if we use this term in a definedness predicate.
>Therefore, I don't think that we should worry for this problem in the
>subsorting context.

NB. The inclusion vs. injection question can be treated entirely
orthogonal to the question which profiles should be identified.
 
>At a more technical level, it feels very bad to me that definedness,
>equalities and predicates "do not commute with subsort injections".
>This makes some specifications look very misleading. For instance, it
>bothers me that a specification like:
>	enrich ( sort s, const a:s, axiom not D(a) )
>	by sort s' > s, axiom D(a)
>is consistent! I believe that this might also be very misleading to
>the "average" user.
As Peter said, everything now commutes with the subsort injections,
and weak monotonicity is deferred to an extension.
But even in the extension with weak monotonicity, the above
specification would be inconsistent, only the following would
be consistent:
	enrich ( sort s, const a:s, axiom not D(a) )
	by sort s' > s, const a:s', axiom D(a)


>Aha, two small issues around here:
>First, I do not like the use of the same symbol cast for subsort
>injections and projections. It seems to introduce more ambiguity than
>necessary into terms. For instance, given
>	sorts s1 < s2 < s3
>	const a: s1
>cast a s2 may intuitively mean either cast (cast (a qua s1) s3) s2 or
>simply cast (a qua s1) s2. I guess this is somehow prevented by a
>condition restricting projection and injection casts occuring next to
>each other. Since we treat projections and injection quite
>differently, I suggest the use of two different symbols here.

We will change this.

>And then, I guess I am missing some technicality here, but I do not
>like the restriction which seems to prevent an appropriate injection
>cast to be inserted before the use of qua. At least for me, this
>would be a typical use of sort assertions, to implicitly invoke a
>subsort inclusion.

The technical point behind this was the need of disambiguous
axioms, which is now achieved by the possibility to qualify
function symbols by explicit profiles.
We now have forbidden silent injections AROUND quas, because
the specified sort of a term should not be overridden. 

>Aha: and I can see no additional harm in allowing declarations of the
>subsorting relations (they would be declarations, not axioms!) to be
>separated from the declarations of the sorts themselves.

This is already allowed in the study note (but in 0.93 not yet).

[I'm waiting with preparing the next version of the language design
summary until after the new version of the study note on subsorting
becomes available. --PDM]

Greetings,
Till