Re: [TYPES] Declarative vs imperative

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


Hi,

Here is a another conception of the notion "declarative" logic and its
difference with imperative languages.
	
	This chair has three legs
	It is nice to sit in it.
	All students attended the lecture this morning.
	Each lecture takes place in exactly one room
	...

They are declarative sentences, pieces of information. They are not
commands, not procedures, not descriptions  of problems.

In this view, a theory in a declarative logic is  a bag of
information. It  is not a command, not a program.  It is not
even a representation of a computational problem.
Consequently, a theory does not "do" anything. It cannot be executed.
It has no solutions.  It provides information, and that is it.

That does not mean that it cannot be useful. In the first place, it can
be used by human experts to communicate information about a domain,
in the same way as currently a UML domain specification is used. It is
like a UML domain specification, but in a formal logic. In the second
place, this information can be used to solve problems, see below.

In this conception,  logic is a clear and precise formal language to
express information. The role of model theory is to give a formal
account of the information content of expressions of the declarative
language.

There is no inherent form of inference to such a logic. Therefore,
theories in such a logic are not representations of problems.

However, the information in a theory can be used to solve
computational problems or perform tasks, by applying suitable forms of
inference. In fact, it may be possible to use the same
theory, the same information,  to solve many types of problems, by
application of DIFFERENT forms of inference.
For example, a theory of a scheduling domain can be used for the task of
checking the correctness of a given schedule (by model checking),
but also of generating schedules (by model generation).


This conception of logic differs from the view in almost every
area of computational logic. Computational "declarative" logics such as
logic programming (e.g. prolog), functional programming languages (e.g.
Haskell), query languages (e.g. SQL), deductive database
languages, Answer set programming, abductive logic programming,
description logics, temporal logics, constraint logic programming,
"deductive" logic, ...: they  have in common that the language is
associated to a unique "inherent" form of inference. They  are
"uni-inferential". This has advantages and disadvantages. In any case,
it invites  human experts to view a theory as a description of a
computational problem (to be solved by applying the inherent form of
inference).

In some cases, like in Prolog  or Haskell, when not only the type of
inference but also its implementation is specified together with the
logic, a (unique) operational semantics is imposed on the language. From
then on, theories can be viewed as procedural programs. E.g., under
SLDNF resolution, Prolog "theories"  can be understood as a sort of
procedural programs (Kowalski's procedural interpretation)  with
non-common procedural features such as backtracking and unification.

We see that   by imposing a unique form of inference and, next, by
imposing an implementation of that inference, "declarative" languages
gradually shift  in the direction of procedural languages. I think that
this is the reason why the notion of "declarative language" and the
difference with imperative langauges has become so blurred.

On the other hand, if no inherent form of inference is attached to the
logic, a theory cannot be viewed as a problem and certainly not as a
program. It is a specification, a bag of information and not more than that.

This does not mean that declarative logic as defined above is not useful
for computational purposes. Quite on the contrary. The above conception
of logic suggests to build Knowledge Base Systems: multi-inference
engines that support different forms of inference on the same theories
(the "knowledge base"). So, perhaps surprisingly, logics without
inherent form of inference are actually "multi-inferential".  This view
of logic and of computing with logic was called the "Knowledge Base
System paradigm" by me and Joost Vennekens in  a position paper at
ICLP2008.

The research project of my group is to build a KBS system called IDP,
for a "declarative" language in the above sense. This language (FO(.))
is a rich extension of classical logic. An example of the knowledge
base paradigm in operation can be seen in a propotype interactive
configuration tool  built with IDP and available at

http://dtai.cs.kuleuven.be/krr/software (See KB-System demo)

This tool supports 5 different forms of inference on the same theory to
support different functionalities for the user: model checking,
propagation, model generation/expansion, model generation with
optimisation, explanation. In this application, the computations to be
performed are not computationally hard, but what counts is the
principle. This system displays a unique form of reuse of the
theory that is excluded in principle in procedural languages and
uni-inferential declarative programming paradigms. Here the conceptual
difference between a declarative theory  and a program is clear-cut.

About imperative and procedural languages

A program in an imperative language can be viewed as a (compound)
command to the computer but it also contains a precise description of
computer processes (the operational semantics). As such, I do not think
there is an important difference between imperative and procedural
languages.

It also means that C, C++, Java programs,... decaratively describe
something: namely these computer processes. In this respect, these
languages can be seen as process logics. So, for me  C is indeed a
declarative logic.

However, it is obviously a very different logic than say classical
logic. One aspect is related to "universality": C++ can only describe a
very restricted class of (computer executable) processes. Classical
logic can be used (although not so conveniently)
to describe such processes as well (e.g., using some
methodology for temperal knowledge representation such as situation or
event calculus).
But Classical logic can also be used to describe other domains :
temporal or non-temporal. E.g., to describe the theory of groups, or
the theory of correct university programs. C++ can not be used for that,
simply because what is described in such a theory are not computer
processes. So C++ is a domain specific logic with a very narrow domain.

Another difference is that C++, seen as a declarative process logic,
is (currently) associated with a unique form of inference:  "execution
inference" of the computer process.


Marc Denecker


-- 

   Marc Denecker (prof)
   KU Leuven   			
   Departement Computerwetenschappen    tel: ++32 (0)16/32.75.57
   Celestijnenlaan 200A Room A02.145    fax: ++32 (0)16/32.79.96
   B-3001 Heverlee, Belgium
   email: [email protected]
   http://people.cs.kuleuven.be/~marc.denecker/
 ........................................................................

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm