0

I have question about weak head normal form and normal form.

Weak head normal form means, the expression will only evaluate as far as necessary to reach to a data constructor.

Normal form means, the expression will be fully evaluated.

Now, I have following expression:

\x -> x * 10

Why the expression above is in normal form?

"Papu" ++ "chon"

Why the expression above is in neither WHNF nor NF?

softshipper
  • 32,463
  • 51
  • 192
  • 400
  • 1
    You've answered your own questions: 1) because "the expression [is] fully evaluated". 2) because "the expression [is not] evaluate[d] as far as necessary to reach to a data constructor". Perhaps you should state what about these definitions is unclear to you. – user2407038 Jun 12 '17 at 11:16

2 Answers2

6

WHNF evaluates far enough to reach a data constructor or lambda function.

If you have a lambda function that hasn't been called with an argument, you cannot evaluate it any further anyway. So a lambda function is in WHNF, and indeed NF, since there is nothing to evaluate further. Now, if you call the lambda function with an argument, we can evaluate what the result might be. But the lambda function on its own? Nothing further to be done.

Your first expression is a lambda function with no arguments. It is therefor in normal form.

Your second expression is neither a data constructor nor a lambda, hence is not in any normal form. Now, if you evaluate it for one step, you obtain

'P' : ("apu" ++ "chon")

Which (although the syntax doesn't look like it) begins with a data constructor (namely (:)), and hence is in WHNF, but not NF (since it still contains the unevaluated (++) subexpression).

Perhaps it's easier if we get rid on the infix syntax:

(++) "Papu" "chon"

vs

(:) 'P' ( (++) "apu" "chon" )
MathematicalOrchid
  • 61,854
  • 19
  • 123
  • 220
  • 1
    Actually, normal form of a lambda term traditionally has meant evaluating as much as possible under the lambda. `\x -> (1 + 1) + x` is not in normal form, as it could be reduced to `\x -> 2 + x` – Carl Jun 12 '17 at 20:42
  • Isn't there a requirement for the data constructor in WHNF to be *lazy*? – Will Ness Jun 30 '17 at 01:43
3
\x -> x * 10

Why the expression above is in normal form?

Because, you can't simplify it.

"Papu" ++ "chon"

Why the expression above is in neither WHNF nor NF?

First of all, if some expression in NF - that means it's in WHNF. NF it's more restricted version of WHNF.

So, We can restructure your question. Why the expression above isn't in WHNF?

Simple answer is: We can simplify it to "Papuchon".

If you want to know what difference between WHNF and NF, you can read, for example, this.

freestyle
  • 3,692
  • 11
  • 21
  • About the lambda expression, what does it mean `simplify`? – softshipper Jun 12 '17 at 10:20
  • 1
    You can `simplify` some expression if it has subexpression which is `lambda application` and you can reduce it (apply it). Or more simpler, you can call function and get result. In your example, you can't calculate `x * 10`, because you don't known an `x` value. – freestyle Jun 12 '17 at 10:28
  • @zero_coding For instance, `\x -> 5+5` and `\x -> id x` can be simplifed / reduced, so they are not NF. `\x -> x (id 5)` can also be reduced, since `id 5` can. Instead, `\x -> x 5` can not be reduced, since we do not know what `x` is, so the lambda is in NF. `\x -> x+x` is also a NF. – chi Jun 12 '17 at 12:16
  • 1
    @chi and MathematicalOrchid: you have two different notions of NF (chi is happy to reduce under lambdas when MathematicalOrchid is not). This could be confusing for the reader. – gallais Jun 12 '17 at 15:27
  • @freestyle `\x -> 5+5` I can simplify/reduce to `\x -> 10` right? – softshipper Jun 12 '17 at 15:29
  • 1
    @zero_coding Yes, you can. More over, you must to do that for transform to NF. – freestyle Jun 12 '17 at 15:35
  • 2
    @zero_coding But in Haskell is convention that WHNF equivalent to NF for functions. (see `instance NFData (a -> b)`) – freestyle Jun 12 '17 at 15:40
  • @gallais Good point. I guess it depends on the context. In some theories, reductions under lambdas are allowed. In most implementations of functional languages, however, we don't reduce under lambdas. – chi Jun 12 '17 at 18:48
  • can `'P' : "apuchon"` be simplified? isn't it in WHNF though? – Will Ness Jun 30 '17 at 00:21
  • @WillNess `"apuchon"` its just syntactic sugar, so `'P' : "apuchon"` ~ `'P':'a':'p':'u':'c':'h':'o':'n':[]`. – freestyle Jun 30 '17 at 07:55
  • that's an irrelevant (here) detail. so, can `'P' : ("apu" ++ "chon")` be simplified? is it in WHNF? – Will Ness Jun 30 '17 at 10:31
  • @WillNess It can be simplified (it isn't in NF) and it's in WHNF (top redex is construct application and it cant be reduced to something). – freestyle Jun 30 '17 at 11:07