(not quite) dissenting views

[Bernd Krieg-Brueckner <bkb@informatik.uni-bremen.de>]

ATTRIBUTION has been *too hastily* removed
------------------------------------------
Bernd Krieg-Brueckner, Till Mossakowski

Proposed change
---------------
reinstate as in previous version, or at least reintroduce as a kind of axiom.

Discussion
----------
In order not to have too many special features, it would be nice to be able
to express things as much as possible within CASL itself, even if only in
extensions of CASL.
ATTRIBUTION for a single argument can be expressed as a predicate, once we
have type parameters (or polymorphism), for a list of arguments once we
have higher-order (this is actually an example we have studied).
In (first-order) CASL, one could even require an explicit type argument, in
which case qualification is unnecessary, e.g.
   Monoid (Nat, o, +), ACI (Nat, [+, *])

Methodology:
It is often a good idea to split properties, e.g. to have a list of
functions that share the ACI property, but state the Monoid property (with
the unit element) separately for each function (cf. CSP example in my
syntax proposal).

Tools:
The argument about tools goes both ways: some tools (e.g. rewriting
engines) need the information that a function is AC, say, but others (some
provers) need the reps. axioms expanded. So why not stick to the previous
solution: ATTRIBUTION is like an axiom, it is recognisable for special
tools, but it can also be considered as an abbreviation, even instantiation
of a predefined / built-in (HO) predicate.

Generality:
why only for a FUN-DECL and not a FUN-DEFN?

Alternative
-----------
To associate properties in declarations, it would be much better to
associate them with the function type rather than the declaration itslef;
this is a general principle when one has extension to higher-order in mind:
then one can also state such properties on functional arguments, e.g. the
Monoid property on the argument for a fold operation on lists.

In my syntax proposal I have experimentally associated the properties to
the function arrows (note: both!), e.g.
   +, * : Nat >< Nat ->ŽAC Nat
These arrows are definable in extensions.

Alternatively, one could (pre)define the properties as parameterised types;
then they would also comprise the constraints for only two arguments of the
same type, etc., e.g.
   +: Monoid(Nat, 0)
   +, *: AC(Nat)

-----------------------------------------------------------------------------

FUN-DEFNs should be partial *and total*
---------------------------------------
Bernd Krieg-Brueckner, Till Mossakowski

Proposed change
---------------

FUN-DEFN	::= fun-defn FUN-NAME FUN-TYPE TERM
SORTS		::= sorts SORT*
		|   parameters VAR-DECL+

Discussion
----------
I do not see any reason for *only* having *partial* functions, especially
for constants [for which they were mainly introduced, I guess].
In fact, as FUN-DEFNs will (and should) be *used*, the emphasis is wrong
here; methodologically (I thought that was agreed?), we want to encourage
the use of *total* functions, among other things with the use of subsorts.

The proposed solution is more uniform (to may taste anyway) and will allow
for the (planned) extension of dependent types and possibly named tuples.

I see no problems in just ignoring the parameter names if they are not
needed; also, parameter names are not always necessary, e.g. in
   const2: Nat -> Nat = 2

Equational Definitions
----------------------
As a PS: I think that FUN-DEFNs *really* make sense when there is a
possibility for complete conditional equational definitions (on the
"right-hand side");
see my syntax proposal.
All these are just syntactic extensions; no problems or changes for the
semantics foreseen.


___________________________________________________________________
Prof. Dr. Bernd Krieg-Brueckner    courier mail only:
FB3 Mathematik und Informatik      MZH 8071, FB3
Universitaet Bremen                Universitaet Bremen
Postfach 330 440                   Bibliothekstr. 1
D-28334 Bremen                     D-28359 Bremen

Telefon: (+49) 421-218-3660        telefax: (+49) 421-218-3054
bkb@Informatik.Uni-Bremen.DE       privat:  (+49) 421-25-1024
http://www.informatik.uni-bremen.de/~bkb/