From: S.J.Thompson
Subject: Reply to Miranda query
Date:
Message-ID: <5445@eagle.ukc.ac.uk>
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
> ········@hanako.stars.flab.fujitsu.junet (Japan)
> ········································@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
···@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