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.