<br><div class="gmail_quote">On Sun, May 4, 2008 at 12:48 PM, PR Stanley <<a href="mailto:prstanley@ntlworld.com">prstanley@ntlworld.com</a>> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class="Ih2E3d"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Hi<br>
What on earth is unapplying function definitions?<br>
The following is taken from chapter 13 of the Hutton book:<br>
"...when reasoning about programs, function definitions can be both<br>
applied from left to right and unapplied from right to left."<br>
</blockquote>
<br>
Well, because of referential transparency, we can say that the left<br>
hand side of a function is exactly equal to the right hand side.<br>
Thus, we can instead of applying functions, and making progress<br>
towards a normal form, unapply them and get further away from a normal<br>
form... for example:<br>
<br>
5 = head [5,6,7,8,9] = head ([5,6] ++ [7] ++ [8,9]) = head (([] ++ [5]<br>
++ [6]) ++ [7] ++ [8,9]) .......<br>
<br>
There are of course an infinite number of ways of doing this, so it's<br>
usually only interesting, if we have some reason for applying a<br>
specific expansion.<br>
<br>
</div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
What is the normal form?<br>
</blockquote></blockquote><div><div></div><div class="Wj3C7c">
</div></div></blockquote><div><br>Essentially, a normal form is an expression where there are no more function applications that can be evaluated. For example, the expression '5' is a normal form; 'succ 5' is not a normal form since the succ can be applied to the 5, producing the normal form 6.<br>
<br>To give another example of what Hutton means, suppose we are given the function definition<br><br>head (x:xs) = x<br><br>Then if we have the expression 'head (1:2:[])', noting that this matches the left-hand side of the definition of head, we can apply that definition to produce the equivalent expression '1'. Given the expression '2', on the other hand, and noting that this matches the *right*-hand side of the definition of head, we can *unapply* the definition to produce the equivalent expression 'head (2:[4,5,6])' (for example). Applying a function definition (moving from the left side of the definition to the right side) brings us closer to a normal form, since there's one less function application. "Unapplying" a function definition (moving from the right side to the left side) moves us further away from normal form since we have introduced another function application.<br>
<br>Of course, you would never want an evaluator to "unapply" functions in this way, but when reasoning about programs as humans, it can sometimes be useful in proving things.<br><br>Does that help clear things up?<br>
-Brent<br> </div></div>