HGKM Manual

Authors:: Richard Weyhrauch (IBUKI), Carolyn Talcott
Note:: The information in this document (and its companion documents) is the confidential proprietary property of IBUKI. It contains trade secret, published and unpublished components. All IBUKI systems (appearing under various names) have been developed over a substantial period of time at IBUKI's expense.

Abstract

This manual describes HGKM (which is shorter than (Herbrand, Godel, Kleene and McCarthy), a simple Turing complete programming language designed to have a clean First order semantics. It was first desigmed by Richard Weyhrauch and Carolyn Tallcot and first implemented at Stanford Artificial Intelligence Laboratory at Stanford. A second extended version was developed by the GTTFOL project under the direction of Fausto Giunchiglia. The version documented here has been reimplemented by IBUKI.

1. Introduction
2. Description of HGKM
3. Examples of Data Machines
4. Examples of Code
5. Conclusion
References
Acknowledgments

1 Introdction


{\bf Table of Contents}

{\bf Introduction}
{\bf Interactive use of the system}
{\bf Data Structures}
    {\bf Symbols}
    {\bf Booleans}
    {\bf Numbers}
        {\bf Characters}
    {\bf Strings}
    {\bf Pairs}
    {\bf Lists}
{\bf Evaluating Forms}
    {\bf Nop: <nop>}
    {\bf Symbols: <symbol>}
    {\bf Quote: <quote>}
    {\bf Application: <appl>}
    {\bf Conditional expressions: <if>}
    {\bf Let: <let>}
    {\bf Sequences of forms: <seq>}
    {\bf Set: <set>}
    {\bf Programs: <pgm>}
    {\bf Special functions}
{\bf Defining Functions and Predicates}
    {\bf Functions}
    {\bf Predicates}
{\bf Reading and Printing}
{\bf Error handling}
{\bf Debugging}
{\bf Bibliography}
{\bf Index}
{\bf Appendix: FOL}
{\bf Appendix: Useful functions}

Introduction

This is a reference manual for HGKM. It interactive version uses the notations of [sexpression]s.

Interactive use of HGKM

Data

HGKM, like all IBUKI Systems, inherits its data from IBUKI Data as described in IBUKI Data. This [data] available in all IBUKI systems. In this document we describe its use in HGKM. It also describes the relations, functions and recognizers that HGKM uses to operate on them. These descriptions have the following form.

First we describe their reader syntax. This is the printed representation that is used by the reader to construct the [data]. This is folllowed by a description of the operations on this [data]. It has the following form:

( <operation-name> <arg-1> ... <arg-n> )  ==>  <type-name>    <operation-type>

This is of the form

 [form] ==> [value-type]   [operation-type]

After the syntax description is a paragraph describing the operaton and sometimes givng some examples.

Examples are further indented like this sentence.

Each operation is either of type [function], [recognizer], [predicate or [action]. The name of the operation is the symbol <operation-name>. The discription of the operation follows immediately after it. In SEUS [form]s can take a different number of values so we do not always describe specify the number of [form]s that are in the argument position of an operaation, but we do specify the number and types of the values that the command must evaluate to. Thus

    [int]

means that the value is an [integer]. If an operation returns more than one valu of a single type, each [type-name] will have a number appended. For example we write

   [str1] [str2]

when we want to say that a form eveluates to two string values. In the case an operation does not care about the type of its value we write

   [obj]

to indicate a value that can be any object. It is an errpr if the arguments of a form are of the wrong type. A SEUS function cannot return a value of the wrong type. What happens when an error occurs is described in section ????.

Thus we write

 (pair-mak [obj1] [obj2] )  ==>  [pair]                  function

when we mean that 'pair-mak' takes exactly two arguments and that they may be arbitarary objects and the eveauation of this form applied the function 'pair-mak' to its argiments and returns exactly one value of type [pair].

The following predicate is defined for all data structures.

   (EQUAL [obj1] [obj2] )                                predicate

This evaluates to $TRUE if and only if both obj1 and obj2 are the 'same' object, $FALSE otherwise. We write 'same' in quotes because the notion od same is a predicate and depend on the [context] that can make that decision. For SEUS, 'same' is defined in the [context] ...


    {\bf Symbols}

<symbol> := <identifier>

Each identifier determines a symbol.  Examples of symbols are: 

abc, CAR, NIL, THISISALONGATOM.  

NOTE: SEUS symbols are case sensitive.  


(SYMBOL? [obj] )predicate

TRUE if obj is a symbol
FALSE otherwise


(SYM:SET:VAL [sym obj] )      action

SYM:SET:VAL changes the value associated with the specified symbol 
to obj. It produces a side effects and it does not return a
        value.

(SYM:GET:VAL [sym] )  ==>  [obj1 ... objn]         pfn 

SYM:GET:VAL returns the values associated with the specified symbol.
Remember symbols may have no values.

(SYM:SET:PROP [sym obj1 obj2 ... objn] )      action

SYM:SET:PROP makes [obj2 ... objn] the values associated with the 
property obj1 for the symbol sym.

(SYM:GET:PROP [sym obj1] )  ==>  [obj2 ... objn]         pfn

 SYM:GET:PROP returns the values (obj2 ... objn] of the ``obj1'' 
        property of sym.  

(SYM2CHR [sym] )          pfn

SYM2CHR returns a list of characters which appear in the print 
name of the symbol.

Example:

(SYM2CHR (QUOTE APPLE)) ==> (65 120 120 114 105)

    {\bf Boolean predicates}


<bool>:= TRUE | FALSE

TRUE and FALSE mane the truth values true and false respectively.

(NOT X)predicate

(AND X Y)predicate

(OR X Y)predicate

(IFF X Y)predicate

(IMP X Y)predicate



    {\bf Boolean functions}


<bval>:= TVAL | FVAL

TVAL and FVAL represent the truth values for functions. We introduce
them to distinguish between predicates that return TRUE and FALSE and
functions.

(IST [obj] )function

TRUE if obj is not FVAL
FALSE if obj is FVAL

(ISF [obj] ) function

TRUE if obj is FVAL
FALSE otherwise

    {\bf Numbers}

The only numbers SEUS supports at present is small integers.  The syntax of 
integer is:

<integer>  :=   <digits> | <sign> <digits> 
<digits>   :=   <digit> | <digit> <digits>
<digit>    :=   0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
<sign>     :=   -

In SEUS there are only integer numbers.

(INTEGER? [obj] ) predicate

TRUE if obj is an integer
FALSE otherwise

(ZERO? [obj] ) predicate

TRUE if obj is zero 
FALSE otherwise

(NATNUM? [int] )predicate

TRUE if integer is a natural number
FALSE otherwise

(MINUS? [int] )predicate

TRUE if the integer is negative
FALSE otherwise

(LE [int1] [int2] )predicate

TRUE if integer1 is less or equal integer2
FALSE otherwise

(GE [int1] [int2] )predicate

TRUE if integer1 is greater or equal integer2
FALSE otherwise

(GT [int1] [int2] )predicate

TRUE if integer1 is greater than integer2
FALSE otherwise

(LT [int1] [int2] )predicate

TRUE if integer1 is less than integer2
FALSE otherwise

Functions (* X and Y stand for integers *):

(MINUS X)= -X

(PLUS X Y)= X + Y

(DIF X Y)= X - Y

(TIMES X Y)= X * Y

(QUO X Y)= X / Y

(REMAINDER X Y) is  X - (X / Y) * Y

(DIVIDE X Y)= (CONS (QUOTIENT X Y) (REMAINDER X Y))

(ADD1 X)= X + 1 

(SUB1 X)= X - 1

        {\bf Characters: <chr>}

<character> :=  <ascii character>

In SEUS we use small integers to represent ascii characters.

(ASCII? [obj] )          recognizer

obj  if obj is a character
[]   otherwise


(CHR2SYM [chr1 ... chrn] ) ==>[sym]                                 pfn

CHR2SYM return the symbol whose print name contains the      
characters as the string.

Example:

(CHR2SYM 65 120 120 114 105)  ==>  APPLE


CHR2SYM is the logical inverse of SYM2CHR, i.e.,

(CHR2SYM (SYM2CHR <sym> ))      = <sym>
(SYM2CHR (CHR2SYM <chrs> ))     = <chrs>

    {\bf Strings: <str>}

<string> := "<any sequence of characters not containing " >"

A string is an arbitrary sequence of characters surrounded by 
double quotes and not containing double quotes.
They have print names that actually include the double quotes
surrounding them.

Examples:"I AM A STRING"

(STRING? [obj] ) predicate

TRUE if obj a string
FALSE otherwise

(SUBSTR [str1] [str2] )predicate

TRUE if str1 is a substring of str2
FALSE otherwise

(SETSTR [str] [int] [chr] )function

SETSTR defines a string and gives it ????

(GETSTR [str] [chr] )function

GETSTR ????

(CAT [str1] [str2] )function

CAT returns a string which is obtained by concatenating
string1 and string2 (eliminating extra " ??)

(LENSTR [str] )function

LENSTR returns an integer equal to the number of 
characters in string.

(SUBSTR [str] [int] )function

returns a string of length integer whose characters 
appear in the first integerth places in string.
If (GT (LENSTR string) integer) then ????


    {\bf Pairs}

<pair>   :=  ( <obj> . <obj> )

SEUS uses CONS, CAR, CDR, ... for operations on pairs.  We use
the usual LISP convention C...R.

(PAIR? [obj] ) predicate

TRUE if obj a pair
FALSE otherwise

(ATOMIC? X)predicate

TRUE if obj is not a pair.
FALSE otherwise

(CONS [obj1] [obj2] )function

returns a pair of obj1 and obj2

(CAR [pair] )function

returns the first element of the pair

(CDR [pair] )function

returns the second element of the pair

(SETCAR	[pair] [obj] )function

changes the first element of the pair to obj. It produces
side effects and it does not return any reliable value

(SETCDR[pair] [obj] )function

changes the second element of the pair to obj. It produces
side effects and it does not return any reliable value



    {\bf Lists}

<list>:=  ()  | ( {<obj>} )

A list either the empty list or a pair whose second element is 
a list.  MTL is the constant whose value is the empty list it 
is represented by (). 

Example: (CONS 3 MTL) is the list ( 3 )

??? Do we need to define the value of applying CAR CDR SETCAR 
??? SETCDR to the empty list ?

(MTL? [obj] ) predicate

TRUE if X is a list and is empty
FALSE if X is a non-empty list


(LIST [obj1] ... [objn] ) function

returns a list of the n arguments

(FIRST [list] )function 

(REST [list] )function

(SECOND [list] )function

(LAST [list] ) function

(NTH [int] [list] )function

returns the element at positive integer position of the list.
If it does not exist ???

(LENGTH [list] )function

returns the number of elements of the list

{\bf Evaluating Forms}

This section describes how <form>s are evaluated by the interpreter.

It is the responsibility of the top level of the SEUS system to evaluate
read <form>s, find their value and to report the value as well as to do
whatever side effects are specified.   Thus a <form> is an SEUS program.
The different types of <form>s are:

<nop> | <symbols> | <quote> | <appl> | <if> | <let> | <set> | <seq> | <pgm>

Their description is in the next subsections which contain the syntax
and the semantics of each type of form.

    {\bf Nop: <nop>}

(NOP)

Is a form whose evaluation does nothing.

    {\bf Variables: <var>}

    A <var> form is simply a symbol in which case the result of the
    evaluation of the form is its value in the current envirionmeent.

    Examples:

    (a.b) be the value of symbol X if (a.b) is the value
    associated with X

    {\bf Quote <quote>}

(QUOTE <form> )

The evaluation of <quote> returns <form>

    {\bf Application: <appl>}

( <applname> <arg1> ... <argn> )

The <name> of the application must be a symbol with associated
a function or a predicate. It can be a constant or built-in symbol
or a user-defined symbol (see Section Defining Functions
and Predicates).
The <argi>s are forms that are evaluated and bound to the corresponding
arguments of the function or predicate (call-by-value).
The result of the application
is the value obtained applying the function or the predicate to
its arguments.

??? Do we say anything about the number of arguments ???

Examples:

(CONS 1 13) evaluates to (1.13)
(MTL? MTL) evaluates to TRUE

    {\bf Conditional expressions: <if>}


(IF <test> <then> <else> )

The <test> must evaluate to a truth value.  If its value is 
TRUE then the value of the <if> is the value of the form 
<then>, otherwise it is the value of the form <else>.  

(IFN <test> <then> <else> )

IFN stands for IF NOT.

Examples:

(IF (MTL? X) FALSE TRUE) 

evaluates to FALSE if X evaluates
to an empty list TRUE otherwise

    {\bf Sequences of forms: <seq>}

(SEQ <form-1> ... <form-n> ).

A SEQ <form>  allows you to write sequences of <form>s
instead of only applicative expressions.  The value of a SEQ 
<form> is the value of its last form <formn>.


    {\bf Setb: <setb>}

(SETB <blist> <forms> )

SETB binds the value of <form> to the variable <var>.
It is an operation defined on environments, in the
global environment it is equivalent to 
(SETVAL (QUOTE <var>) <form>) because we represent
variables as symbols. It produces
side effects and does not return any reliable value.

Examples:

(SEQ 
                  (SETVAL (QUOTE X) 1)
                  (LET (X 5) (SEQ (SET X 3) X)))  )

		  evaluates to 3 and leaves the value of X to be 1

		  (SEQ 
		    (SETVAL (QUOTE X) 1)
		              (LET (X 5)
			          (SEQ (SETVAL (QUOTE X) 3) X))))

				  evaluates to 5 and leaves the value of X to be 3

    {\bf Let <let>}

(LET ( (var-1 <form-1>) ... (var-n <form-n>) ) <body>)

LET is used to create and initialize local variables.  

The result of evaluating a LET is given by
the evaluation of the form <body> in a new environment
which associates with the var-is the values 
obtained by the evaluation of the respective <form-i>s.
The <form-i>s do not contain any reference to var-is.

The semantics of LET is the same as

( (LAM (var-1 ... var-n) <body> ) <form-1> ... <form-n> )

        This is call by nalue evaluation???.

    {\bf Programs: <pgm>}

(PGM (v1 ... vn) stm1 stm2 ... stmn)

The <pgm> form provides a facility for executing ALGOL like
programs, similar to LISP PROG.  The normal order of
executing <stm>s is in the sequence.  However, this may be
modified by the use of branch instructions or the RETURN
instruction.  The variables v1 to vn are local to the
<pgm> and are initialized to NIL.  Their values are lost
once the <pgm> exits but may be referred to within the <pgm>.

{\bf Branch instructions}

Within a <pgm> form, the following statements are provided for 
branching to labels:

(BRT <label> <condition>) 

Branches to <label> if <condition> is TRUE.

(BRF <label> <condition>) 

Branches to <label> if <condition> is FALSE.

(GOTO <label>) - Branches to <label>.


{\bf Labels}


<symbol>

Labels are statements which are simply symbols.  They are not 
        evaluated but provide markers for the branch statements.

{\bf Return}


(RETURN <form>)

The execution of the PGM is halted and the value of <form> is 
returned.  RETURN statements can only be used as a statement 
in a <pgm> form.

    {\bf special functions}

(EVAL <form> )

EVAL computes the value of the <form>.
Mention call by value.

Example:

(EVAL (QUOTE (ADD1 3))) = 4


(APPLY <funnam> <arg1> ... <argn> )

APPLY evaluates and binds each <argi> to the 
corresponding arguments of the function or predicate <funnam>,
and returns the value of applying the function or predicate
to the arguments.

Example:

(APPLY APPEND (QUOTE ((A B) (C D)))) = (A B C D)


{\bf Defining Functions and Predicates}

Since different systems may use different notions of booleans and
first order logic is well typed (and so is finite type theory for
that matter) SEUS distinguishes between predicates which always
return TRUE and FALSE and functions that may return any HGKM
object but TRUE and FALSE.  This distinction is necessary if we
expect to read axioms directly from the code and vice versa.

The definition of a function or a predicates causes a change in the
global environment. HGKM is lexically scoped and this means that
function and predicate definitions are special forms that are not
handled by the evaluator.

{\bf Functions}

A function definition is a special form

(FUNCDEF <funname> ( <var1> ... <varn> ) <body> )

FUNCDEF informes HGKM that the symbol <funname> will be used as
the name of the function defined by the form <body> and that it
argument will be ( <var1> ... <varn> ).

Examples:

(FUNCDEF ID (X) X)

This defines ID to be the function that always returns its
argument as its value.

(FUNCDEF SQUARE (X) (TIMES X X))

This defines SQUARE to be a function that computes the square of
its argument, if X is a number.  Otherwise, an error will result.

{\bf Predicates}

A predicate definition is a special form

(PREDDEF <predname> ( <var1> ... <varn> ) <body> )

FUNCDEF works in the same way as FUNCDEF, but it defines a
predicate.

Examples:

(PREDDEF EVEN (X) (IF (ZERO? (REMAINDER X 2)) TRUE FALSE))

This defines EVEN to be a predicate that returns TRUE when the
argument is an even integer.


{\bf Boolean functions and boolean predicates}

To be clean in the distinction between function and predicates
HGKM supplies a data structure for boolean predicates and a data
structure for boolean functions.

Boolean predicates return

TRUE FALSE

Boolean functions return

the true object TVAL or any other object than FVAL the false 
object FVAL

Examples:

(PREDDEF not (X) (IF X FALSE TRUE))

defines the boolean predicate not

(FUNCDEF fnot (X) (IF (MTL? X) FVAL X))

defines a function that returns FVAL if the argument 
is an empty list.


{\bf Reading and Printing}

1. FOLISP will use `;' (ascii 73) as the comment character.  It will be 
assumed that when the reader sees a `;' it will ignore the rest of the line.



3. FOL is case sensitive and so its code will be.  This is not the usual LISP
default!!!  We need this feature because we want the code to reflect directly
the axiomatization that we will produce of FOL.

READ will accept any S-expression which conforms to the following syntax:

Syntax:

<readable S-expr>::= <atom>
::= @<readable S-expr>
::= (<readable S-exprlist>
 .<readableS-expr> )
 ::= ( )= NIL

 <readable S-expr list>::= <readable S-expr>
 ::= <readable S-expr><readable S-
 expression list>

 Semantics:

 The delimiter "@" designates that the following readable S-expression is
 to be quoted.
 
 Examples:@Ameans (QUOTE A)
 @(@A B) means (QUOTE ((QUOTE A) B))
 @@Ameans (QUOTE (QUOTE A)))
    {\bf The scanner}

