You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When a lambda's body was just a free variable, we were creating a new
global that pointed at the real global. For example, suppose "false"
is at address #1, and we're reducing the input at address #3:
#1: Global "false" #2#2: Closure (λt. λf. f)
#3: Apply #4#5 <---------[input]--------> (λa. false) (λb. b)
#4: Closure (λa. false)
#5: Closure (λb. b)
We would reduce the input as follows:
1. (λa. false) (λb. b)
2. false
3. false
4. λt. λf. f
This is because we were instantating the body of the lambda by creating
a new Global:
#1: Global "false" #2#2: Closure (λt. λf. f)
#3: Global "false" #1
Instead of a new pointer:
#1: Global "false" #2#2: Closure (λt. λf. f)
#3: Pointer #1
And then we would have to unwind and fetch the global twice. The fix is
to use a Pointer instead (which we correctly keep unwinding through).
α-captures are correctly handled in terms of semantics, but the displayed expression doesn't display the α-conversion.
At step 2 we should have something like (λn. (λx. x y) n z) z so that the conversion is made explicit.
A minor problem, but wanted to make note of it in case there are people confused. It should be trivial to fix.
The text was updated successfully, but these errors were encountered: