Hi What on earth is unapplying function definitions? The following is taken from chapter 13 of the Hutton book: "...when reasoning about programs, function definitions can be both applied from left to right and unapplied from right to left." Cheers Paul
On 4 May 2008, at 17:33, PR Stanley wrote:
Hi What on earth is unapplying function definitions? The following is taken from chapter 13 of the Hutton book: "...when reasoning about programs, function definitions can be both applied from left to right and unapplied from right to left."
Well, because of referential transparency, we can say that the left hand side of a function is exactly equal to the right hand side. Thus, we can instead of applying functions, and making progress towards a normal form, unapply them and get further away from a normal form... for example: 5 = head [5,6,7,8,9] = head ([5,6] ++ [7] ++ [8,9]) = head (([] ++ [5] ++ [6]) ++ [7] ++ [8,9]) ....... There are of course an infinite number of ways of doing this, so it's usually only interesting, if we have some reason for applying a specific expansion. Bob
Hi What on earth is unapplying function definitions? The following is taken from chapter 13 of the Hutton book: "...when reasoning about programs, function definitions can be both applied from left to right and unapplied from right to left."
Well, because of referential transparency, we can say that the left hand side of a function is exactly equal to the right hand side. Thus, we can instead of applying functions, and making progress towards a normal form, unapply them and get further away from a normal form... for example:
5 = head [5,6,7,8,9] = head ([5,6] ++ [7] ++ [8,9]) = head (([] ++ [5] ++ [6]) ++ [7] ++ [8,9]) .......
There are of course an infinite number of ways of doing this, so it's usually only interesting, if we have some reason for applying a specific expansion.
What is the normal form?
On Sun, May 4, 2008 at 12:48 PM, PR Stanley
Hi
What on earth is unapplying function definitions? The following is taken from chapter 13 of the Hutton book: "...when reasoning about programs, function definitions can be both applied from left to right and unapplied from right to left."
Well, because of referential transparency, we can say that the left hand side of a function is exactly equal to the right hand side. Thus, we can instead of applying functions, and making progress towards a normal form, unapply them and get further away from a normal form... for example:
5 = head [5,6,7,8,9] = head ([5,6] ++ [7] ++ [8,9]) = head (([] ++ [5] ++ [6]) ++ [7] ++ [8,9]) .......
There are of course an infinite number of ways of doing this, so it's usually only interesting, if we have some reason for applying a specific expansion.
What is the normal form?
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. To give another example of what Hutton means, suppose we are given the function definition head (x:xs) = x 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. 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. Does that help clear things up? -Brent
Hi Paul! I'm not sure about the context of Hutton, but maybe "unapplying functions" refers to the principle of extensionality. Leibnitz' rule of the "indiscernibility of identicals" [1] says that if two functions are equal, then the respective results of applying each to *any* value of their common domain are equal: f, g :: a -> b and f = g ==> forall (x :: a) . f x = g x Since Haskell contains the undefined value in every type, this applies as well to undefined: f x and g x must either both be undefined or equal. We can keep going from left to right, so that for any validly typed y, f x y = g x y, f x y z = g x y z, etc. The converse of this is also true, and called the principle of extensionality: Two functions can be considered equal if they have a common domain (type) and if, for each value in that domain (type), which in Haskell includes undefined, they give the same result. So if we have two functions f and g, and we know [2] that for *every* z (i.e. z is a free variable or a universally quantified variable) that f x y z = g x y z ==> f x y = g x y We can keep going from right to left: if in addition, this is true for all y, then f x = g x. And finally, if this is true for all x, then f = g. Note that Leibnitz allows for "any" argument, extensionality requires equality for "every" argument. Dan Weston [1] http://en.wikipedia.org/wiki/Identity_of_indiscernibles#Identity_and_indisce... [2] We know this because e.g. there is some definition or theorem saying so. We cannot compute this (even for finite domains) by trying each value. They need to give the same result even for undefined arguments, so that you cannot give a computable extensional definition of function equality even for finite domains, since if one function doesn't halt when applied to 3, the other must also not halt, and you can't wait for ever to be sure this is true. PR Stanley wrote:
Hi What on earth is unapplying function definitions? The following is taken from chapter 13 of the Hutton book: "...when reasoning about programs, function definitions can be both applied from left to right and unapplied from right to left."
Cheers Paul
participants (4)
-
Brent Yorgey -
Dan Weston -
PR Stanley -
Thomas Davie