#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
Owner: | set to goldfiere |
---|
comment:2 Changed 3 years ago by
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
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
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
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:7 Changed 3 years ago by
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:9 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
This seems all set now. Reopen if you think otherwise.
comment:10 Changed 2 years ago by
Milestone: | → 8.0.1 |
---|
(Making Richard aware of this ticket.)