search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Is 'fix v' a value? #161

Closed seohongpark closed 9 years ago

seohongpark commented 9 years ago

In MoreStlc chapter, there isn't any mention of 'fix v can be a value', but in Assignment12_00.v, it says fix v can be a value when v is a value.

Can anybody explain which choice is right and why?

jaewooklee93 commented 9 years ago

I think, yes, every fixpoint function is a value, too. (like ordinary functions)

At least, we cannot evaluate without giving an argument to function. So fix v is value, given v is value.

However, I think our definition, professor gave, is somewhat weak. Because value (tfix (tnat 0)) seems ill-typed, but we can prove it since (tnat 0) is value.

The reason there is no mention about fix may be because everything about fix is actually exercise.

seohongpark commented 9 years ago

Thanks! Additionally, I concluded that fix v can be a value because we adopt ST_AppFix rule in Assignment12_00.v. Contrastively, if we adopt ST_FixAbs rule (MoreStlc version), I think we can make well-typed fix v always take a step. Also, It seems that the problem you mentioned can be resolved if we adopt the rule of MoreStlc version.

jaewooklee93 commented 9 years ago

Oh, I see. I agree with your opinion.