Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199304211204.AA02028@infix.cs.ruu.nl>
Subject: Announce: Lifted Pred. Calc. Library
To: info-hol@ted.cs.uidaho.edu (hol mailing list)
Date: Wed, 21 Apr 1993 14:04:42 +0100 (METDST)
Content-Type: text
Content-Length: 3399

Hi everyone,

There is a new library in the HOL contrib ftp-site, it is called
Predicate.


What the library provides, in short, are:

   (1) All logical operators ~, /\, \/, ==>, plus ! and ? are lifted
       to the predicate level. ie:
       
           p AND q = (\s. (p s) /\ (q s))

       etc.

   (2) Basic properties of the lifted operators.

   (3) Two tactics to automatically solve simple formula in the
       calculus of lifted operators.

   (4) Induction for finite predicates.

As for the motivation for the library:

Predicate calculus is supported by standard HOL. The negation, the
standard logical connectives, and the quantors ! and ? are all
defined and some of their basic properties are part of HOL built-in
features. There is even a tautology checker to automatically prove the
validity of a proposition calculus formula.

In programming people extensively make use of predicate calculus, or
at least people pretend they use predicate calculus. The primitive
concept in programming is predicate, which is a function from some
domain to BOOL. Predicate is used, for example, to describe a set
of states, for example those states where the value of variable z is
0.

If P and Q are predicates, the expression P AND Q cannot be a
formula in predicate calculus. The expression does not even make sense
since AND is a logical operator, so it expects Boolean arguments,
not predicates. Yet in programming, we pretend that the expression
does make sense and that it can be treated as a predicate calculus
formula.

What people has silently done is that they overload the symbol AND
to denote the point-wise lift of the logical AND. Indeed, the
lifted AND inherits all algebraic properties of the logical AND.
But this does not mean that they are semantically the same thing.

What is actually applied in programming is the predicate calculus
lifted to the predicate level. It is a calculus of predicates rather
than predicate calculus. Because the inference rules of predicate
calculus also applies to the lifted predicate calculus, people then
pretend that they work with predicate calculus instead.

When it comes to formalization however, we have to be very precise. So
an explicit distinction between logical operators and lifted logical
operators has to be made.

In the library called predicate we provide the lifted operators of
predicate calculus and their basic properties, including finite
predicates induction. The library basically provides the user with the
lifted predicate calculus, which is not yet supported by the standard
HOL.

Really, the library is not a big deal. Why, I even believe in fact
that every one who has been formalizing one programming logic or
another in HOL has ever written something like that. But that's just
the point, isn't it? There should be a common library for such, or
otherwise people will always end up with duplicating the same stuff.


How to Install
--------------

There is a LaTeX source called predicate.tex. You can compile it to
generate a nice documentation of the library. PRINT THE DOCUMENT
FIRST, you will find a direction of how to install there!

Or, if you are too lazy to do this, you should:

   (1) create a new subdirectory called predicate in your standard
       HOL library.
   (2) build the theory file by: make TPred
   (3) to load from HOL do: load_library `predicate`
   (4) that's it!


-Wishnu Prasetya-