CSE271: Principles of Programming Languages

Parameter Passing

Jooyong Yi (UNIST)

Without Store

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁) = (proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂))                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁) = 𝑣𝑎𝑙
----------------------------------------------------------------
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑣𝑎𝑙]ρ₂)

Without Store

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁) = (proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂))                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁) = 𝑣𝑎𝑙
----------------------------------------------------------------
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑣𝑎𝑙]ρ₂)

(define value-of                                                                          
  (lambda (exp env)
    (cases expression exp      
      ...
      (call-exp (rator rand)
        (let ((proc (expval->proc (value-of rator env)))
              (arg (value-of rand env)))
          (apply-procedure proc arg))))))

(define apply-procedure                                                                      
  (lambda (proc1 val)
    (cases proc proc1
      (procedure (var body saved-env)
        (value-of body (extend-env var val saved-env))))))

Explicit Reference

  (* Explicit Reference *)
  let counter = newref(0)
  in let f = proc (x) setref(counter, deref(counter) + 1)
     in let a = (f (f 1))
        in deref(counter)

Explicit Reference

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
------------------------------------------------------------------------
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑣𝑎𝑙]ρ₂ σ₃)

Explicit Reference

(define value-of-program                                                                                            
  (lambda (pgm)
    (initialize-store!)               ; new for explicit reference
    (cases program pgm
      (a-program (exp1)
        (value-of exp1 (init-env))))))

(define initialize-store!
    (lambda ()
      (set! the-store (empty-store))))

(define value-of                                                                                                
  (lambda (exp env)
    (cases expression exp      
      ...
      (call-exp (rator rand)
        (let ((proc (expval->proc (value-of rator env)))
              (arg (value-of rand env)))
          (apply-procedure proc arg))))))

(define apply-procedure                                                                      
  (lambda (proc1 val)
    (cases proc proc1
      (procedure (var body saved-env)
        (value-of body (extend-env var val saved-env))))))

Implicit Reference

  (* Implicit Reference *)
  let counter = 0
  in let f = proc (x) set counter = counter + 1
     in let a = (f (f 1))
        in counter

Implicit Reference

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
----------------------------------------------------------------------------
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

• 𝑙 ∉ dom(σ₃)

Implicit Reference

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
---------------------------------------------------------------------------- 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

(define value-of                                                                                                
  (lambda (exp env)
    (cases expression exp      
      ...
      (call-exp (rator rand)
        (let ((proc (expval->proc (value-of rator env)))
              (arg (value-of rand env)))
          (apply-procedure proc arg))))))

(define apply-procedure                                                                      
  (lambda (proc1 val)
    (cases proc proc1
      (procedure (var body saved-env)
        (value-of body (extend-env var (newref val) saved-env))))))

(define newref
  (lambda (val)
    (let ((next-ref (length the-store)))
       (set! the-store (append the-store (list val)))
     next-ref)))

Question

• Which value will be returned?

let p = proc (x) set x = 4
in let a = 3
   in begin (p a); a end

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
---------------------------------------------------------------------------- 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

Question

• Which value will be returned?

let p = proc (x) set x = 4
in let a = 3
   in begin (p a); a end

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
---------------------------------------------------------------------------- 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

• What do we pass to a callee, p?

Stack Frame

          |            |  ↑ higher address
          |            |
          |------------| ← %rbp (base pointer or frame pointer)
          |    arg0    | ← -8(%rbp)
          |    arg1    | ← -16(%rbp)
          |     ...    |
          |   local0   |
          |   local1   |
          |            |
          |            |
          |------------| ← %rsp (stack pointer)
          |            |
          |            | ↓ lower address 

Question

• Which value will be returned?

let p = proc (x) set x = 4
in let a = 3
   in begin (p a); a end

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
---------------------------------------------------------------------------- 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

• What do we pass to a callee, p?

Call-by-Value

• Implicit Reference

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
---------------------------------------------------------------------------- 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

Question

• What if we want to return 4?

let p = proc (x) set x = 4
in let a = 3
   in begin (p a); a end

Call-by-Reference

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                   
  (value-of 𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
------------------------------------------------------------------------------------ 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

↓

Call-by-Reference

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                   
  (value-of 𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
------------------------------------------------------------------------------------ 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

↓

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                         
----------------------------------------------------------------------------------------
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=ρ₁(𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟)]ρ₂ σ₂)

Example

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                         
----------------------------------------------------------------------------------------
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=ρ₁(𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟)]ρ₂ σ₂)

let p = proc (x) set x = 4
in let a = 3
   in begin (p a); a end

Example

let p = proc (x) set x = 4
in let a = 3
   in begin (p (+ a 1)); a end

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                         
----------------------------------------------------------------------------------------
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=ρ₁(𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟)]ρ₂ σ₂)

Call-by-Reference (𝑟𝑎𝑛𝑑 ≠ var-exp)

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                         
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
--------------------------------------------------------------------------------- 𝑟𝑎𝑛𝑑 ≠ var-exp ∧ 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

Spec of Call-by-Reference

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                         
----------------------------------------------------------------------------------------
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=ρ₁(𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟)]ρ₂ σ₂)

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                         
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
--------------------------------------------------------------------------------- 𝑟𝑎𝑛𝑑 ≠ var-exp ∧ 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

Impl of Call-by-Reference

(define value-of                                                                                                
  (lambda (exp env)
    (cases expression exp      
      ...
      (call-exp (rator rand)
        (let ((proc (expval->proc (value-of rator env)))
              (arg (value-of-operand rand env)))  ; value-of -> value-of-operand
          (apply-procedure proc arg))))))

(define value-of-operand
  (lambda (exp env)
    (cases expression exp
      (var-exp (var) (apply-env env var))
      (else (newref (value-of exp env))))))
        
