An exercise in Chapter 11 suggested to write a program
to read a grammar and write all strings up to a given length
that are in the language generated by that grammar.
The program given here does that in a minimal way ---
to keep it as simple as possible all non-terminals
are just uppercase letters,
and the starting symbol is just S.
In the following listing,
the first part demonstrates familiar aspects of grammars.
The program again uses continuations to achieve backtracking
when generating strings in the language defined by the grammar.
In addition to these continuations for second order recursion,
the program uses an further layer of continuations
to explore their power.
So the second part of this listing introduces some new operators
which are entirely experimental and at this stage not well understood.
As the examples show, they clearly increase
the expressive power of regular expressions and of context free grammars.
{ CONTEXT FREE GRAMMARS }
S = 0 | aSb . 10
ab aabb aaabbb aaaabbbb
{ well-formed parentheses }
S = 0 | ( '( S ') )+ . 10
() (()) ((())) (((()))) ((()())) (()()) (()(()))
((())()) ()() ()(()) ()((())) ()()() (())() (())(())
((()))()
{ prefix }
S = 'p | 'N S | ('A | 'K) S S . 5
p Np NNp NNNp NNNNp NNApp NNKpp NApp NApNp NANpp
NKpp NKpNp NKNpp App ApNp ApNNp ApApp ApKpp ANpp
ANpNp ANNpp AAppp AKppp Kpp KpNp KpNNp KpApp KpKpp
KNpp KNpNp KNNpp KAppp KKppp
{ minimally parenthesised infix,
but triple negation to reduce output }
S = T ('v T)* ;
T = F ('& F)* ;
F = 'p | '-'-'-F | '( S ') . 13
p pvp pvpvp pvpvpvp pvpvp&p pvpvp&p&p pvpv---p
pvpv(p) pvp&p pvp&pvp pvp&pvp&p pvp&p&p pvp&p&pvp
pvp&p&p&p pvp&p&---p pvp&---p pvp&---p&p pvp&(p) pv---p
pv---pvp pv---p&p pv---p&p&p pv------p pv---(p) pv(p)
pv(p)vp pv(p)&p pv(pvp) pv(p&p) pv(---p) p&p p&pvp
p&pvpvp p&pvpvp&p p&pvp&p p&pvp&pvp p&pvp&p&p p&pvp&---p
p&pv---p p&pv---p&p p&pv(p) p&p&p p&p&pvp p&p&pvpvp
p&p&pvp&p p&p&pv---p p&p&p&p p&p&p&pvp p&p&p&p&p
p&p&p&p&p&p p&p&p&---p p&p&p&(p) p&p&---p p&p&---pvp
p&p&---p&p p&p&------p p&p&(p) p&p&(p)&p p&p&(p&p) p&---p
p&---pvp p&---pvp&p p&---p&p p&---p&pvp p&---p&p&p
p&---p&---p p&------p p&------p&p p&---(p) p&(p) p&(p)vp
p&(p)&p p&(p)&p&p p&(pvp) p&(p&p) p&(p&p)&p p&(p&p&p)
p&(---p) p&((p)) ---p ---pvp ---pvpvp ---pvp&p ---pvp&p&p
---pv---p ---pv(p) ---p&p ---p&pvp ---p&pvp&p ---p&p&p
---p&p&pvp ---p&p&p&p ---p&p&---p ---p&---p ---p&---p&p
---p&(p) ------p ------pvp ------p&p ------p&p&p ---------p
------(p) ---(p) ---(p)vp ---(p)&p ---(pvp) ---(p&p)
---(---p) (p) (p)vp (p)vpvp (p)vp&p (p)v---p (p)&p
(p)&pvp (p)&p&p (p)&p&p&p (p)&---p (p)&(p) (pvp) (pvp)vp
(pvp)&p (pvpvp) (pvp&p) (pv---p) (p&p) (p&p)vp (p&p)&p
(p&p)&p&p (p&pvp) (p&p&p) (p&p&p)&p (p&p&p&p) (p&---p)
(p&(p)) (---p) (---p)vp (---p)&p (---pvp) (---p&p)
(------p) ((p)) ((p))&p ((p)&p) ((p&p))
{ an alternative grammar for the same language }
S = T ('v S)? ;
T = F ('& T)? ;
F = 'p | '-'-'-F | '( S ') . 13
p pvp pvpvp pvpvpvp pvpvp&p pvpvp&p&p pvpv---p
pvpv(p) pvp&p pvp&pvp pvp&pvp&p pvp&p&p pvp&p&pvp
pvp&p&p&p pvp&p&---p pvp&---p pvp&---p&p pvp&(p) pv---p
pv---pvp pv---p&p pv---p&p&p pv------p pv---(p) pv(p)
pv(p)vp pv(p)&p pv(pvp) pv(p&p) pv(---p) p&p p&pvp
p&pvpvp p&pvpvp&p p&pvp&p p&pvp&pvp p&pvp&p&p p&pvp&---p
p&pv---p p&pv---p&p p&pv(p) p&p&p p&p&pvp p&p&pvpvp
p&p&pvp&p p&p&pv---p p&p&p&p p&p&p&pvp p&p&p&p&p
p&p&p&p&p&p p&p&p&---p p&p&p&(p) p&p&---p p&p&---pvp
p&p&---p&p p&p&------p p&p&(p) p&p&(p)&p p&p&(p&p) p&---p
p&---pvp p&---pvp&p p&---p&p p&---p&pvp p&---p&p&p
p&---p&---p p&------p p&------p&p p&---(p) p&(p) p&(p)vp
p&(p)&p p&(p)&p&p p&(pvp) p&(p&p) p&(p&p)&p p&(p&p&p)
p&(---p) p&((p)) ---p ---pvp ---pvpvp ---pvp&p ---pvp&p&p
---pv---p ---pv(p) ---p&p ---p&pvp ---p&pvp&p ---p&p&p
---p&p&pvp ---p&p&p&p ---p&p&---p ---p&---p ---p&---p&p
---p&(p) ------p ------pvp ------p&p ------p&p&p ---------p
------(p) ---(p) ---(p)vp ---(p)&p ---(pvp) ---(p&p)
---(---p) (p) (p)vp (p)vpvp (p)vp&p (p)v---p (p)&p
(p)&pvp (p)&p&p (p)&p&p&p (p)&---p (p)&(p) (pvp) (pvp)vp
(pvp)&p (pvpvp) (pvp&p) (pv---p) (p&p) (p&p)vp (p&p)&p
(p&p)&p&p (p&pvp) (p&p&p) (p&p&p)&p (p&p&p&p) (p&---p)
(p&(p)) (---p) (---p)vp (---p)&p (---pvp) (---p&p)
(------p) ((p)) ((p))&p ((p)&p) ((p&p))
{ *************************************************************** }
{ The remainder of this listing illustrates some experimental
operators which at this stage are not well understood }
{ AUGMENTED REGULAR EXPRESSIONS }
{ The language a^n b^n }
S = (a b>)* . 12
ab aabb aaabbb aaaabbbb aaaaabbbbb
{ The language (a|b)* followed by : and its reverse }
S = (a a> | b b>)* ': . 10
: a:a aa:aa aaa:aaa aaaa:aaaa aaab:baaa aab:baa
aaba:abaa aabb:bbaa ab:ba aba:aba abaa:aaba abab:baba
abb:bba abba:abba abbb:bbba b:b ba:ab baa:aab baaa:aaab
baab:baab bab:bab baba:abab babb:bbab bb:bb bba:abb
bbaa:aabb bbab:babb bbb:bbb bbba:abbb bbbb:bbbb
{ The language over (ab) for which N(a) = N(b)
and for each prefix, N(a) >= N(b) }
S = (a & b)* . 15
ab abab ababab abababab ababaabb abaabb abaabbab
abaababb abaaabbb aabb aabbab aabbabab aabbaabb aababb
aababbab aabababb aabaabbb aaabbb aaabbbab aaabbabb
aaababbb aaaabbbb
{ Similar, but N(a) = N(b) = N(c)
and for each prefix, N(a) >= N(b) >= N(c) }
S = (a & b & c)* . 20
abc abcabc abcabcabc abcababcc abcaabcbc ababcc
ababccabc ababcabcc abababccc abaabcbcc aabcbc aabcbcabc
aabcbabcc aabcabcbc aababccbc aaabcbcbc
{ The language over (ab) in which for each suffix, N(a) <= N(b) }
S = a# b+. 8
ab abb abbb abbbb abbbbb abbbbbb abbbbbbb abab
ababb ababbb ababbbb ababbbbb ababab abababb abababbb
abababab ababbab ababbabb ababbbab abbab abbabb abbabbb
abbabbbb abbabab abbababb abbabbab abbbab abbbabb
abbbabbb abbbabab abbbbab abbbbabb abbbbbab
{ For comparison with the previous L, a+ instead of a# }
S = a+ b+. 8
ab abb abbb abbbb abbbbb abbbbbb abbbbbbb aab aabb
aabbb aabbbb aabbbbb aabbbbbb aaab aaabb aaabbb aaabbbb
aaabbbbb aaaab aaaabb aaaabbb aaaabbbb aaaaab aaaaabb
aaaaabbb aaaaaab aaaaaabb aaaaaaab
{ AUGMENTED CONTEXT FREE GRAMMARS }
{ The language a^n b^n c^n }
S = 0 | a S c> b . 10
abc aabbcc aaabbbccc
{ The language a^n b^n c^n d^n }
S = 0 | a d> S c> b . 20
abcd aabbccdd aaabbbcccddd aaaabbbbccccdddd
{ The language (a|b)* followed by : and itself }
S = ': | a S a> | b S b> . 10
: a:a aa:aa aaa:aaa aaaa:aaaa aaab:aaab aab:aab
aaba:aaba aabb:aabb ab:ab aba:aba abaa:abaa abab:abab
abb:abb abba:abba abbb:abbb b:b ba:ba baa:baa baaa:baaa
baab:baab bab:bab baba:baba babb:babb bb:bb bba:bba
bbaa:bbaa bbab:bbab bbb:bbb bbba:bbba bbbb:bbbb
{ The language a^S(i), S(i) is the sum of the first i integers }
S = a | 0 (S & 0) a . 40
a aaa aaaaaa aaaaaaaaaa aaaaaaaaaaaaaaa
aaaaaaaaaaaaaaaaaaaaa aaaaaaaaaaaaaaaaaaaaaaaaaaaa
{ The language a^(2^n) }
S = aa | 0 S (a & a) . 40
aa aaaa aaaaaaaa aaaaaaaaaaaaaaaa
aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
To save space, this implementation is
kept to an absolute minimum, it is intended to be used
for experimentation by experienced users.
Hence there is no error checking at all.
The following is the standard Pascal source
for the grammar generator program.
Interested readers should be able to understand the
definition and implementation of the new experimental operators
(marked NEW) in the body of the expanding procedure exp.
PROGRAM grammar_generator(input,output);
LABEL 99;
CONST maxcode = 500;
VAR
ch : char;
nonterminals : ARRAY ['A'..'Z'] OF integer;
current : char;
code : ARRAY [1..maxcode] OF
RECORD op : char; left,right : integer END;
cx : integer;
s : ARRAY [1..120] OF char;
p,max : integer;
linelength : integer;
PROCEDURE getc;
BEGIN
If eof THEN GOTO 99;
IF eoln
THEN BEGIN readln; writeln; ch := ' ' END
ELSE BEGIN read(ch); write(ch) END
END; (* getc *)
PROCEDURE getch;
LABEL 1;
BEGIN (* getch *)
1:REPEAT getc UNTIL ch > ' ';
IF ch = '{' THEN
BEGIN REPEAT getc UNTIL ch = '}'; GOTO 1 END
END; (* getch *)
PROCEDURE gen(c : char; l,r : integer);
BEGIN (* gen *)
cx := cx + 1;
WITH code[cx] DO
BEGIN op := c; left := l; right := r END
END; (* gen *)
PROCEDURE expression;
VAR left : integer;
PROCEDURE and_expression;
VAR left : integer;
PROCEDURE term;
VAR left : integer;
PROCEDURE factor;
BEGIN (* factor *)
IF ch IN ['A'..'Z','a'..'z','0','%','$'] THEN
BEGIN gen(ch,0,0); getch END
ELSE IF ch = '(' THEN
BEGIN getch; expression; IF ch = ')' THEN getch END
ELSE IF ch = '''' THEN
BEGIN getc; gen('''',0,ord(ch)); getch END;
WHILE ch IN ['*','+','#','?','>'] DO
BEGIN gen(ch,0,cx); getch END
END; (* factor *)
BEGIN (* term *)
factor;
IF ch IN ['A'..'Z','a'..'z','0','%','$','(',''''] THEN
BEGIN left := cx; term; gen('_',left,cx) END
END; (* term *)
BEGIN (* and_expression *)
term;
IF ch = '&' THEN
BEGIN getch; left := cx; and_expression; gen('&',left,cx) END
END; (* and_expression *)
BEGIN (* expression *)
and_expression;
IF ch = '|' THEN
BEGIN getch; left := cx; expression; gen('|',left,cx) END
END; (* expression *)
PROCEDURE show;
CONST gap = 3;
VAR i,length : integer;
BEGIN (* show *)
length := 0;
FOR i := 1 TO p DO
IF ord(s[i]) > 0 THEN length := length + 1;
IF linelength + gap + length < 70
THEN BEGIN write(' ':gap); linelength := linelength + gap END
ELSE BEGIN writeln; linelength := 0 END;
FOR i := 1 TO p DO write(s[i]);
linelength := linelength + length
END; (* show *)
PROCEDURE skip;
BEGIN END;
PROCEDURE call(PROCEDURE cp);
BEGIN cp END;
PROCEDURE exp(t : integer; PROCEDURE cp(PROCEDURE ccp);PROCEDURE ccp);
PROCEDURE putch(c : integer);
BEGIN p := p + 1; s[p] := chr(c); cp(ccp); p := p - 1 END;
PROCEDURE delayccp1;
BEGIN exp(code[t].right,call,ccp) END;
PROCEDURE cpccp;
BEGIN cp(ccp) END;
PROCEDURE rightccp;
BEGIN exp(code[t].right,cp,ccp) END;
PROCEDURE rightcp(PROCEDURE ccp);
BEGIN exp(code[t].right,cp,ccp) END;
PROCEDURE dittoccp;
BEGIN exp(t,cp,ccp) END;
PROCEDURE dittocp(PROCEDURE ccp);
BEGIN exp(t,cp,ccp) END;
BEGIN (* exp *)
IF p < max THEN
WITH code[t] DO
CASE op OF
'a'..'z' : putch(ord(op));
'''' : putch(right);
'A'..'Z' : exp(nonterminals[op],cp,ccp);
(* NEW *) '%' : cp(show); (* abort the ccp *)
(* NEW *) '$' : ccp; (* abort the cp *)
'0' : putch(0);
'*' : BEGIN putch(0); exp(right,dittocp,ccp) END;
'+' : BEGIN exp(right,cp,ccp); exp(right,dittocp,ccp) END;
(* NEW *) '#' : BEGIN exp(right,cp,ccp); exp(right,cp,dittoccp) END;
'?' : BEGIN putch(0); exp(right,cp,ccp) END;
(* NEW *) '>' : cp(delayccp1);
'_' : exp(left,rightcp,ccp);
(* NEW *) '&' : exp(left,cp,rightccp);
'|' : BEGIN exp(left,cp,ccp); exp(right,cp,ccp) END;
END (* CASE *)
END; (* exp *)
BEGIN (* main *)
FOR current := 'A' TO 'Z' DO nonterminals[current] := 0;
cx := 0;
REPEAT
getch;
IF ch IN ['A'..'Z'] THEN
BEGIN (* read production *)
current := ch; getch; IF ch = '=' THEN getch;
expression;
IF NOT (ch IN [';','.']) THEN
writeln('seen "',ch,'"');
nonterminals[current] := cx
END (* read production *)
ELSE IF ch IN ['0'..'9'] THEN
BEGIN
max := 0;
REPEAT
max := 10 * max + ord(ch) - ord('0'); getc
UNTIL NOT (ch IN ['0'..'9']);
p := 0; linelength := 0; exp(nonterminals['S'],call,show);
IF linelength > 0 THEN writeln
END
UNTIL false;
99:
END.
A theorem prover for algebra
In the last section of Chapter 15 it was suggested
that theorem proving in algebra might be done along the lines
of theorem proving in logic.
The following is a listing produced by such a program.
Lines beginning with .. are responses from the program,
other lines are echoed input lines from the file
already shown at the end of the last section of Chapter 15.
a * b + c - d = c + b * a - d.
.. valid
a * b + c - d = c - b * a + d.
.. invalid
(p - q) * (r - s) = pr - ps - qr + qs.
.. valid
(p - q) * (r - s) = pr - ps - sr + sq.
.. invalid
pppq * qr * ssr = pppqqrrss.
.. valid
pppq * qr * sssr = pppqqrrss.
.. invalid
(2 + 3) * 4 = 8 + 12.
.. valid
(2 + 3) * 4 = 21.
.. invalid
(2a + 3b) * 4c = 8ac + 12bc.
.. valid
(2a + 3b) * 4c = 8ac + 15bc.
.. invalid
(aaa + aab)/(aa) = a + b.
.. valid
(aaaa + aab)/(aa) = a + b.
.. invalid
(a^2 + 2ab + b^2) ^ 3 = (a + b) ^ 6.
.. valid
(a^2 + ab + b^2) ^ 3 = (a + b) ^ 6.
.. invalid
abbccc - c^3 b^2 a = 0 !
.. valid
abbccc - c^2 b^2 a^2 = 0 !
.. invalid, countermodel when the following is nonzero:
+ab^2c^3 -a^2b^2c^2
(a^3 b^2 - (bc)^3) ^ 4 =
6 * (a^6 b^10 c^6) + b^12 c^12 + a^12 b^8
- 4 * (a^9 b^9 c^3) - 4 * (a^3 b^11 c^9) !
.. valid
(a^3 b^2 - (bc)^3) ^ 4 =
6 * (a^6 b^10 c^6) + b^10 c^15 + a^8 b^10
- 2 * (a^9 b^9 c^3) - 4 * (a^3 b^11 c^9) !
.. invalid, countermodel when the following is nonzero:
+a^12b^8 -2a^9b^9c^3 +b^12c^12 -b^10c^15 -a^8b^10
Writing a grammar and then a recursive descent parser
should be entirely straightforward.
It would be possible to allow for the unlikely case
of all 26 potential variables to be used.
However, some searching will be more efficient if only
a smaller number, say 8, is allowed.
Then any variables that actually occur in an equation
will have to be mapped onto the first few positive integers,
and, for writing, these will have to be mapped back
to variables.
This processing has to be done inside procedure factor,
on the first occurrence of a given variable.
First occurrences result in the two maps being augmented:
one which assigns an ordinal number to the lower case letter,
and one which assigns lower case letters to such numbers.
For code generation
the ordinal number of the variable is used.
Numerals generate numeric nodes.
All binary operators generate binary tree nodes,
this includes exponentiation and equality.
After reading an equation and generating code for it,
the main program has to initialise
some global variables and then
pass control to the recursive interpreter.
On return the main program inspects those
variables to determine whether the equation was valid or not.
The principal variable is a table,
initially empty, of assignments of powers to variables,
together with integer coefficients.
On return the table will be non-empty,
but if all coefficients are zero because
they have been cancelled,
then the equation was valid.
Another variable is a buffer which will contain
assignments of powers to the variables to be collected for each path.
The buffer is later used by the interpreter to
pass information about the current path to
the table.
In the main program the buffer has to be initialised to
zero power for each variable.
It would seem that a small ARRAY is the appropriate data
structure,
but it is necessary to search the table for any previous
occurrence of the buffer,
and Pascal does not allow comparison of ARRAYs.
However, it does allow comparison of strings,
which are PACKEDARRAYs of characters.
So, the buffer and the power assignments to variables
in the table are implemented as strings,
and some character in the middle of the range is
treated as zero.
The interpreter uses the tree code as one parameter,
a continuation as another,
and for the sign and the exponent of an expression
two further parameters which will only have the values -1 or 1.
The required cases have already been outlined
in the last section of Chapter 15.
Only the case for variables is a little tricky
because the buffer is implemented as a string.
So, arithmetic on the power for the particular
variable is actually character manipulation.
The initial global continuation will eventually
be executed,
it is a procedure which updates the table of powers.
First it searches the table for the
content of the current buffer.
If it is not there already,
a new entry is made using
as the coefficient the sign of the current buffer.
That sign is passed to the procedure as a parameter.
It is is there already,
the coefficient for that assignment of powers in the table
is incremented or decremented according to the
sign of the current buffer.
The following is the Pascal source:
PROGRAM algebra(input,output);
LABEL 1, 99;
CONST
interactive = false;
maxcode = 100;
maxvars = 8;
maxproducts = 100;
zero = 100; (* do not change *)
TYPE
message = PACKED ARRAY [1..30] OF char;
varnames = 'a'..'z';
polarity = -1..1; (* never 0 *)
powertype = PACKED ARRAY[1..maxvars] OF char;
(* this is a pretend string to allow comparisons *)
VAR
ch : char;
occurrences : SET OF varnames;
ordinals : ARRAY[varnames] OF integer;
translations : ARRAY [1..maxvars] OF char;
lastvar : integer;
code : ARRAY[1..maxcode] OF
RECORD op : char; left,right : integer END;
lastcode : integer;
producttable : ARRAY[0..maxproducts] OF
RECORD prod : powertype; coeff : integer END;
last_prodtable : integer;
buff : powertype;
show_countermodel,told_countermodel : boolean;
i,j,x : integer;
PROCEDURE error(mes : message);
BEGIN (* error *)
writeln;
IF ch <> ' ' THEN
BEGIN write('seen "',ch,'" when '); readln END;
writeln(mes);
GOTO 1
END; (* error *)
PROCEDURE getc;
BEGIN (* getc *)
IF eof THEN GOTO 99;
IF eoln
THEN BEGIN readln; IF NOT interactive THEN writeln; ch := ' ' END
ELSE BEGIN read(ch); IF NOT interactive THEN write(ch) END
END; (* getc *)
PROCEDURE getch;
BEGIN (* getch *)
REPEAT getc UNTIL ch > ' '
END; (* getch *)
PROCEDURE generate(o : char; l,r : integer);
BEGIN (* generate *)
lastcode := lastcode + 1;
WITH code[lastcode] DO
BEGIN op := o; left := l; right := r END
END; (* generate *)
(* - - - - - T R A N S L A T O R - - - - - *)
PROCEDURE equation;
VAR saveleft : integer;
PROCEDURE expression;
VAR savech : char; saveleft : integer;
PROCEDURE term;
VAR savech : char; saveleft : integer;
PROCEDURE factor;
VAR num,saveleft : integer;
BEGIN (* factor *)
CASE ch OF
'a'..'z' :
BEGIN
IF NOT (ch IN occurrences) THEN
BEGIN
IF lastvar = maxvars THEN
error('too many variables ');
occurrences := occurrences + [ch];
lastvar := lastvar + 1;
ordinals[ch] := lastvar;
translations[lastvar] := ch
END;
generate(ch,0,ordinals[ch]);
getch
END;
'0'..'9' :
BEGIN
num := ord(ch) - ord('0');
getc;
IF ch IN ['0'..'9'] THEN
BEGIN
num := 10 * num + ord(ch) - ord('0');
getch
END
ELSE
IF ch <= ' ' THEN getch;
generate('#',0,num)
END;
'(' :
BEGIN
getch;
expression;
IF ch = ')' THEN getch ELSE
error('")" expected ')
END;
OTHERWISE
error('factor expected ')
END; (* CASE *)
IF ch = '^' THEN
BEGIN
saveleft := lastcode; getch;
IF NOT (ch IN ['0'..'9']) THEN
error('exponent must be numeral ');
factor;
WITH code[lastcode] DO
IF op = '^' THEN
error('repeated "^" not allowed ')
ELSE
BEGIN op := '^'; left := saveleft END
END
END; (* factor *)
BEGIN (* term *)
factor;
WHILE ch IN ['*','/','a'..'z','0'..'9','('] DO
BEGIN
IF NOT(ch IN ['*','/']) THEN savech := '*' ELSE
BEGIN savech := ch; getch END;
saveleft := lastcode;;
factor;
generate(savech,saveleft,lastcode)
END
END; (* term *)
BEGIN (* expression *)
term;
WHILE ch IN ['+','-'] DO
BEGIN
savech := ch; getch; saveleft := lastcode;;
term;
generate(savech,saveleft,lastcode)
END
END; (* expression *)
BEGIN (* equation *)
expression;
IF ch = '=' THEN getch ELSE
error('"=" expected ');
saveleft := lastcode;
expression;
generate('=',saveleft,lastcode)
END; (* equation *)
(* - - - - - I N T E R P R E T E R - - - - - *)
PROCEDURE insert(sign : polarity);
VAR i : integer;
BEGIN
producttable[0].prod := buff; i := last_prodtable;
WHILE producttable[i].prod <> buff DO i := i - 1;
IF i = 0 THEN
BEGIN (* not found, insert *)
IF last_prodtable = maxproducts THEN
error('Too many products ');
last_prodtable := last_prodtable + 1;
WITH producttable[last_prodtable] DO
BEGIN prod := buff; coeff := sign END;
END
ELSE (* found, adjust *)
WITH producttable[i] DO coeff := coeff + sign
END; (* insert *)
PROCEDURE interpret(sign,exp : polarity;
n : integer; PROCEDURE cp(s : polarity));
VAR i : integer;
PROCEDURE mulright(s : polarity);
BEGIN interpret(s,exp,code[n].right,cp) END;
PROCEDURE divright(s : polarity);
BEGIN interpret(s,-exp,code[n].right,cp) END;
PROCEDURE exponents(s : polarity);
BEGIN (* exponents *)
i := i - 1;
IF i < 0 THEN cp(s) ELSE interpret(s,exp,code[n].left,exponents);
i := i + 1
END; (* exponents *)
BEGIN (* interpret *)
WITH code[n] DO
CASE op OF
'a'..'z' :
BEGIN
buff[right] := chr(ord(buff[right]) + exp);
cp(sign);
buff[right] := chr(ord(buff[right]) - exp)
END;
'+','-','=' :
BEGIN
IF exp = -1 THEN
error('division by sum or difference ');
interpret(sign,exp,left,cp);
IF op = '+' THEN interpret(sign,exp,right,cp)
ELSE interpret(-sign,exp,right,cp)
END;
'*' :
interpret(sign,exp,left,mulright);
'/' :
interpret(sign,exp,left,divright);
'#' :
FOR i := 1 TO right DO cp(sign);
'^' :
BEGIN i := right; exponents(sign) END;
END (* CASE *)
END; (* interpret *)
(* - - - - - M A I N - - - - - *)
BEGIN (* main *)
1:
REPEAT
IF interactive THEN write('? '); getch;
lastvar := 0; occurrences := []; lastcode := 0;
equation;
IF ch IN ['.','!'] THEN
BEGIN show_countermodel := ch = '!'; ch := ' ' END
ELSE error('"." or "!" expected ');
IF NOT interactive THEN BEGIN readln; writeln END;
FOR i := 1 TO lastvar DO buff[i] := chr(zero);
last_prodtable := 0;
interpret(1,1,lastcode,insert);
write(' .. ');
told_countermodel := false;
i := 0;
WHILE i < last_prodtable DO
BEGIN
i := i + 1;
WITH producttable[i] DO
IF coeff <> 0 THEN
BEGIN
IF NOT told_countermodel THEN
BEGIN
write('invalid');
IF show_countermodel THEN
BEGIN
writeln(', countermodel when ',
'the following is nonzero:');
write(' ')
END
ELSE
i := last_prodtable; (* ESCAPE LOOP *)
told_countermodel := true
END;
IF show_countermodel THEN
BEGIN
IF coeff = 1 THEN write('+')
ELSE IF coeff = -1 THEN write('-')
ELSE write(coeff:0);
FOR j := 1 TO lastvar DO
BEGIN
x := ord(prod[j]) - zero;
IF x <> 0 THEN
BEGIN
write(translations[j]);
IF x <> 1 THEN write('^',x:0)
END
END;
write(' ')
END (* IF *)
END (* IF *)
END; (* WHILE *)
IF NOT told_countermodel THEN write('valid');
writeln
UNTIL false;
99:
END. (* main *)
S5 modal logic tableaux
The program developed in this section is a theorem prover for the S5
modal logic as suggested in an exercise in Chapter 15.
The necessity and possibility operators are N and P, in other
respects the syntax is familiar. An interactive session would look
as follows, note that at most one counter-model is shown.
Na > a.
.. S5-valid
a > Pa.
.. S5-valid
a > Na.
.. not S5-valid, countermodel -
A: +a
B: -a
Na > NNa.
.. S5-valid
PPa > Pa.
.. S5-valid
PNa > Na.
.. S5-valid
P(a v b) = (Pa v Pb).
.. S5-valid
N(a v b) = (Na v Nb).
.. not S5-valid, countermodel -
A: -a +b
B: +a -b
N(a & b) = (Na & Nb).
.. S5-valid
N(a v -a).
.. S5-valid
N( (a v b) & (a > c) & (b > d) > (c v d) ).
.. S5-valid
N( (a v b) & (a > c) & (b > d) > (c & d) ).
.. not S5-valid, countermodel -
A: +a -b +c -d
-( P(a & -b & -c) & P(-a & b & -c) & P(-a & -b & c) ).
.. not S5-valid, countermodel -
A: +a -b -c
B: -a +b -c
C: -a -b +c
-( P(a & -b & -c) & P(-a & b & -c) & P(-a & -b & c)
& -a & -b & -c ).
.. not S5-valid, countermodel -
A: -a -b -c
B: +a -b -c
C: -a +b -c
D: -a -b +c
(Na > b) = (P-b > N-a) ?
1 a 0 0
2 N 0 1
3 - 0 2
4 b 0 0
5 # 3 4
6 b 0 0
7 - 0 6
8 P 0 7
9 - 0 8
10 a 0 0
11 - 0 10
12 N 0 11
13 # 9 12
14 & 5 13
15 # 5 13
16 - 0 15
17 # 14 16
goal = F world = A delaying = T 17 # 14 16
goal = F world = A delaying = T 14 & 5 13
goal = F world = A delaying = T 5 # 3 4
goal = F world = A delaying = T 3 - 0 2
goal = T world = A delaying = T 2 N 0 1
goal = F world = A delaying = T 4 b 0 0
goal = F world = A delaying = T 16 - 0 15
goal = T world = A delaying = T 15 # 5 13
goal = T world = A delaying = T 5 # 3 4
goal = T world = A delaying = T 3 - 0 2
goal = F world = A delaying = T 2 N 0 1
goal = F world = A delaying = T 1 a 0 0
goal = T world = A delaying = F 2 N 0 1
goal = T world = A delaying = T 1 a 0 0
goal = F world = B delaying = T 1 a 0 0
goal = T world = A delaying = F 2 N 0 1
goal = T world = A delaying = T 1 a 0 0
goal = T world = B delaying = T 1 a 0 0
goal = T world = A delaying = T 4 b 0 0
goal = T world = A delaying = T 13 # 9 12
goal = T world = A delaying = T 9 - 0 8
goal = F world = A delaying = T 8 P 0 7
goal = F world = A delaying = F 8 P 0 7
goal = F world = A delaying = T 7 - 0 6
goal = T world = A delaying = T 6 b 0 0
goal = T world = A delaying = T 12 N 0 11
goal = T world = A delaying = F 12 N 0 11
goal = T world = A delaying = T 11 - 0 10
goal = F world = A delaying = T 10 a 0 0
goal = T world = A delaying = F 2 N 0 1
goal = T world = A delaying = T 1 a 0 0
goal = F world = A delaying = T 13 # 9 12
goal = F world = A delaying = T 9 - 0 8
goal = T world = A delaying = T 8 P 0 7
goal = T world = A delaying = T 7 - 0 6
goal = F world = A delaying = T 6 b 0 0
goal = F world = A delaying = T 12 N 0 11
goal = F world = A delaying = T 11 - 0 10
goal = T world = A delaying = T 10 a 0 0
goal = F world = A delaying = T 16 - 0 15
goal = T world = A delaying = T 15 # 5 13
goal = T world = A delaying = T 5 # 3 4
goal = T world = A delaying = T 3 - 0 2
goal = F world = A delaying = T 2 N 0 1
goal = F world = A delaying = T 1 a 0 0
goal = F world = B delaying = T 1 a 0 0
.. not S5-valid, countermodel -
A: +a -b
B: -a
As the printed internal code reveals,
the two input operators > and =
of the input language are replaced by equivalent though slightly longer
code using just the other operators. This was done solely for variety,
it makes the tableau generator slightly shorter but also slightly less
efficient. The same method could have been used to eliminate
one of the two modal operators.
The parser uses recursive descent,
but instead of four procedures factor, term, expression
and formula, only one is used which takes
a small integer 0, 1, 2, 3
as a parameter to represent the precedence of operators that would
be accepted.
Note that as in Prolog, low numbers represent stronger binding power ---
and one might argue that the numbers really represent
not the binding power of the operator but
the length of the scope of the operators.
The theorem prover is again based on the tableau method,
it attempts to find counter-models to the input formula.
It works by maintaining a collection of possible worlds
A, B, C and so on.
The first of these, A, is the actual world,
it is present in any model,
and any non-modal formulas are made true or false in that world.
When it is required to make a possibility formula true,
first an attempt is made to use one of the existing worlds,
and then a new world is created in a further attempt.
In terms of the theorem prover for monadic logic in Chapter 15,
this amounts to attempting small models first,
with as few worlds as possible.
When it is required to make a necessity formula true,
this is done in two stages.
Initially the formula is delayed because a global boolean
variable is set to true.
The delaying is done by calling the continuation
which itself takes a continuation --- in this case
a local procedure to resume the delayed formula.
Eventually there are only delayed formulas waiting,
and now their actual processing begins:
For each of the existing worlds each of the delayed
necessity formulas has to be made true.
Much of the detail is really very similar to the theorem
prover for monadic logic.
However, there is one important difference.
In the monadic logic prover all required individuals
are created first and then an attempt is made to make all
universal formulas true of them.
In this attempt no further individuals could be created,
essentially because the syntax chosen does not allow for
nested quantification.
The situation is quite different here, though,
because modal operators can be nested.
Hence when an attempt is made to make necessity formulas
true in all worlds that exist at the moment,
this might involve subformulas that require the creation
of further possible worlds,
and these have to be checked against the delayed necessity formulas, too.
The source is as follows:
PROGRAM s5_modal_logic(input,output);
LABEL 1,99;
CONST
maxcode = 200;
actualworld = 'A'; maxworld = 'Z';
TYPE
message = PACKED ARRAY [1..30] OF char;
VAR
ch : char;
code : ARRAY [1..maxcode] OF
RECORD op : char; left,right : integer END;
cx,i : integer;
worlds : ARRAY [actualworld .. maxworld] OF
ARRAY [boolean] OF SET OF 'a' .. 'z';
c,lastworld : char;
delaying : boolean;
tracing : boolean;
PROCEDURE error( mes : message);
BEGIN
writeln('seen "',ch,'" when ',mes); readln; GOTO 1
END; (* error *)
PROCEDURE getch;
BEGIN
REPEAT
IF eof THEN GOTO 99;
IF eoln
THEN BEGIN readln; writeln; ch := ' ' END
ELSE BEGIN read(ch); write(ch) END
UNTIL ch > ' '
END; (* getch *)
PROCEDURE generate(o : char; l,r : integer);
BEGIN
cx := cx + 1;
WITH code[cx] DO
BEGIN op := o; left := l; right := r END
END; (* generate *)
PROCEDURE formula(precedence : integer);
VAR c : char; cx1,cx2 : integer;
BEGIN
CASE precedence OF
0 : (* "factor" *)
CASE ch OF
'a'..'z' :
BEGIN generate(ch,0,0); getch END;
'-','P','N' :
BEGIN c := ch; getch; formula(0); generate(c,0,cx) END;
'(' :
BEGIN
getch; formula(3);
IF ch = ')' THEN getch ELSE
error('operator or ")" expected ')
END;
OTHERWISE
error('factor expected ');
END; (* CASE *)
1,2 : (* "term", "expression" *)
BEGIN
formula(precedence - 1);
WHILE (precedence = 1) AND (ch = '&') OR
(precedence = 2) AND (ch = 'v') DO
BEGIN
IF ch = 'v' THEN c := '#' ELSE c := '&';
cx1 := cx; getch;
formula(precedence - 1); generate(c,cx1,cx)
END;
END;
3 : (* "formula" *)
BEGIN
formula(2);
IF ch = '>' THEN
BEGIN
generate('-',0,cx); cx1 := cx; getch;
formula(3); generate('#',cx1,cx)
END
ELSE IF ch = '=' THEN
BEGIN (* a=b => (a&b)v-(avb) *)
cx1 := cx; getch; formula(3); cx2 := cx;
generate('&',cx1,cx2);
generate('#',cx1,cx2); generate('-',0,cx);
generate('#',cx-2,cx)
END
END;
END (* CASE *)
END; (* formula *)
PROCEDURE stopdelaying(PROCEDURE cp);
VAR save_delaying : boolean; save_lastworld : char;
BEGIN
save_delaying := delaying; save_lastworld := lastworld;
delaying := false; cp;
delaying := save_delaying; lastworld := save_lastworld
END; (* stopdelaying *)
PROCEDURE show;
VAR w,c : char;
BEGIN
writeln(' .. not S5-valid, countermodel -');
FOR w := actualworld TO lastworld DO
BEGIN
write(w,': ');
FOR c := 'a' TO 'z' DO
IF c IN worlds[w,true] THEN write(' +',c) ELSE
IF c IN worlds[w,false] THEN write(' -',c);
writeln;
worlds[w,true] := []; worlds[w,false] := []
END;
writeln; GOTO 1
END; (* show *)
PROCEDURE make(g : boolean; w : char; f : integer;
PROCEDURE cp(PROCEDURE c);
PROCEDURE ccp);
VAR w1 : char;
PROCEDURE goalright(PROCEDURE c);
BEGIN make(g,w,code[f].right,cp,c) END;
PROCEDURE delayed;
PROCEDURE call(PROCEDURE c);
BEGIN c END;
BEGIN delaying := false; make(g,w,f,call,ccp) END;
PROCEDURE allworlds;
BEGIN
IF w = lastworld THEN cp(ccp) ELSE
BEGIN
w := succ(w);
make(g,w,code[f].right,cp,allworlds);
w := pred(w)
END
END; (* allworlds *)
BEGIN (* make *)
WITH code[f] DO
BEGIN
IF tracing THEN
writeln('goal = ',g:1,' world = ',w,
' delaying = ',delaying:1,f:6,' ',op,left:4,right:4);
CASE op OF
'a' .. 'z' :
IF NOT (op IN worlds[w,NOT g]) THEN
IF op IN worlds[w,g] THEN cp(ccp) ELSE
BEGIN
worlds[w,g] := worlds[w,g] + [op];
cp(ccp);
worlds[w,g] := worlds[w,g] - [op]
END;
'-' :
make(NOT g,w,right,cp,ccp);
'&','#' :
IF (op = '&') = g THEN make(g,w,left,goalright,ccp) ELSE
BEGIN
make(g,w,left,cp,ccp); make(g,w,right,cp,ccp)
END;
'N','P' :
IF (op = 'P') = g THEN
BEGIN
FOR w1 := actualworld TO lastworld DO
make(g,w1,right,cp,ccp);
lastworld := succ(lastworld);
make(g,lastworld,right,cp,ccp);
lastworld := pred(lastworld)
END
ELSE
IF delaying THEN cp(delayed) ELSE
BEGIN
delaying := true; w1 := w;
w := pred(actualworld); allworlds;
delaying := false; w := w1
END
END (* CASE *)
END (* WITH *)
END; (* make *)
BEGIN (* main *)
FOR c := actualworld TO maxworld DO
BEGIN worlds[c,true] := []; worlds[c,false] := [] END;
1: REPEAT
cx := 0; getch; formula(3);
IF NOT (ch IN ['.','?'])
THEN error('operator or "." expected ')
ELSE tracing := ch = '?';
writeln;
IF tracing THEN
FOR i := 1 TO cx DO
WITH code[i] DO writeln(i:3,' ',op,left,right);
lastworld := actualworld; delaying := true;
make(false,actualworld,cx,stopdelaying,show);
writeln(' .. S5-valid')
UNTIL false;
99:
END. (* main *)
Fourth order recursion for tableaux
This program solves an exercise of Chapter 12.
It uses recursive continuation parsing to implement the semantic tableau method
without internal code.
For simplicity,
input formulas are again built from single characters.
There is no trunk-before-branch optimisation.
The block structure of the program is almost in every detail
dictated by the input grammar and the requirements of recursive continuation parsing.
Hence the main structure is identical to the truth table program
without internal code as given in Chapter 12.
However, a further order is necessary
for the backtracking of the tableau method.
The program is best understood in terms of these design steps:
Step 1 Parsing:
Recursive continuation parsing dictates the following structure
for the parsing procedures.
The first four parsing procedures
correspond to the non-terminals of a conventional grammar.
They each take a continuation as a parameter cp
as a formal parameter for further parsing.
These continuations and the last three parsing procedures
have to be of the same type,
because the last three parsing procedures will serve
as actual parameters.
Step 2 Saving:
The next level introduces local procedures
which save continuations.
These are for saving
negations, conjunctions, disjunctions,
conditionals and equivalences.
They each take two procedures as parameters
which are for verifying their respective components.
Step 3 ver and fal continuations:
The next level introduces procedures for verifying
and falsifying the atoms,
the conjunctions, the disjunctions,
the conditionals and the equivalences.
Those for verifying and falsifying atoms are local to parse_factor,
those for verifying and falsifying
conjunctions, disjunctions, conditionals and equivalences
as local to the corresponding procedures
for saving conjunctions, disjunctions,
conditionals and equivalences.
Step 4 verify-left and verify-right:
The last level introduces local procedures
which serve as continuations
to verify the right part of conjunctions,
to falsify the right part of disjunctions,
to falsify the right part of conditionals,
to verify the right and falsify the right of equivalences.
PROGRAM verify_falsify_cont(input,output);
LABEL 99;
TYPE
message = PACKED ARRAY[1..20] OF char;
VAR
ch : char;
truevars, falsevars : SET OF 'a'..'z';
num_countermodels : integer;
PROCEDURE getch;
BEGIN
REPEAT
IF eof THEN GOTO 99;
read(ch)
UNTIL ch > ' '
END; (* getch *)
PROCEDURE error(mes : message);
BEGIN
writeln('ERROR: seen "',ch,'" when ',mes);
readln
END; (* error *)
PROCEDURE show;
VAR c : char;
BEGIN
IF num_countermodels = 0 THEN
writeln('not tautology, countermodels -');
num_countermodels := num_countermodels + 1;
write(num_countermodels:0,': ');
FOR c := 'a' TO 'z' DO
IF c IN truevars THEN write('+',c,' ') ELSE
IF c IN falsevars THEN write('-',c,' ');
writeln
END; (* show *)
PROCEDURE check_period
(PROCEDURE ver_main_formula(PROCEDURE cp);
PROCEDURE fal_main_formula(PROCEDURE cp));
BEGIN
IF ch <> '.' THEN error('"." expected ');
num_countermodels := 0;
fal_main_formula(show);
IF num_countermodels = 0 THEN
writeln('tautology')
END; (* check_period *)
PROCEDURE parse_formula
(PROCEDURE cp(PROCEDURE ver_ccp(PROCEDURE cccp);
PROCEDURE fal_ccp(PROCEDURE cccp)));
PROCEDURE parse_expression
(PROCEDURE cp(PROCEDURE ver_ccp(PROCEDURE cccp);
PROCEDURE fal_ccp(PROCEDURE cccp)));
PROCEDURE parse_term
(PROCEDURE cp(PROCEDURE ver_ccp(PROCEDURE cccp);
PROCEDURE fal_ccp(PROCEDURE cccp)));
PROCEDURE parse_factor
(PROCEDURE cp(PROCEDURE ver_ccp(PROCEDURE cccp);
PROCEDURE fal_ccp(PROCEDURE cccp)));
VAR at : char;
PROCEDURE check_right_parenthesis
(PROCEDURE ver_ccp(PROCEDURE cccp);
PROCEDURE fal_ccp(PROCEDURE cccp));
BEGIN (* check_right_parenthesis *)
IF ch <> ')' THEN error('")" expected ') ELSE
BEGIN getch; cp(ver_ccp,fal_ccp) END
END; (* check_right_parenthesis *)
PROCEDURE ver_atom(PROCEDURE cccp);
BEGIN (* ver_atom *)
IF NOT (at IN falsevars) THEN
IF at IN truevars THEN cccp ELSE
BEGIN
truevars := truevars + [at];
cccp;
truevars := truevars - [at];
END
END; (* ver_atom *)
PROCEDURE fal_atom(PROCEDURE cccp);
BEGIN (* fal_atom *)
IF NOT (at IN truevars) THEN
IF at IN falsevars THEN cccp ELSE
BEGIN
falsevars := falsevars + [at];
cccp;
falsevars := falsevars - [at];
END
END; (* fal_atom *)
PROCEDURE save_negation
(PROCEDURE ver_negand(PROCEDURE cccp);
PROCEDURE fal_negand(PROCEDURE cccp));
BEGIN cp(fal_negand,ver_negand) END;
BEGIN (* parse_factor *)
CASE ch OF
'a'..'z' :
BEGIN at := ch; getch; cp(ver_atom,fal_atom) END;
'-' :
BEGIN getch; parse_factor(save_negation) END;
'(' :
BEGIN
getch;
parse_formula(check_right_parenthesis)
END;
OTHERWISE
error('factor expected ')
END (* CASE *)
END; (* parse_factor *)
PROCEDURE parse_term2
(PROCEDURE ver_left(PROCEDURE cccp);
PROCEDURE fal_left(PROCEDURE cccp));
PROCEDURE save_conjunction
(PROCEDURE ver_right(PROCEDURE cccp);
PROCEDURE fal_right(PROCEDURE cccp));
PROCEDURE ver_conjunction(PROCEDURE cccp);
PROCEDURE verifyright;
BEGIN ver_right(cccp) END;
BEGIN (* ver_conjunction *)
ver_left(verifyright)
END; (* ver_conjunction *)
PROCEDURE fal_conjunction(PROCEDURE cccp);
BEGIN fal_left(cccp); fal_right(cccp) END;
BEGIN (* save_conjunction *)
cp(ver_conjunction,fal_conjunction)
END; (* save_conjunction *)
BEGIN (* parse_term2 *)
IF ch = '&' THEN
BEGIN getch; parse_term(save_conjunction) END
ELSE cp(ver_left,fal_left)
END; (* parse_term2 *)
BEGIN (* parse_term *)
parse_factor(parse_term2)
END; (* parse_term *)
PROCEDURE parse_expression2
(PROCEDURE ver_left(PROCEDURE cccp);
PROCEDURE fal_left(PROCEDURE cccp));
PROCEDURE save_disjunction
(PROCEDURE ver_right(PROCEDURE cccp);
PROCEDURE fal_right(PROCEDURE cccp));
PROCEDURE ver_disjunction(PROCEDURE cccp);
BEGIN ver_left(cccp); ver_right(cccp) END;
PROCEDURE fal_disjunction(PROCEDURE cccp);
PROCEDURE falsifyright;
BEGIN fal_right(cccp) END;
BEGIN (* fal_disjunction *)
fal_left(falsifyright)
END; (* fal_disjunction *)
BEGIN (* save_disjunction *)
cp(ver_disjunction,fal_disjunction)
END; (* save_disjunction *)
BEGIN (* parse_expression2 *)
IF ch IN ['v','#'] THEN
BEGIN getch; parse_expression(save_disjunction) END
ELSE cp(ver_left,fal_left)
END; (* parse_expression2 *)
BEGIN (* parse_expression *)
parse_term(parse_expression2)
END; (* parse_expression *)
PROCEDURE parse_formula2
(PROCEDURE ver_left(PROCEDURE cccp);
PROCEDURE fal_left(PROCEDURE cccp));
PROCEDURE save_conditional
(PROCEDURE ver_right(PROCEDURE cccp);
PROCEDURE fal_right(PROCEDURE cccp));
PROCEDURE ver_conditional(PROCEDURE cccp);
BEGIN fal_left(cccp); ver_right(cccp) END;
PROCEDURE fal_conditional(PROCEDURE cccp);
PROCEDURE falsify_consequent;
BEGIN fal_right(cccp) END;
BEGIN (* fal_conditional *)
ver_left(falsify_consequent)
END; (* fal_conditional *)
BEGIN (* save_conditional *)
cp(ver_conditional,fal_conditional)
END; (* save_conditional *)
PROCEDURE save_equivalence
(PROCEDURE ver_right(PROCEDURE cccp);
PROCEDURE fal_right(PROCEDURE cccp));
PROCEDURE ver_equivalence(PROCEDURE cccp);
PROCEDURE verify_right;
BEGIN ver_right(cccp) END;
PROCEDURE falsify_right;
BEGIN fal_right(cccp) END;
BEGIN (* ver_equivalence *)
ver_left(verify_right);
fal_left(falsify_right)
END; (* ver_equivalence *)
PROCEDURE fal_equivalence(PROCEDURE cccp);
PROCEDURE verify_right;
BEGIN ver_right(cccp) END;
PROCEDURE falsify_right;
BEGIN (* falsify_right *)
fal_right(cccp)
END; (* falsify_right *)
BEGIN (* fal_equivalence *)
ver_left(falsify_right);
fal_left(verify_right)
END; (* fal_equivalence *)
BEGIN (* save_equivalence *)
cp(ver_equivalence,fal_equivalence)
END; (* save_equicvalence *)
BEGIN (* parse_formula2 *)
IF ch = '>' THEN
BEGIN getch; parse_formula(save_conditional) END
ELSE IF ch = '=' THEN
BEGIN getch; parse_formula(save_equivalence) END
ELSE cp(ver_left,fal_left)
END; (* parse_formula2 *)
BEGIN (* parse_formula *)
parse_expression(parse_formula2)
END; (* parse_formula *)
BEGIN (* main *)
truevars := []; falsevars := [];
REPEAT
write('?- '); getch;
parse_formula(check_period)
UNTIL false;
99:
writeln(clock:0,' milliseconds')
END. (* main *)
As an experiment, the program and three more conventional versions
(using an internal data structure) were modified to read a formula once
but forced to determine whether it is a tautology 1000 times.
For the input
(p v q) & (p > r) & (q > s) > (r v s)
the complex constructive dilemma,
the time for the program was 9450 milliseconds,
for the various conventional programs it was 13870, 21290, and 25460
milliseconds.
So it does seem that there is some saving.
Developing this program was aided significantly
by the rigorous type checking done by
Digital Equipment Corporation's VAX Pascal compiler.