Download 3-D Graphics / AI Theory

using it in the process of establishing
relationships.
The Eval(s,bi,bo) relation holds iff (if
tion method (called SLD-resolution). In
short-we instantiate a rule by replacing
all of its variables by constants before
Figure 3 - A Trace of Program Exp Execution
whiles executed
1
2
3
4
END
or
& Y
&
x
&
n
&
&
&
&
&
1
&
2
&
&
4
&
&
&
16
256
&
5
2
1
&
2
2
32
&
°
&
&
&
nl
-
2
1
°
LISTINQ
By Paul 1. Voda
CompIete Logic systems Inc.
741 Blueridge Ave.
N. Vancouver, B.C. V7R 2J5 Canada
and only if) the program, liS," executed
under the variable bindings given by
''bi'' stops with, possibly new, variable
bindings, ''bo.''
We use a string representation of
programs to emphasize that a program is
a sequence of symbols. Strings are
decomposed with the help of "highpowered" but obvious string patternmatching constructs. Alternatively, we
could have used lists to encode programs
in the so-called abstract syntax.
Variable bindings are lists of variables
coupled with their current values.
For example-
Figure 4 -Eval. Definition
[('x',2),
Val('N',b,v) <- Number ('N' ,v)
Val('V',b,v) <- Select(b,'V',v)
Val('El + E2' ,b,vl+v2) <- Val('El' ,b,vl),
Val('El - E2' ,b,vl-v2) <- Val('El' ,b,vl),
Val('El * E2' ,b,vl*v2) <- Val('El' ,b,vl),
Val('El / E2',b,vl/v2) <- Val('El',b,vl),
Val('El = E2',b,1)
<- Val('El',b,vl),
Val('El = E2' ,b,O)
<- Val('El' ,b,vl),
Val('El < E2' ,b,l)
<- Val('El' ,b,vl),
Val('El < E2' ,b,O)
<- Val('El' ,b,vl),
Editor's note: The symbols, [ and] enclose
a list.
Val('E2' ,b,v2)
Val('E2',b,v2)
Val('E2',b,v2)
Val('E2',b,v2)
Val('E2' ,b,v2),
Val('E2' ,b,v2),
Val('E2' ,b,v2),
Val('E2',b,v2),
Number ('D' ,v) <- Dig('D' ,v)
Number('ND',lO*v+d) <- Dig('D',d), Number('N',v)
Dig('O' ,0) <Dig(' l' ,1) <Dig('9',9) <Select ( [('V' ,v) It),'V' ,v) <Select ( [('W' ,w) It], 'V' ,v) <-
'V' <> 'W', Select(t, 'V' ,v)
Eval('V := E; S' ,bi,bo) <Val('E',bi,v), Newb(bi,'V',v,bb), Eval('S',bb,bo)
Eval('if E then Sl else S2 end; S',bi,bo) <Val('E',bi,O), Eval('S2',bi,bb), Eval('S',bb,bo)
Eval('if E then Sllelse S2 end; S',bi,bo) <Val('E',bi,l), Eval('Sl',bi,bb), Eval('S',bb,bo)
Eval('if E then Sl end; S',bi,bo) <Eval('if E then Sl else end; S',bi,bo)
Eval('while E do Sl end; S',bi,bo) <Eval('if E then Sl while E do Sl end; end; S',bi,bo)
Newb([('V',w) It), 'V', v, [('V',v)lt) <Newb([('W',w) It), 'V', v, [('W',w) Itt)) <Newb(t, 'V' ,v,tt)
END
or
'W' <> 'V',
vl
vl
vl
vl
= v2
v2
v2
= v2
('y',l),
('n',S)]
The relation Select(b,var,val) holds iff
the variable var is associated with the
value val in the bindings b. The relation
Newb(bi,var,val,bo) holds iff the bindings in bo are like bi but with the value
val associated with the variable var. This
relation obviously captures the effect of
the assignment var := val.
The relation Val(exp,b,val) holds iff
the value of expression exp computed
under bindings b is val.
The meaning of programs in L is
given indirectly by the relation Eval.
Nevertheless, this is a perfectly valid approach and the programs are amenable
to mathematical analysis. We can prove
facts about the relation Eval.
For example, let's denote by P the
while loop of the program in Figure 2.
By using induction on the variable n
we can easily prove that-
°
If n >=
and p is the smallest
number of the form p = 2 A k
such that p >= n then,
LISTINQ
Eval(
&
&
'P',
[('y',y),
('x',x),
('n',n),
MICRO CORNUCOPIA, #41, May-June 1988
23