Martin Baker <[email protected]> writes:
| On Monday 10 Oct 2011 20:32:32 Waldek Hebisch wrote:
| > Martin Baker wrote:
| > > On Monday 10 Oct 2011 17:54:47 Bill Page wrote:
| > > > What is unclear about macro? This is simple substitution. Or do you
| > > > mean the use of %false?
| > >
| > > Yes, I'm guessing from the context that %, when used as a prefix, is
| > > some sort of built-in function? but I don't know.
| >
| > % is just part of name, like letters. '%false (note the apostrophe)
| > is just a symbol with funny name.
|
| I still don't think I have all the information I need?
|
| In PropositionalFormula (in OpenAxiom - boolean.spad.pamphlet) the following
| macros are defined:
|
| macro FALSE == '%false
| macro TRUE == '%true
| macro NOT == '%not
| macro AND == '%and
| macro OR == '%or
| macro IMP == '%implies
| macro EQV == '%equiv
|
| These are used where SetCategory is expected but I can't find anywhere where
| '%not is defined as a SetCategory. So I'm guessing that, although '%not is
| theoretically no differerent from any other name, that '% may be some sort of
| escape code to indicate that its definition is built in?
First: Yes, those names are builtin.
Second: some background.
It is a stated goal of OpenAxiom to move beyond Lisp as its only runtime.
There is an ongoing project to integrate OpenAxiom to some popular proof
assistant systems, see the Calculemus 2011 paper
http://www.springerlink.com/content/d1t6326678385516/
As part of that project, among other things, we need:
-- to define precisely the semantics of Spad constructs
-- precise definition of compilation of Spad programs, which require
an intermediate language
-- to make Lisp systems redundant, e.g. we want to compile OpenAxiom to
the Poly/ML abstract machine.
Most the names you will find in OpenAxiom source code that start with %
are builtin. They are part of the intermediate language we compile to.
The translation of the intermediate language to Lisp is done in the file
src/interp/lisp-backend.boot
In this specific case of the use of these names in PropositionalFormula,
you will notice that they are just names of the kernel operators as
stated by the comment:
-- Local names for proposition logical operators
macro FALSE == '%false
macro TRUE == '%true
macro NOT == '%not
macro AND == '%and
macro OR == '%or
macro IMP == '%implies
macro EQV == '%equiv
They are used to build symolic expressions, for example:
conjunction(p,q) ==
per kernel(operator(AND, 2), [p, q], 1 + max(level p, level q))
Here, AND has not other meaning than being the internal name of the
logical conjunction operators. I kept the name close to the
intermediate language representation since they have similar (or exact)
semantics.
-- Gaby
------------------------------------------------------------------------------
All the data continuously generated in your IT infrastructure contains a
definitive record of customers, application performance, security
threats, fraudulent activity and more. Splunk takes this data and makes
sense of it. Business sense. IT sense. Common sense.
http://p.sf.net/sfu/splunk-d2d-oct
_______________________________________________
open-axiom-devel mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