7UP uses a table driven token scanner.  The tables are user modifiable but 
this feature is not yet supported.  

{\bf Characters}

There are seven types of characters: letters, digits, delimiters, iddelimiters,
ignore, escape, and special.

<character>   :=  <letter> | <digit> | <delim> | <iddel> | 
                  <ignore> | <escape> | <special> 

<letter>	  A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
                a b c d e f g h i j k l m n o p q r s t u v w x y z

<digit>		0 1 2 3 4 5 6 7 8 9

<delim>		( ) , . : ; [ ] { }

<iddel>		^ ^B ^C ^D ^E ^F ^G ^H ^N ^O ^P ^Q ^R ^S ^T ^U ^V ^W _ 
                = ~ ^Z ^\ ^] ^^ ^_
		! " # $% & ' * + - / < = > ? @ / ^ = ` | 

<ignore> null tab lf vt ff cr space altmode backspace

<escape>

<special>


These characters are used to uniquely decompose an string into tokens.
There are four kinds of tokens


<token>       :=  <identifier> | <number> | <delimiter> | <string>
<identifier>  :=  <iddel>
                  <letter>
                  <identifier> <letter>
                  <identifier> <digit>


{\bf Strings}

Syntax:

string::=  (a string-start followed by any sequence of
characters ending in a string-end)

