Opened 3 years ago

Closed 3 years ago

Last modified 23 months ago

#10121 closed bug (fixed)

operational semantics is incomplete?

Reported by: javran Owned by: goldfire
Priority: normal Milestone: 8.0.1
Component: Documentation Version: 7.8.4
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I was trying to read docs/core-spec/core-spec.pdf to understand the operational semantics for core language. So I started off by playing with operational semantics rules manually.

But I found the following expression gets stuck:

v1 = let fix = \f -> let x = f x in x
         pf = \f x -> if x == 0
                          then x
                          else f (pred x)
     in (fix pf) 2
-- S_LETNONREC
v2 = ((\f -> let x = f x in x)
      (\f x -> if x == 0
                   then x
                   else f (pred x)))
     2
-- S_APP
v3 = (let x = (\f x -> if x == 0
                           then x
                           else f (pred x)) x
      in x) 2
-- S_APP; S_LETREC
v4 = (let x = (\f x -> if x == 0
                           then x
                           else f (pred x)) x
      in (\f x -> if x == 0
                      then x
                      else f (pred x)) x) 2
-- S_APP
v5 = (let x = (\f x -> if x == 0
                           then x
                           else f (pred x)) x
      in (\x1 -> if x1 == 0
                     then x1
                     else x (pred x1))) 2

at this point x is not a free variable so S_LETRECRETURN cannot be applied.

Did I make it wrong or some rules are missing for the operational semantics?

Change History (10)

comment:1 Changed 3 years ago by nomeata

Owner: set to goldfiere

(Making Richard aware of this ticket.)

comment:2 Changed 3 years ago by goldfire

Owner: changed from goldfiere to goldfire

Good point. The operational semantics are just wrong around letrec. Will think about this a little later, but a suggestion for a fix is welcome.

comment:3 Changed 3 years ago by goldfire

Emails back and forth with the poster indicate that this is harder than I thought. That person is working on it, and I will wait to hear back. Once we have a way forward, I'm happy to update the spec accordingly.

comment:4 Changed 3 years ago by darchon

Sorry for the shameless self-plug... but perhaps check out Appendix C of: http://doc.utwente.nl/93962/1/thesis_C_Baaij.pdf

It's System FC + Letrec + Case... very much like Core.

comment:5 Changed 3 years ago by goldfire

Cool beans. Thanks for posting that. After a quick look-through, the rules around letrec there look quite promising. At least Christiaan has a proof that they work, unlike the system in core-spec. @javran, thoughts? If these look good to you, I'll rewrite core-spec accordingly.

comment:6 Changed 3 years ago by javran

Thanks @darchon @goldfire that looks good to me :)

comment:7 Changed 3 years ago by darchon

Yeah... those rules are the only ones I could think of and stay within the domain of the original small-step semantics of System FC. Another way to go about it is to add an explicit heap to the semantics, and put let-bindings to that heap, ala "a natural semantics for lazy evaluation". But then you'd have to update all the other rules also.

comment:8 Changed 3 years ago by Richard Eisenberg <eir@…>

In 414e20bc7f5166d020ace3d92cd605e121d5eb3c/ghc:

Fix the formal operational semantics (#10121)

This adapts the work of Christiaan Baaij to present a sensible
operational semantics for FC with mutual recursion.

comment:9 Changed 3 years ago by goldfire

Resolution: fixed
Status: newclosed

This seems all set now. Reopen if you think otherwise.

comment:10 Changed 23 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.