This program solves another exercise in Chapter 10. It implements the semantic tableau for the identity calculus. The propositional connectives are multi-letter symbols in capitals, the propositional atoms and the individual constants are lower case multi-letter identifiers.
The following are an input file and the output produced by the program. The input file states the puzzle given at the end of Chapter 11. The first seven lines express the assumptions which are implicit in the puzzle. The last four lines are essentially a transcription of the clues that had been given. Since the program always tries to show that a formula is not a logical truth, the formula expressing the puzzle is negated. If the program finds a countermodel to the negated formula, this model will make the assumptions and the clues true --- in other words the model constitutes a solution. The following is the input:
The implementation given here again uses the simplest and cleanest parsing and translation method: recursive descent.
The scanner, procedure getsym,
has to be able to recognise symbols starting with letters
or symbols consisting of a single non-letter character.
Some parts of the procedure are similar to corresponding
parts in the scanning procedure used in Chapter ?
for the program to process context free grammars.
For symbols starting with a letter any further letters or digits
are collected into a string.
If the first letter was uppercase,
then it should be one of the five operators,
otherwise an error is reported.
If the first letter was lowercase,
then a linear sentinel search is conducted through
a table of identifiers.
If it is not found there, it is entered
and marked as undefined.
In any case the scanner reports back where the identifier is located.
For symbols that are just single non-letter characters
a CASE statement can be made to handle these.
The parser uses recursive descent in an entirely conventional manner.
The only part that deserves comment is procedure factor
in the case dealing with identifiers.
There are two alternatives:
either after the identifier
the next symbol is one of the relations,
= or # for identity or diversity,
and then the identifier is an individual constant,
or the next symbol is something else,
and the identifier is a proposition.
So what the identifier should be can only be determined
by inspection of the next symbol,
and hence, when the identifier is seen,
its location in the table has to be saved in a local variable.
When the next symbol has been seen,
one or the other action is taken.
If the next symbol is one of the two relations,
= or #,
then the previous identifier,
whose location was saved locally,
has to be an individual constant.
This checking is done by a separate local procedure
which makes the identifier into an individual constant
in case it was new.
After the relation,
another individual constant is expected,
and this is checked by another call to the same procedure.
On the other hand,
if the symbol following the first identifier in the factor
is not one of the two relations,
then the identifier has to be checked to be a proposition.
The three possibilities,
the relations a = b or a # b
and atomic propositions, generate three different kinds of tree code.
The other parts of procedure factor,
and all of the procedures term, expression and formula,
are entirely conventional.
Tableau generator: The other changes are to the procedure for making formulas true or false, and to the procedure for showing the countermodels that have been constructed. Both access the table of identifiers which at run time have to have an extension: propositions have a truth value, individual constants have an individual 1, 2, and so on.
The procedure for making formulas true or false has familiar cases
for the boolean operators not, and, imp and iff,
and for the operands true and false.
The case for propositional atoms is also essentially familiar,
except that the truth value is now recorded in the table.
The only case that needs extensive discussion is the case
for the relations = and #.
The goal can be to make a formula true or to make it false.
To make a = b true, and to make a # b false,
really amount to the same thing,
and similarly for making a = b false
and for making a # b true.
But for each of these two possibilities
there are further variations to consider,
depending on whether the two individual constants a
and b have individuals assigned to them or not.
Hence there are a total of eight subcases to consider.
One way to do so is to have a branching fan of IF-THEN-ELSE
statements three levels deep to implement the eight subcases.
Another way is to compute one of eight numbers,
0 to 7,
from the possible variations,
and to let a CASE statement branch on the computed value.
This is the method used here.
The two simplest cases arise when the two individual constants
both have individuals assigned to them.
If the two individuals assigned are identical or different
as required, then the continuation procedure is called,
otherwise nothing happens.
Then there are two cases
where an identity has to be made true
and one of the two individual constants has an individual
assigned to it but the other does not.
In these two cases a local procedure with two parameters is called;
what it does is to assign the individual given by the one parameter
to the individual constants given by the other, undefined parameter,
call the continuation, and then set the previously undefined
individual constant back to undefined.
The remaining four cases have more in common than might be supposed
at first.
Some of them require identities to be made true,
others require identities to be made false.
Some have one of the two individual constants instantiated,
others have none instantiated.
What they have in common is that some uninstantiated
individual constant will have to be assigned an individual,
either an old one or a new one,
to make the relational formula true or false as required.
In these cases a local procedure will be called which takes
only one parameter.
What it does is to assign either an old or a new individual
to the individual constant which is given as a parameter.
In detail, this works as follows:
First a FOR loop is used to step through all the individuals
in the current domain;
for each individual it uses the other previously mentioned
procedure to assign that individual to the parameter that was given.
Second, a new individual is created,
the other procedure is used to assign this new individual
to the parameter,
and on return the new individual is destroyed.
The procedure for showing countermodels first deals with atomic propositions and then with individual constants. For both it has to step through the table repeatedly. For the propositions it writes, for each of the two truth values, all the propositions having that truth value it can find in the table. For the individual constants it does much the same --- for each individual it writes out the individual constants having that individual as their extension it can find in the table. It would have been possible to make do with only one pass through the table, writing out the proposition or the individual constant and their extensions, if any, in the order in which they occur in the table. This method would be more efficient on the computer, but somewhat more tedious for the human reader.
I am still using this program in a course. The source will be made available towards the end of 2003.
This program is an implementation of
the exercise on Proplog in Chapter 11.
Recall that + switches the system into a mode for adding
information to a database,
and that - switches it into querying mode.
Here is a demonstration of the program,
including negation:
The implementation is modelled as far as possible on the general parser for context free grammars in Chapter 11. This was done mainly to illustrate the closeness between grammars and the Proplog language.
The main program clearly has to consist of a REPEAT loop which reads
the first symbol of the input.
If it is one of + or -,
a variable indicating the current mode is set to entering or to questioning.
Otherwise, depending on what the current mode is,
a question is to be read or a fact or rule is to be entered.
In the first case,
an expression is to be read and the interpreter then
determines whether it generates the language {0} or the language {}.
Alternatively we can say that the interpreter either succeeds or fails
in proving the expression from its current database.
In the second case a new fact or rule is to be entered.
For both of these the current symbol must be an atom
which the scanner may or may not have seen before.
If the next symbol is a period .,
then what is being entered is a fact,
and the symbol table entry for that atom has to be given a code entry
that make later attempts to prove it succeed.
If the next symbol is not a .,
then it should be a :- turnstyle followed by an expression.
Then the symbol table entry for the atom
should be given the code generated by the expression,
so that attempting to prove the atom later results
in attempting to prove the expression.
Expressions have to be processed by a procedure expression
for questions being read or for rules
being entered.
In either case internal code is generated in the form of a binary tree.
The program again uses recursive descent,
with subsidiary procedures term and factor,
all three modelled on the corresponding procedures
in the parser for context free grammars.
One minor difference is that expression and term deal with infix
operators ; and ,,
to be interpreted as or and and.
A more important differences occurs in factor:
there are no terminals, only non-terminals, and here they are called atoms.
Also, there is a case for a unary negation operator,
and of course another for parentheses.
The scanner, procedure getsym, contains no surprises.
After skipping blanks it enters one or another branch
depending on whether the first printing character is a letter.
If it is, then the letter and any further letters and digits
are collected into a string.
If that happens to be the string not,
the only reserved word,
then it is passed to the parsing procedure as the negation symbol.
All other strings count as atoms,
and a symbol table has to be searched to determine whether
they have been seen before.
If they have not been seen before,
they are entered as new and are given a code entry
that will make attempts to prove them fail.
Such an entry may later be overridden
by the main program when facts or rules are being entered.
If the first printing character is not a letter,
then it should be one of a small number of special characters
which are either single character symbols
or the two character symbol :-, the turnstyle.
If the first printing character is not one of these,
then an error is reported.
The interpreter, called by main in questioning mode,
is of course very similar to the procedure parse
of the context free grammar parser.
One difference is that the global procedure that is used as the
initial continuation does not result in any printout;
essentially because there is nothing to print out
except perhaps {0},
the language containing just the null string.
On the logical interpretation this would indicate
that the formulas has been proved.
So, instead of printing, the procedure sets a global
success flag to true.
This flag is initially set to false in main before the interpreter
is called,
and its value on return determines whether main will write
yes or no.
The body of the interpreter dispatches a CASE statement
on the operator part of the tree code.
A call-instruction,
resulting from an atom,
causes the table to be consulted.
If the code found there is a special success code for facts,
then the continuation is called.
If the code found is for an expression,
the interpreter calls itself recursively.
An and-instruction is handled in a now familiar manner,
with a local procedure as a continuation.
An or-instruction results in the left disjunct being attempted
as before, but the right disjunct is attempted only
if the left disjunct failed to set the success flag.
A not-instruction leads to a recursive call with the negand
but without the continuation that had been passed as the parameter.
Instead the global procedure for setting the success flag is used
as a continuation.
Then upon return of the recursive call,
if the flag is still false,
indicating failure of the negand and hence success of the negation,
then the continuation parameter is called,
otherwise the success flag is set to false.
The following is the standard Pascal source program for the Proplog program.
This sections describes a solution to the last exercise
in Chapter 13,
to design a simple translation machine.
All instructions have an operator field.
Additionally some also have either an address field
for calls, gotos and matches,
or a character or string field for write instructions,
and a character set field for matches.
There is an array to contain whatever number of instructions
are required.
For the interpretation a stack of integers is provided
which contains return address and (ord-values of) local character
variables.
The interpreter at the end of the program has the usual structure,
note that it is quite independent of the input and output languages.
The input and output languages are determined by the program
that will be run.
The method adopted here was to use the first of the three ways
mentioned at the end of the exercise:
A program for translating from prefix to fully parenthesised
infix was written in the language which the interpreter understands.
This program was then easily translated into a series of assignments
to various fields of an ARRAY p.
These assignment statements constitute the rather ugly initialisation section.
The ARRAY now contains a program that
will be run by the translation machine in the REPEAT loop.
The method works --- but it is not recommended for anything but
the smallest demonstration programs because the style
makes the programs just about unmaintainable.
For anything larger one would want to use either
the second or the third way mentioned.
The program uses two optimisations: For formulas starting with a binary operator the program does not jump over the error section to the end of the procedure where one might expect a return instruction. Instead the return instruction is executed immediately after the formula containing the binary operator has been completed. For formulas beginning with a negation it even uses what is known as "tail recursion": Instead of calling another formula, it simply gotos to the beginning of the code for formulas. This is possible in the special case where after returning from a negated formulas there is nothing further to do at the point of return. For errors it is necessary to clear the stack again, so instead of returning, flow of control goes right back to the beginning.
The method of putting the string message into the instructions has the effect that all instructions need that much space. In any but a toy program this would be an intolerable waste, and the few message instructions should really use an index into an array of messages. However, this does make the machine just marginally more complex.
The following is the standard Pascal source for the general translator.
Note that this collection of parsing primitives
will only work for languages without lookahead ---
such as prefix notation or fully parenthesised infix notation.
For minimally parenthesised infix notation it is necessary
to have a one symbol lookahead in a global variable
and a getch instruction.