244

1 
Proves about loops and tailrecursive functions


2 
===============================================


3 


4 
Problem A


5 


6 
P = while B1 do S od


7 
Q = while B1 or B2 do S od


8 


9 
Prove P;Q = Q (provided B1, B2 have no side effects)


10 


11 



12 


13 
Looking at the denotational semantics of while, we get


14 


15 
Problem B


16 


17 
[B1]:State>Bool


18 
[B2]:State>Bool


19 
[S ]:State>State


20 
f :State>State


21 


22 
p = fix LAM f.LAM x. if [ B1 ] x then f([ S ] x) else x fi


23 
q = fix LAM f.LAM x. if [ B1 ] x orelse [b2 ] x then f([ S ] x) else x fi


24 


25 
Prove q o p = q rsp. ALL x.q(p(x))=q(x)


26 


27 
Remark: 1. Bool is the threevalued domain {UU,FF,TT} since tests B1 and B2 may


28 
not terminate.


29 
2. orelse is the sequential or like in ML


30 


31 



32 


33 
If we abstract over the structure of stores we get


34 


35 
Problem C


36 


37 
b1:'a > Bool


38 
b2:'a > Bool


39 
g :'a >'a


40 
h :'a >'a


41 


42 
p = fix LAM h.LAM x. if b1(x) then h(g(x)) else x fi


43 
q = fix LAM h.LAM x. if b1(x) orelse b2(x) then h(g(x)) else x fi


44 


45 
where g is an abstraction of [ S ]


46 


47 
Prove q o p = q


48 


49 
Remark: there are no restrictions wrt. definedness or strictness for any of


50 
the involved functions.


51 


52 



53 


54 
In a functional programming language the problem reads as follows:


55 


56 
p(x) = if b1(x)


57 
then p(g(x))


58 
else x fi


59 


60 
q(x) = if b1(x) orelse b2(x)


61 
then q(g(x))


62 
else x fi


63 


64 


65 
Prove: q o p = q


66 


67 


68 



69 


70 
In you like to test the problem in ML (bad guy) you have to introduce


71 
formal parameters for b1,b2 and g.


72 


73 
fun p b1 g x = if b1(x)


74 
then p b1 g (g(x))


75 
else x;


76 


77 


78 
fun q b1 b2 g x = if b1(x) orelse b2(x)


79 
then q b1 b2 g (g(x))


80 
else x;


81 


82 
Prove: for all b1 b2 g .


83 
(q b1 b2 g) o (p b1 g) = (q b1 b2 g)


84 


85 
===========


86 


87 
It took 4 persondays to formulate and prove the problem C in the


88 
Isabelle logic HOLCF. The formalisation was done by conservative extension and


89 
all proof principles where derived from pure HOLCF.


90 


91 


92 


93 


94 


95 


96 


97 