(define apply-procedure                                                                      
  (lambda (proc1 val)
    (cases proc proc1
      (procedure (var body saved-env)
        (value-of body (extend-env var val saved-env))))))

Lambda Calculus Example

• Church numerals

0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f (f x)
3 = λf. λx. f (f (f x))
...

Lambda Calculus Example

0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f (f x)
3 = λf. λx. f (f (f x))
...

((λn. λf. λx. f (n f x)) (λf. λx. x))

Lambda Calculus Example

((λn. λf. λx. f (n f x)) (λf. λx. x))
=
(λn. λf. λx. f (n f x))[n ↦ (λf. λx. x)]

• Replace n with (λf. λx. x)
• This is called β-reduction in lambda calculus

Lambda Calculus Example

(λn. λf. λx. f (n f x))[n ↦ (λf. λx. x)]
=
λf. λx. f ((λf. λx. x) f x)

Lambda Calculus Example

λf. λx. f ((λf. λx. x) f x)
=
λf. λx. f ((λf. λx. x)[f ↦ f] x)

Lambda Calculus Example

λf. λx. f ((λf. λx. x)[f ↦ f] x)
=
λf. λx. f ((λx. x) x)

Lambda Calculus Example

λf. λx. f ((λx. x) x)
=
λf. λx. f (λx. x)[x ↦ x]

Lambda Calculus Example

λf. λx. f (λx. x)[x ↦ x]
=
λf. λx. f x

Lambda Calculus Example

  ((λn. λf. λx. f (n f x)) (λf. λx. x))
= λf. λx. f ((λf. λx. x) f x)
= λf. λx. f x

            ----------------------------
λf. λx. x → |  λn. λf. λx. f (n f x)    | → λf. λx. f x
            ----------------------------

Lambda Calculus Example

  ((λn. λf. λx. f (n f x)) (λf. λx. x))
= λf. λx. f ((λf. λx. x) f x)
= λf. λx. f x

            ----------------------------
λf. λx. x → |  λn. λf. λx. f (n f x)    | → λf. λx. f x
            ----------------------------
                Successor function

0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f (f x)
3 = λf. λx. f (f (f x))
...

Call-by-Name

((λn. λf. λx. f (n f x)) (λf. λx. x))
=
(λn. λf. λx. f (n f x))[n ↦ (λf. λx. x)]

• Replace n with (λf. λx. x)
• This is called β-reduction in lambda calculus
• (λf. λx. x) is passed to the callee as is
  • (λf. λx. x) is not evaluated before passing

Question

• What value will be returned?

letrec f = proc (x) (f (+ x 1))
in let g = proc (y) 10
   in (g (f 0))

Lazy Evaluation

• Evaluate the expression only when it is needed

letrec f = proc (x) (f (+ x 1))
in let g = proc (y) 10
   in (g (f 0))

Thunk

(define-datatype thunk thunk?
  (a-thunk
    (exp expression?)
    (env environment?)))

Call-by-Name (𝑟𝑎𝑛𝑑 ≠ var-exp)

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                         
---------------------------------------------------------------------------------------------- 𝑟𝑎𝑛𝑑 ≠ var-exp ∧ 𝑙 ∉ dom(σ₂)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=(a-thunk 𝑟𝑎𝑛𝑑 ρ₁)]σ₂)

Spec of Call-by-Name

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                         
---------------------------------------------------------------------------------------------- 𝑟𝑎𝑛𝑑 ≠ var-exp ∧ 𝑙 ∉ dom(σ₂)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=(a-thunk 𝑟𝑎𝑛𝑑 ρ₁)]σ₂)

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                         
----------------------------------------------------------------------------------------
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑐𝑎𝑙𝑙𝑒𝑒-𝑣𝑎𝑟=ρ₁(𝑐𝑎𝑙𝑙𝑒𝑟-𝑣𝑎𝑟)]ρ₂ σ₂)

Impl of Call-by-Name

(define value-of                                                                                                
  (lambda (exp env)
    (cases expression exp      
      ...
      (call-exp (rator rand)
        (let ((proc (expval->proc (value-of rator env)))
              (arg (value-of-operand rand env)))
          (apply-procedure proc arg)))
      ...)))

(define value-of-operand
  (lambda (exp env)
    (cases expression exp
      (var-exp (var) (apply-env env var))
      (else (newref (a-thunk exp env)))))) ; value-of -> a-thunk
        
(define apply-procedure                                                                      
  (lambda (proc1 val)
    (cases proc proc1
      (procedure (var body saved-env)
        (value-of body (extend-env var val saved-env))))))

Impl of Call-by-Name

(define value-of                                                                                                
  (lambda (exp env)
    (cases expression exp      
     ...
     (var-exp (var)
        (let ((ref1 apply-env env var)))
          (let (w (deref ref1)))
            (if (expval? w)
                w
                (value-of-thunk w)))
     ...)))

(define value-of-thunk
  (lambda (th)
    (cases thunk th
      (a-thunk (exp1 saved-env)
        (value-of exp1 saved-env)))))

Example

let f = proc (x) (+ x x)
in (f (+ 1 2))

Call-by-Need

(define value-of                                                                                                
  (lambda (exp env)
    (cases expression exp      
     ...
     (var-exp (var)
        (let ((ref1 apply-env env var)))
          (let (w (deref ref1)))
            (if (expval? w)
                w
                (let ((val1 (value-of-thunk w)))
                  (begin
                    (set! ref1 val1)
                    val1))))
     ...)))

Question

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
---------------------------------------------------------------------------- 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

• What happens to 𝑙 ∈ σ₃ once the procedure returns?