operational semantics is incomplete?
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?
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.4 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Documentation |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |