The people of this group mainly involved in this area are E.Astesiano and M.Cerioli (Contact person)

A very natural way of describing the data structures used by (any paradigm of) programming languages is using algebraic approaches.
Indeed, data structures consist of collections of data type elements and functions handling them, that should be their interface with the users, corresponding to the rigorous mathematical concept of algebra. Moreover using logical formulas the relevant properties of a data type can be captured, so that reasoning on its axiomatization allows to abstract from any implementative detail.
Although standard many-sorted algebras are a powerful tool to describe many simple data types, some features of very common data types are not easily and immediately represented by them, so that more sophisticated approaches have, and currently are, been investigated.
This group is mainly concerned with the following issues.

#### Partiality

Although each partial function can be represented as a total function on enriched domains, where a special element (bottom) has been added to represent the undefined, this coding usually does not respect the categorical structure of model classes and is not axiomatizable (in the general case).
Therefore, as many computable functions are inherently partial, in the late seventies the paradigm of partial algebras, that are simply algebras where operation symbols are interpreted by partial (= non necessarily total) functions, has been introduced. In the seminal papers on partiality, the form of logical formulas used to describe data types were restricted to the so called positive conditional axioms, because such formulas correspond to a natural coding of recursive definitions and guarantee the same properties used in total many-sorted approaches. But positive conditional axioms are too restrictive, for instance, to code extensionality. Hence if the data type to be axiomatized includes higher-order types, as it is the case for imperative languages with the usual model environment-store approach, where both environments and stores are functions and appear as argument in expression and code evaluation functions, such formulas are too poor.
A complete analyses of a richer logic for partial data types, called conditional, that is the minimal extension of the standard positive conditional approach able to express extensionality-like properties, has recently appeared in Free Objects and Equational Deduction for Partial Conditional Specifications.
Using the theory of partial conditional axioms, partial higher-order data types are fully investigated in Partial Higher-Order Specifications .
This group is currently involved in writing a chapter on partiality for the book Algebraic Foundation of Information Systems Specification (Hans-Joerg Kreowski, Bernd Krieg-Brueckner and Egidio Astesiano Editors), that will be the theoretical foundation for the semantics of the language proposed by the CoFI (Common Framework Initiative).

#### Non-strictness

A function from a domain A is called non-strict if it can yields a result on an input non belonging to A. There are basically two cases of non-strictness common in programming languages:
• don't care arguments, as for instance in the construct if_then_else_ where, depending on the value of the boolean switch, either branch can be erroneous without effecting the evaluation of the if_then_else, because the evaluation of the expression reduces to the evaluation of the other branch. Non-strict function of this kind are monotonic, in the sense that if a correct result is yielded on an incomplete input, then the same result is obtained whatever value is substituted for the missing input.
This kind of non-strictness is investigated in the (forthcoming) Non-strict don't care Algebras and Specifications.
• error recovery, for instance for finite implementations of theoretically unbounded data types, like integers or stacks, where some expression can be evaluated on a correct value even if some its sub-expression is a divergent calculation, as for example (maxint + n) - k, for some k>n, that could be evaluated as maxint + (n - k).
The main difference w.r.t. the previous case of non-strictness is that in this case the non-strict functions are not required to be monotonic.
The use of lazy-valuation techniques to define a new kind of algebras, called lazy indeed, is proposed in A Lazy Approach to Partial Algebras, and its applications are currently furtherly investigated.

 Please send suggestions and comments to: Last Updated: Maura Cerioli cerioli@disi.unige.it 29 April, 1996