Semantics:

String-start and string-end are specifiable.


{\bf Numbers}

Syntax:

Same  as specified in Chapter 4, except that leading signs (+
or -) in numbers are treated as delimiters.



{\bf Token scanning primitives}

The scanner is a backupable top down scanner.  It does this by using
an array, TSTACK, to store "tokens" as they are scanned.  Actually
RSCAN returns both a type and a value, where  "value" is the atom
scanned and "type" is: 

 0 if the value is an identifier
  1 if the value is a non-negative integer
   2 if the value is a delimiter.
  
Two global variables are used to keep track of what token we are
looking at in the input stream.  They are PC and ENDSTK.  PC
points into TARRAY at to place the FOL scanner is looking.  ENDSTK
is the last location in TARRAY that has been filled from the current
input.  TARRAY is necessary because RSCAN destroys the input stream.
The FOL parser, being top down, needs to back up.  The main accessing 
routine for TARRAY is the function TSTACK which calls RSCAN if not 
enough tokens have been read.

(TSTACK N)  =  accesses the token stack, TARRAY
               N is the position of the token wanted
               if N is larger than ENDSTK this routine calls RSCAN 
	              until the appropriate token is read.

(TOKEN)     =  PC=C+1
(TOKENV)    =  PC=C+1 and returns val of new PC
(TOKENT)    =  PC=C+1 and returns type of new PC
 
