X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=fbad0ea11f481bdf1b0c061ea92c0f0b2fea7895;hp=e2f3a968dec9a656c8970f2439375e6ec7868302;hb=bff5a598be513f497ad61d29b7c7584f94d2b993;hpb=feee31da167a3c0505d2683d3e81e2597743f1a6 diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex index e2f3a96..fbad0ea 100644 --- a/Chapters/Normalization.tex +++ b/Chapters/Normalization.tex @@ -1788,17 +1788,17 @@ expression shows an example: \startlambda - app2 :: (Word -> Word) -> Word -> Word - app2 = λf.λa.f (f a) + twice :: (Word -> Word) -> Word -> Word + twice = λf.λa.f (f a) main = λa.app (λx. x + x) a \stoplambda - This example shows a function \lam{app2} that takes a function as a + This example shows a function \lam{twice} that takes a function as a first argument and applies that function twice to the second argument. Again, we've made the function monomorphic for clarity, even though this function would be a lot more useful if it was polymorphic. The - function \lam{main} uses \lam{app2} to apply a lambda epression twice. + function \lam{main} uses \lam{twice} to apply a lambda epression twice. When faced with a user defined function, a body is available for that function. This means we could create a specialized version of the @@ -1808,23 +1808,23 @@ Applying this transformation to the example gives: \startlambda - app2' :: Word -> Word - app2' = λb.(λf.λa.f (f a)) (λx. x + x) b + twice' :: Word -> Word + twice' = λb.(λf.λa.f (f a)) (λx. x + x) b main = λa.app' a \stoplambda The \lam{main} function is now in normal form, since the only higher order value there is the top level lambda expression. The new - \lam{app2'} function is a bit complex, but the entire original body of - the original \lam{app2} function is wrapped in a lambda abstraction + \lam{twice'} function is a bit complex, but the entire original body of + the original \lam{twice} function is wrapped in a lambda abstraction and applied to the argument we've specialized for (\lam{λx. x + x}) and the other arguments. This complex expression can fortunately be effectively reduced by repeatedly applying β-reduction: \startlambda - app2' :: Word -> Word - app2' = λb.(b + b) + (b + b) + twice' :: Word -> Word + twice' = λb.(b + b) + (b + b) \stoplambda This example also shows that the resulting normal form might not be as