sjt@eagle.ukc.ac.uk (S.J.Thompson) (08/10/88)
In reply to the query: > I have been reading about miranda and am trying to understand a simple > program given in the article "An Overview of Miranda" from SIGPLAN > Notices, December 1986. It should be easy for anyone who has actually > programmed in miranda and I'm wondering if someone would mind giving > me a hand. The problem is: > > answer = twice twice twice suc 0 > twice f x = f (f x) > suc x = x + 1 > > I'm trying to apply partial paramaterization at each step and get an > exact picture of what's going on as far as the execution mechanism is > concerned, but keep coming up with weird results. I think the > parenthesis are confusing me. I am assuming that functions inside > parenthesis should be applied to arguments and then parenthesis > removed. I know I am doing something simple fundamentally wrong but > can't figure it out. Has anyone looked at this before? > > Thanks. > > Mark Feldman > Fujitsu Laboratories Ltd. Kawasaki, Japan > feldmark@hanako.stars.flab.fujitsu.junet (Japan) > feldmark%hanako.stars.flab.fujitsu.junet@uunet.uu.net (USA) The following is a Miranda script which will generate the sequence of reductions according to the usual reduction rules for function expressions. Appended at the end is a print out of the results. Simon Thompson, University of Kent at Canterbury sjt@ukc ||----------------------------------------------------------------------|| || The best way to see how the term || || twice twice twice suc 0 || || behaves under reduction is to write a Miranda script to || || generate the reductions for you: || || We start with an algebraic type of terms, thus... || ||----------------------------------------------------------------------|| term ::= T | S | Num num | App term term ||----------------------------------------------------------------------|| || ... and then explain how a one-step reduction of those terms || || is performed. The only terms which change are Applications, and || || in these we have a rule for the twice function, and a rule || || for the successor - if we fail to have a top-level reduction || || we either reduce the function part of the application, or the || || argu,ent part. || ||----------------------------------------------------------------------|| reduce :: term -> term reduce T = T reduce S = S reduce (Num n) = Num n reduce (App (App T f) x) = (App f (App f x)) reduce (App S (Num n)) = Num (n+1) reduce (App t1 t2) = App r1 t2 , t1 ~= r1 = App t1 r2 , otherwise where r1 = reduce t1 r2 = reduce t2 ||----------------------------------------------------------------------|| || test is the (concrete version of) the term in question || ||----------------------------------------------------------------------|| test :: term test = App (App (App (App T T) T) S) (Num 0) ||----------------------------------------------------------------------|| || fixpt takes us to the first fixed point of the sequence || || x , f x , f (f x), ... || ||----------------------------------------------------------------------|| fixpt :: (* -> *) -> * -> * fixpt f x = n , n=x = fixpt f n , otherwise where n = f x ||----------------------------------------------------------------------|| || and fixsq generates the whole sequence to that fixed point || ||----------------------------------------------------------------------|| fixsq :: (* -> *) -> * -> [*] fixsq f x = [x] , n=x = x : (fixsq f n) , otherwise where n = f x ||----------------------------------------------------------------------|| || pretty_fixsq gives a readable version of the fixsq, so to see || || exactly how the reduction proceeds, type || || pretty_fixsq test || || in the Miranda system. || ||----------------------------------------------------------------------|| pretty_fixsq :: term -> [char] pretty_fixsq t = concat (map (add_nl . print_term) (fixsq reduce t)) where add_nl x = x ++ "\n" print_term :: term -> [char] print_term (Num n) = show n print_term T = "twice" print_term S = "suc" print_term (App t1 t2) = print1 ++ " " ++ print2 where print1 = print_term t1 print2 = p2 , simple t2 = "(" ++ p2 ++ ")" , otherwise p2 = print_term t2 simple (Num n) = True simple T = True simple S = True simple (App x y) = False ||----------------------------------------------------------------------|| || The end of the Miranda script. || ||----------------------------------------------------------------------|| The sequence of reductions which we generate is as follows - remember that function application associates to the LEFT, so (f g x) means (f g) x, for example. twice twice twice suc 0 twice (twice twice) suc 0 twice twice (twice twice suc) 0 twice (twice (twice twice suc)) 0 twice (twice twice suc) (twice (twice twice suc) 0) twice twice suc (twice twice suc (twice (twice twice suc) 0)) twice (twice suc) (twice twice suc (twice (twice twice suc) 0)) twice suc (twice suc (twice twice suc (twice (twice twice suc) 0))) suc (suc (twice suc (twice twice suc (twice (twice twice suc) 0)))) suc (suc (suc (suc (twice twice suc (twice (twice twice suc) 0))))) suc (suc (suc (suc (twice (twice suc) (twice (twice twice suc) 0))))) suc (suc (suc (suc (twice suc (twice suc (twice (twice twice suc) 0)))))) suc (suc (suc (suc (suc (suc (twice suc (twice (twice twice suc) 0))))))) suc (suc (suc (suc (suc (suc (suc (suc (twice (twice twice suc) 0)))))))) suc (suc (suc (suc (suc (suc (suc (suc (twice twice suc (twice twice suc 0))))))))) suc (suc (suc (suc (suc (suc (suc (suc (twice (twice suc) (twice twice suc 0))))))))) suc (suc (suc (suc (suc (suc (suc (suc (twice suc (twice suc (twice twice suc 0)))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (twice suc (twice twice suc 0))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (twice twice suc 0)))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (twice (twice suc) 0)))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (twice suc (twice suc 0))))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (twice suc 0)))))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc 0))))))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc 1)))))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc 2))))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc 3)))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc 4))))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc 5)))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc (suc 6))))))))) suc (suc (suc (suc (suc (suc (suc (suc (suc 7)))))))) suc (suc (suc (suc (suc (suc (suc (suc 8))))))) suc (suc (suc (suc (suc (suc (suc 9)))))) suc (suc (suc (suc (suc (suc 10))))) suc (suc (suc (suc (suc 11)))) suc (suc (suc (suc 12))) suc (suc (suc 13)) suc (suc 14) suc 15 16