(FLUSH)     =  flush input stream - anticipating starting scanning afresh
 
(PEEKV N)   =  returns the val of PC+N
(PEEKT N)   =  returns the type of PC+N
(NEXTV I)   =  if the val of the next token = I then return it ow return NIL
(NEXTT N)   =  if the type of the next token = N then return it ow return NIL
  
(NTOKEN E)  =  sets TK to val, TKT to type and returns E

Syntactic type Value of SCANValue of SCNVAL

identifier0the uninterned identifier
string1the string
number2the value
delimiter3 the ASCII value of the
  delimiter.


{\bf Scanner modifying functions}

In the following descriptions, all characters are specified by their
numerical ASCII value.  For example, in octal, blank is 40 and A is 101.

(SCANINIT comment-start comment-end string-start string-end slashifier)
SCANINIT modifies  the  LISP  scanner  to  be  an  ALGOL-type
scanner  with  special delimiters for comments and strings.  SCANINIT
must be called before any of the other scanner functions.

(LETTER X)
(DIGIT X)
(DELIM X)
(IDDEL X)
(IGNORE X)
(ESCAPE X)
(SPEC X)


{\bf Input/Output}

{\bf Modifying the scanner}

The scanner modifying functions are not a normal part of the HGKM system
and are presently not available to a user.

