Hi, all.
I read the book named "The Formal Semantics of Programming Languages".
It introduces the principle of rule induction and the special principle of it in chapter 4.
However, I couldn't understand the latter. The principle is following.
Let R be a set of rules of the form (X/y), where X is either the empty set or some set
of premises, and y is the conclusion. Let Ir = { y | ||-r y } (i.e. set defined by rules).
Let Q be a property of elements in A. Then
for all elements a in A, Q(a) iff
for all rule instances (X/y) in R, if X is a subset of Ir, y is in A and for all elements x in
the intersection of X and A, Q(x) then Q(y)
The book has two or more syntactic sets.
It says that if one wants to prove a property of one syntactic set, then one need prove
the property only with respect to the set.
example:
I have two syntactic sets, Aexp and Bexp.
BNF of Aexp
a := n(numeral) | X(variable) | a + a
evaluation rules of Aexp
<a1>->m <a2>->n
------------- ------------- (m is the content of X) ------------------------- (m+n =p)
<n> -> n <X> -> m <a1+a2> -> p
BNF of Bexp
b := true | false | a1 = a2 (a1 and a2 are in A)
evaluation rules of Bexp
<a1>->m <a2>->n <a1>->m <a2>->n
-------------------- ---------------------- ------------------------- (m=n) ------------------------- (not m=n)
<true> -> true <false> -> false <a1=a2> -> true <a1=a2> -> false
Now Suppose I want to prove that all programs of Bexp always halt.
Then I need not prove that all programs of Aexp do by the special principle of rule induction.
Why is it?
Or I have mistakes in the understanding?
Thanks,
Sekiyama
