Background

Declarative languages are widely considered as the theoretical and methodological basis for the definition of programming languages, suited to all the various applications of computing. Recently, the need for secure programming on the one hand and programming for supercomputing on the other hand, brought people to consider such languages as the only ones which can support good certified code and more, code that can be checked to fit into the various contexts in which mobile computing can be involved. Eventually declarative code is easily structured in closed parts (expressions) which can be computed separately on independent machines.

Interesting subjects to develop are:

• Since [Tarski-Givant 1987] introduced a calculus for complete first order logic without variables, till nowadays, much progress has been made and interesting results are obtained as far as combinatory calculus for logical and relational programming is concerned. We also, [Bellia and Occhiuto 1999], have defined one combinator for unification. It allows to deal with unification by means of abstracts of terms of first order formulas. It furnishes a linear reduction system for unification. Nevertheless logic programming (or, better logic languages) requires many more ad hoc mechanisms than those provided by first order logic: constraints, negation and also control mechanisms which are not logic. Hence the question arises on how to extend these combinatory theories to deal with such mechanisms [Broome and Lipton 1994].

• Another aspect of the definition of a combinatory calculus for declarative programming, is the definition of a calculus with (based on) supercombinators [Hughes 1982] which is able to reduce the huge [Broda and Damos 1997] dimension of the code (expressions) obtained using a fixed number of combinators. This is a fundamental problem if we want to:
  • use a combinatory code in mobile computing,
  • reduce the code fragmentation of independent parts in supercomputing.

  To study solutions, we started with studying techniques of parallel reduction for the mechanisms which are the kernel of declarative languages, such as unification or the substitution rule.

• Studying the theories, like monads, to understand if and to what extent they can furnish a suitable support to the integration of the logical and the functional features and as such provide mechanisms to deal with logical variables and higher order. Monad has been successfully developed to interface the functional paradigm with various frameworks: state, I/O, streams [Scholz 1999].