[comp.lang.misc] Reply to Miranda query

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