I/O in HGKM is very simple.  It is similiar in style to the I/O 
found in early versions of LISP.


{\bf Disk File Names}

<filename>

A filename is specific to the system you are on see appendix x.


{\bf Channel Names}

(OPEN <filename> <channel> <direction> )function

A channel is any symbol.  


{\bf Selection and Control}

(SELECT <channel> )function

INPUT releases any file previously initialized on the channel, 
and initializes for input the first file specified by the 
filename-list.	INPUT returns the channel if one was specified, 
T otherwise.  INPUT does not evaluate its arguments.

(CLOSE <channel> )


$EOF$system constant

(ABORT (QUOTE $EOF$)) is called.  The use of TRAP
around any functions which accept input therefore makes it possible to
detect and trap an end of file.  If no TRAP is used, control returns 
to the top level of HGKM.  


{\bf Reading and writing to multiple files}

In order to READ from multiple input sources, separate channels should 
be opened using OPEN, and SELECT can then select the appropriate channel 
to READ from.

Example: The following show a fairly typical sort of manipulation of two
files at once.

{\bf Input Functions}

(LOAD <filename> )function

The function DSKIN is supplied for this purpose.  It has the same effect
as doing INC and INPUT on its arguments, except that no channel name is
admissible, and no device name is required.  The channel name will always
be T, and `DSK' will be supplied as a device name, if none is given.

Example:

(LOAD "integer.ax")

Will read ...

(READ)function

READ causes the next S-expression to be read from the selected input
channel, and returns the internal representation of the S-expression.

See the details of the reader below

(TYI)function

TYI causes the next character to be read from the selected input 
device and returns the ASCII code for that character.


Example:

(DEFLAM TEREAD () (IF (EQ (TYI) LF) () (TEREAD)) )

TEREAD will ignore all characters until a line-feed is seen.


{\bf Output}

{\bf Printing functions}

(PRINC S)function

(CRLF) function

CRLF positions the cursor at the beginning of the next line.

(PRINT [obj] ) function

Prints the print name of obj or the print representation
of the data structure. It does not return any reliable value.


(TYO [char] )function

TYO prints the character whose ASCII value is N, and returns N.

{\bf Error handling}

(TRAP <form> )

TRAP evaluates <form> and if no error occurs during its evaluation, TRAP
returns the samee thing as (LIST <form>).  If a system error occurs during 
        an evaluation then TRAP returns an atomic object that can be tested for 
        determining what the error was.  If the function ABORT is called during 
	evaluation of <form> then TRAP will return the value of the argument of 
	ABORT.

(ABORT <form> )

ABORT returns the value of <form> to the most recent ERRSET, or to the 
top level of HGKM if there is no TRAP.

{\bf Debugging}

{\bf Bibliography}

{\bf Index}

{\bf Appendix: FOL}

FOL note:   The conditional form of HGKM does not distinguish 
between functions and predicates.  This means that you write 
a form that is not an FOLform.

{\bf Appendix: Useful functions}


{\bf Mapping functions}

(FOR (IN <var> <list> ) DO <form> )
(FOR (IN <var> <list> ) COLLECT <form> )

(TOEACH (IN <var> <list> ) DO <form> )

(FORALL (IN <var> <list> ) DO <form> )
(EXISTS (IN <var> <list> ) DO <form> )

(COLLECT <form-1> ... <form-n> )


{\bf specifically for WFFs}

(FOR (INARGS <var> <args> ) DO <form> )
(FOR (INARGS <var> <args> ) COLLECT <form> )

(TOEACH (INARGS <var> <args> ) DO <form> )

(FORALL (INARGS <var> <args> ) DO <form> )
(EXISTS (INARGS <var> <args> ) DO <form> )

(MKARGS <form-1> ... <form-n> )

(EQ X Y)

The value of EQ is T if X and Y are the same pointer, i.e., the same
internal address.  Identifiers on the OBLIST have unique addresses and
therefore EQ will be T if X and Y are the same identifier.  EQ will also
return T for equivalent INUMs, since they are represented as addresses.
However, EQ will not compare equivalent numbers of any other kind. For
non-atomic S-expressions, EQ is T if X and Y are the same pointer.

Examples:(EQ T T)= T
(EQ T NIL)= NIL
(EQ (QUOTE A)(QUOTE B))= NIL
(EQ 1 1.0) = NIL
(EQ 1 1)= T
(EQ 1.0 1.0)= NIL

(EQUAL X Y)

The value of EQUAL is T if X and Y are identical S-expressions.  EQUAL can
also test for equality of numbers of mixed types.  EQUAL is equivalent to:

(LAMBDA(X Y) (COND ((EQ X Y) T)
   ((AND (NUMBERP X) (NUMBERP Y))
       (ZEROP (*DIF X Y)))
          ((OR (ATOM X)(ATOM Y)) NIL)
	     ((EQUAL (CAR X) (CAR Y))
	         (EQUAL (CDR X) (CDR Y)))))

Examples:	 (EQUAL T T) = T
(EQUAL 1 1)	 = T
(EQUAL 1 1.0)	 = T
(EQUAL (QUOTE (A B)) (QUOTE (A B)))= T
(EQUAL (QUOTE (T)) T)= NIL

.ssect1(S-expression Predicates);

(NULL L)= T if and only if L is NIL.

(MEMBER L1 L2) = T if and only if L1 is EQUAL to a top level element of L2.

MEMBER is equivalent to:

(LAMBDA(L1 l2) (COND ((ATOM L2) NIL)
     ((EQUAL L1 (CAR L2))T)
          (T(MEMBER L1 (CDR L2)))))

Examples: (MEMBER (QUOTE (C D)) (QUOTE ((A B)(C D)E)))= T
(MEMBER (QUOTE C)(QUOTE (C))))= NIL

(MEMQ L1 L2)= T iff L1 is EQ to a top level element of L2.

MEMQ is equivalent to:

(LAMBDA(L1 L2)(COND ((ATOM L2) NIL)
    ((EQ L1 (CAR L2)) T)
        (T(MEMQ L1 (CDR L2)))))

Examples:(MEMQ (QUOTE (C D))(QUOTE ((A B)(C D) E))) = NIL
(MEMQ (QUOTE A) (QUOTE (Q A B))) = T

.ssect1(Boolean Predicates);

The Boolean predicates perform logical operations on the truth values NIL
and T.  A non-NIL value is considered equal to T.

(NOT X) = T if X is NIL
= NIL otherwise

(AND X^1 X^2 ...X^n)= T if all X^i are non-NIL
= NIL otherwise

Note: (AND) = T.   AND evaluates its arguments  from  left to right
until either NIL is  found  in  which  case  the  remaining
arguments  are  not  evaluated,  or until the  last  argument
is evaluated.

(OR X^1 X^2 ... X^n)= T if any X^i is non-NIL
= NIL otherwise

.sect(Functions on S-expressions);

This section describes functions for building, fragmenting, modifying,
transforming, mapping, and searching S-expressions, as well as some
non-standard functions on S-expressions.

.ssect1(%4CONS%*);

(CONS X Y)

The value of CONS of two S-expressions is the pair of those S-expressions.

Example:(CONS(QUOTE A) (QUOTE B)) = (A.B)

(XCONS X Y) = (CONS Y X)
(NCONS X)   = (CONS X NIL)
(LIST X1 ... Xn) = (CONS X^1 (CONS X^2 ...(CONS X^n NIL)...))

List evaluates all of its arguments and returns a list of their values.

Examples:(LIST) = NIL
(LIST (QUOTE A)) = A
(LIST (QUOTE A) (QUOTE B)) = (A B)

(APPEND X Y)

(DE APPEND (X Y)
     (COND ((NULL X) Y)
        (T (CONS (CAR X) (APPEND (CDR X) Y)))))

Example:(APPEND) = NIL
(APPEND (QUOTE (A B)) (QUOTE (C D)) (QUOTE (E))) = (A B C D E)

.ssect1(|%4CAR%* and %4CDR%*|);

(CAR L)

The CAR of a non-atomic S-expression is the first element of that dotted
pair.  CAR of an atom is undefined and will usually cause an illegal
memory reference.

(CDR L)

The CDR of a non-atomic S-expression is the second (and last) element of
that dotted pair.  The CDR of an identifier is its property list.  The CDR
of an INUM causes an illegal memory reference.  The CDR of any other
number is the list structure representation of that number.

Examples: (CAR (QUOTE (A B C))) = A
(CAR (QUOTE A)) is illegal
(CDR (QUOTE (A B C))) = (B C)
(CDR (QUOTE A)) is the property list of A
(CDR (QUOTE (A)))  = NIL


CAAR, CADR,..., CDDDDR

All  of  the  composite CAR-CDR functions with up to four A's
and D's are available.

Examples:(CADR X) = (CAR (CDR X))
(CAADDR X) = (CAR (CAR (CDR (CDR X))))

(LAST L)

LAST  returns  the  last  part  of  a  list  according to the
following definition:

(DE LAST (L)
    (COND ((ATOM (CDR L)) L)
      (T (LAST (CDR L)))))

Examples:(LAST (QUOTE (A B C))) = (C) = (C.NIL)
(LAST (QUOTE (A B . C))) = (B.C)

.ssect1(S-expression transforming functions);

The following functions transform S-expressions from one form to
another.

(LENGTH L)

LENGTH  returns  the number of top-level elements of the list
L. LENGTH is equivalent to:

(DE LENGTH (L)
    (COND ((ATOM L) 0)
      (T (ADD1 (LENGTH (CDR L))))))

(REVERSE L)

REVERSE  returns  the  reverse  of  the  top level of list L.
REVERSE is equivalent to:

(DE REVERSE (L) (REVERSE1 L NIL))
(DE REVERSE 1 (L M)
(COND ((ATOM L) M)
      (T (REVERSE1 (CDR L) (CONS (CAR L) M)))))

(SUBST X Y S)

SUBST substitutes S-expression X for all EQUAL occurrences of
S-expression Y in S-expression S.  SUBST is equivalent to:

(DE SUBST (X Y S)
            (COND ((EQUAL Y S) X)
	      ((ATOM S) S)
	        (T (CONS (SUBST X Y (CAR S))
		   (SUBST X Y (CDR S))))))

Note:  (SUBST 0 0 X) is useful for creating a copy of the list X.

Example:(SUBST 5 (QUOTE FIVE) (QUOTE (FIVE PLUS FIVE IS TEN)))
       = (5 PLUS 5 IS TEN)

.ssect1(S-expression mapping functions);

The  following  functions perform mappings of lists according
to the functional arguments supplied.

(MAP FN L)

MAP  applies the function FN of one argument to list L and to
successive CDRs of L until L is reduced to NIL.  The value of MAP  is
NIL. MAP is equivalent to:

(DE MAP (FN L)
    (PROG NIL
         L1  (COND ((NULL L)(RETURN NIL)))
	   (FN L)
	     (SETQ L (CDR L))
	       (GO L1)))

Example:       (MAP (FUNCTION PRINT) (QUOTE (X Y Z))) =

PRINT:(X Y Z)
PRINT:(Y Z)
PRINT:(Z)
PRINT:NIL

(MAPC FN L)

MAPC is identical to MAP except that MAPC applies function FN
to the CAR of the remaining list at each step.  MAPC is equivalent to:

(DE MAPC (FN L)
    (PROG NIL
        L1    (COND ((NULL L)(RETURN NIL)))
	(FN (CAR L))
	(SETQ L (CDR L))
	(GO L1)))

Example:(MAPC (FUNCTION PRINT) (QUOTE (X Y Z))) =

PRINT:X
PRINT:Y
PRINT:Z
PRINT:NIL

(MAPLIST FN L)

MAPLIST applies the function FN of one argument to list L and
to  successive  CDRs  of  L  until L is reduced to NIL.  The value of
MAPLIST is the list of values returned by FN.  MAPLIST is  equivalent
to:

(DE MAPLIST (FN L)
    (COND ((NULL L) NIL)
        (T (CONS (FN L) (MAPLIST FN (CDR L))))))


Examples:(MAPLIST (FUNCTION CAR) (QUOTE (A B C D))) = (A B C D)
(MAPLIST (FUNCTION REVERSE) (QUOTE (A B C D))) =
((D C B A) (D C B) (D C) (D))

(MAPCAR FN L)

MAPCAR is identical to MAPLIST except that MAPCAR applies  FN
to  the CAR of the remaining list at each step.  MAPCAR is equivalent
to:

(DE MAPCAR (FN L)
    (COND ((NULL L) NIL)
      (T (CONS (FN (CAR L)) (MAPCAR FN (CDR L))))))

Examples:(MAPCAR (FUNCTION NCONS) (QUOTE (A B C D))) = ((A) (B) (C) (D))
(MAPCAR (FUNCTION ATOM) (QUOTE ((X) Y (Z)))) = (NIL T NIL)

.ssect1(S-expression Searching Functions);

(ASSOC X L)

ASSOC searches the list of dotted pairs L for a pair whose CAR is EQ to X.
If such a pair is found it is returned as the value of ASSOC, otherwise
NIL is returned.  ASSOC is equivalent to:

(DE ASSOC (X L)
    (COND ((NULL L) NIL)
      ((EQ X (CAAR L)) (CAR L))
        (T (ASSOC X (CDR L)))))

Example:(ASSOC 1 (QUOTE ((1.ONE) (2.TWO)))) = (1.ONE)

{\bf more stuff}

HGKM supplies also a special form SUBSTDEF to define
functions that we expect the compiler to put in line.

(SUBSTDEF <funname> ( <var1> ... <varn> ) <body> )  


    {\bf Functions}

Functions have fixed arity

(DEFFLAM
(DEFPLAM

(DEFFMAC
(DEFPMAC

(DEFFSUB
(DEFPSUB

    {\bf Predicates}

    Examples:

    (DEFPFUN not (X)     (IF X FALSE TRUE))
    (DEFPFUN and (X Y)   (IF X (IF Y TRUE) FALSE))
    (DEFPFUN or  (X Y)   (IF X TRUE Y))
    (DEFPFUN imp (X Y)   (IF X (IF Y TRUE FALSE) TRUE))

Predicates test S-expressions for particular values, forms, or ranges of
values.  All predicates described in this chapter return either NIL or T
corresponding to the truth values false and true, unless otherwise noted.
Some predicates cause error messages or undefined results when applied to
S-expressions of the wrong type.





(DEFLAM function-name argument-list body).

We will never use DEFUN or DE.

We will supply a special form DEFSUB which will be used to define FOL
functions that we expect the compiler to put in line when we make
production versions of FOL.  This would be used for defining abstract
syntatic functions, for example.  It has the syntax

(DEFSUB function-name argument-list body).

We use DEFMAC for normal macros.

(DEFMAC macro-name arg body)


You cannot have a global constant and an equal function name.  Logic doesn't 
allow this and we won't either.


We will write FOL functions in such a way that they always take a fixed 
arguments.  It is possible that the LAST argument may be a list of list if
this is the case we enclose these arguments in the special form

(CART A1 ... An)

to annotate the information that they are to thought of as a muultiple
argument.  In LISP these will be translated into (LIST A1 ... An).


EMPTYA constant with no value



Since different systems may use different notions of booleans and first
order logic is well typed (and so is finite type theory for that matter)
we will need to distinguish between predicates, where we will always
return TRUE and FALSE, and functions, which must return values.  To be
clean we supply two predicates, IST and ISF, which for all objects assign
them either to represent TRUE or FALSE.  We use TVAL and FVAL as two
objects that are guarenteed to to have the following behavior.

(IST TVAL) == TRUE
(IST FVAL) == FALSE
(ISF TVAL) == FALSE
(ISF FVAL) == TRUE 

Of course 

(FORALL OBJ (NOT (IFF (IST OBJ) (ISF OBJ))))

These will be made to work this way in all environments.  If we always
return TRUE or FALSE explicitly in the code for defined predicates things
will work correctly hereditarily.

For predicates we return 

TRUE
FALSE

For functions we return 

TVAL     the canonical true object
FVAL     the canonical false object

IST is a predicate on all objects determining which are ``FALSE''
ISF      is a predicate on all objects determining which are ``TRUE''

These conventions are necessary if we expect to read axioms directly from the
code and vice versa.

We will supply a special form DEFLAM which will be used to define FOL
FOL functions.  It has the syntax

HGKM Manual

Abstract

Table of contents

1 Introdction

Introduction

Interactive use of HGKM