[GHC] #10121: operational semantics is incomplete?
#10121: operational semantics is incomplete? -------------------------------------+------------------------------------- Reporter: javran | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: | Version: 7.8.4 Documentation | Operating System: Unknown/Multiple Keywords: | Type of failure: None/Unknown Architecture: | Blocked By: Unknown/Multiple | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- 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: {{{#!hs 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10121 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10121: operational semantics is incomplete? -------------------------------------+------------------------------------- Reporter: javran | Owner: goldfiere Type: bug | Status: new Priority: normal | Milestone: Component: Documentation | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by nomeata): * owner: => goldfiere Comment: (Making Richard aware of this ticket.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10121#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10121: operational semantics is incomplete? -------------------------------------+------------------------------------- Reporter: javran | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Documentation | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * owner: goldfiere => goldfire Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10121#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10121: operational semantics is incomplete? -------------------------------------+------------------------------------- Reporter: javran | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Documentation | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10121#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10121: operational semantics is incomplete? -------------------------------------+------------------------------------- Reporter: javran | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Documentation | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10121#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10121: operational semantics is incomplete? -------------------------------------+------------------------------------- Reporter: javran | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Documentation | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10121#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10121: operational semantics is incomplete? -------------------------------------+------------------------------------- Reporter: javran | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Documentation | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by javran): Thanks @darchon @goldfire that looks good to me :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10121#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10121: operational semantics is incomplete? -------------------------------------+------------------------------------- Reporter: javran | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Documentation | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10121#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10121: operational semantics is incomplete?
-------------------------------------+-------------------------------------
Reporter: javran | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone:
Component: Documentation | Version: 7.8.4
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: None/Unknown | Unknown/Multiple
Blocked By: | Test Case:
Related Tickets: | Blocking:
| Differential Revisions:
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#10121: operational semantics is incomplete? -------------------------------------+------------------------------------- Reporter: javran | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Documentation | Version: 7.8.4 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => fixed Comment: This seems all set now. Reopen if you think otherwise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10121#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC