Pushout property

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

Dear friends,

after some period of debugging (both the static analysis tool
and the basic datataypes), the main six libraries
of the basic datatypes (including StructuredDatatypes) now
go through the full static analysis, including all
checks required by the static semantics.

During this process, the question arose is whether the check for the pushout
property is so useful. It has been included into the language
mainly because the referees wanted it.

Usually, the argument to include it is to derive
the amalgamation property. However, this fails in the
CASL institution.

Moreover, the check of the pushout property is very time-consuming
(the tool has become much slower since we have included the check).

Last but not least, some examples are ruled out.
Of course, many examples where actual parameter and
body share symbols can be saved through the import
mechanism. However, the pushout property requires more.
Indeed, in the basic datatypes, two instantations are not legal:

spec
     Int =
     ExtEuclidianRing [PreInt fit Elem |-> Int]
...
end

spec
     Rat =
     ExtField [PreRat fit Elem |-> Rat]
...
end

The idea with these examples is that the integers and the rationals
automatically should inherit all the derived operations for
euclidian rings (resp. fields).
In the first example, symbols with different profiles
(__*__:Elem*Int->Elem in an arbitrary Euclidian ring
and __*__:Int*Int->Int in PreInt) get equated. This
destroys the pushout property.
In the second example, dozens of profiles newly get into
the overloading relation, which again destroys the pushout property.

Since
  - nothing is gained,
  - tools get much slower, and
  - examples are ruled out,
  
I wonder if it would not be better to just delete the pushout
property. (In the semantics, just the condition would have to
be reomved, without any further effect.)
Perhaps the referees can tell in the light of these arguments
whether they still consider the pushout property to be important.

[BKB: why not make it optional as in some other cases?]

Greetings,
Till
-----------------------------------------------------------------------------
Till Mossakowski                Phone +49-421-218-4683, monday: +49-4252-1859
Dept. of Computer Science       Fax +49-421-218-3054
University of Bremen            till@informatik.uni-bremen.de         
 
P.O.Box 330440, D-28334 Bremen  http://www.informatik.uni-bremen.de/~till
-----------------------------------------------------------------------------