proofs
Rijk-Jan van Haaften
rjchaaft@cs.uu.nl
Wed, 17 Oct 2001 20:06:49 +0200
I will attempt to explain how I would work out the
problem. If my description is incomplete or wrong
sure some more experienced reader will tell us.
>I want to learn how to go about proving things like
> (p >>= j) >= k == p >>= (\x->(j x >>= k))
> where
> p >>= k = \s0 -> let (s1, a) = p s0
> in k a s1
First, I give the results of my (3-minute) analysis:
Substitution of the given definition leads for the left-hand side to
(\s0 ->
let {
(s1, a) = p s0
(s2, b) = j a s1
} in
k b s2
)
The right-hand side is
(\s0 ->
let {
(s1, a) = p s0
(s2, b) = j a s1
} in
k b s2
)
These are clearly the same
I used 3 main properties for the process:
1. Renaming of variables
for example:
(\x -> x + y)
==
(\z -> z + y)
Changing x to z is legal here. However,
we can not rename x to y because y
is already used. So be carefull with renaming
actions.
2. Lifting local let definitions to a higher level
let
f =
let
g = gExpr
in
fExpr
in
expr
can be translated into
let
g = gExpr
f = fExpr
in
expr
The definition of g which is local for f in the first
expression is made more global in the second
one.
The translation back is not always possible
(impossible if g and f are mutual recursive,
that is: use each other)
3. Lambda elimination
(\x -> x + 3) y
==
y + 3
---------------------------------------------------
Complete example (left-hand side)
---------------------------------------------------
>I want to learn how to go about proving things like
> (p >>= j) >= k == p >>= (\x->(j x >>= k))
> where
> p >>= k = \s0 -> let (s1, a) = p s0
> in k a s1
(p >== j)
equals
(\s0 -> let (s1, a) = p s0 in j a s1)
rename s0, s1 and a to s2, s3 and b resp.
(\s2 -> let (s3, b) = p s2 in j b s3)
This avoids name-conflicts later on.
Say this last expression is called f (just to make reading
easier), so
f == (\s2 -> let (s3, b) = p s2 in j b s3)
f >= k
equals
(\s0 -> let (s1, a) = f s0 in k a s1)
Now substitute de definition for f
(\s0 ->
let
(s1, a) = (\s2 -> let (s3, b) = p s2 in j b s3) s0
in
k a s1
)
Lambda elimination is the next step.
((\s2 -> ...) s0) is candidate for this step.
The result is
(\s0 ->
let (s1, a) =
let (s3, b) = p s0 in j b s3
in
k a s1
)
This was the step which eliminated s2, so we can rename
s3 to s2 now, just to remove the gap between s1 and s3:
(\s0 ->
let (s1, a) =
let
(s2, b) = p s0
in j b s2
in
k a s1
)
At this point, lifting a local definition to a higher level comes in view:
let
(s1, a) =
let
(s2, b) = p s0
in
j b s2
in
...
is the same as
let
(s2, b) = p s0
(s1, a) = j b s2
in
...
This yields
(\s0 ->
let
(s2, b) = p s0
(s1, a) = j b s2
in
k a s1
)
Which is the result above, except that
the names of s1 and s2 are swapped.
This makes no real difference though and
a renaming action is enough to fix it.
Now, try to write out the right-hand side
yourself. These three transformations are
enough for now.
There are lots of such equality (or half-
equality) transformations, but I don't know
concrete resources. Others on the mailing
list can probably point out some good
resources.
Rijk-Jan