CSE271: Principles of Programming Languages

State

Jooyong Yi (UNIST)

Question

• What value will be returned?

let counter = 0
in let f = proc (x) (let counter = counter + 1 in x)
   in let a = (f (f 1))
      in counter

Question

• What if we want to count the number of times f is called?

let counter = 0
in let f = proc (x) (let counter = counter + 1 in x)
   in let a = (f (f 1))
      in counter

Answer

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

Answer

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

|  Var    | Val |   | Loc | Val |
|---------|-----|   |-----|-----|
| counter | l   |   |  l  |  0  |

Answer

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

|  Var    | Val |   | Loc | Val |
|---------|-----|   |-----|-----|
| counter | l   |   |  l  |  2  |

Store (Memory)

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

Environment: Var → Val         Store: Loc → Val               

|  Var    | Val |              | Loc | Val |
|---------|-----|              |-----|-----|
| counter | l   |              |  l  |  2  |

State

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

Environment: Var → Val         Store: Loc → Val               

|  Var    | Val |              | Loc | Val |      | Loc | Val |      | Loc | Val |
|---------|-----|              |-----|-----|  →   |-----|-----|  →   |-----|-----|
| counter | l   |              |  l  |  0  |      |  l  |  1  |      |  l  |  2  |
                                 
                                     σ₀                σ₁                  σ₂

Storeless Specification

(value-of 𝑒𝑥𝑝 ρ) = 𝑣𝑎𝑙

• Example

Store-Passing Specification

(value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑣𝑎𝑙, σ₁)

Store-Passing Specification

(value-of (const-exp 𝑛) ρ σ₀) = (𝑛, σ₀)

Store-Passing Specification

     (value-of 𝑒𝑥𝑝₁ ρ σ₀) = (𝑣𝑎𝑙₁, σ₁)
     (value-of 𝑒𝑥𝑝₂ ρ σ₁) = (𝑣𝑎𝑙₂, σ₂) 
-----------------------------------------------------------
  (value-of (diff-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) ρ σ₀) = (𝑣𝑎𝑙₁ - 𝑣𝑎𝑙₂, σ₂)

Store-Passing Specification

     (value-of 𝑒𝑥𝑝₁ ρ σ₀) = (𝑣𝑎𝑙₁, σ₁)
-----------------------------------------------------------
  (value-of (if-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂ 𝑒𝑥𝑝₃) ρ σ₀) 
  = 
  (value-of 𝑒𝑥𝑝₂ ρ σ₁) if (expval->bool 𝑣𝑎𝑙₁) = #t
  or
  (value-of 𝑒𝑥𝑝₃ ρ σ₁) if (expval->bool 𝑣𝑎𝑙₁) = #f

Store-Manipulating Operations

[Concrete Syntax]
Expression ::= ...
            | newRef (Expression)
            | deref (Expression)
            | setRef (Expression, Expression)

[Abstract Syntax]
Expression ::= ...
            |  newref-exp (exp)
            |  deref-exp (exp)
            |  setref-exp (exp1 exp2)

Spec of newref

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑣𝑎𝑙, σ₁)      𝑙 ∉ dom(σ₁)
-----------------------------------------------------------
(value-of (newref-exp 𝑒𝑥𝑝) ρ σ₀) = (𝑙, [𝑙=𝑣𝑎𝑙]σ₁)

Spec of deref

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑙, σ₁)
-----------------------------------------------------------
(value-of (deref-exp 𝑒𝑥𝑝) ρ σ₀) = (__, __)

Spec of deref

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑙, σ₁)
-----------------------------------------------------------
(value-of (deref-exp 𝑒𝑥𝑝) ρ σ₀) = (σ₁(𝑙), σ₁)

Spec of setref

      (value-of 𝑒𝑥𝑝₁ ρ σ₀) = (𝑙, σ₁)
      (value-of 𝑒𝑥𝑝₂ ρ σ₁) = (𝑣𝑎𝑙, σ₂)
-----------------------------------------------------------
(value-of (setref-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) ρ σ₀) = (𝑣𝑎𝑙, __)

Spec of setref

      (value-of 𝑒𝑥𝑝₁ ρ σ₀) = (𝑙, σ₁)
      (value-of 𝑒𝑥𝑝₂ ρ σ₁) = (𝑣𝑎𝑙, σ₂)
-----------------------------------------------------------
(value-of (setref-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) ρ σ₀) = (𝑣𝑎𝑙, [𝑙=𝑣𝑎𝑙]σ₂)

Impl of newref

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑣𝑎𝑙, σ₁)      𝑙 ∉ dom(σ₁)
-----------------------------------------------------------
(value-of (newref-exp 𝑒𝑥𝑝) ρ σ₀) = (𝑙, [𝑙=𝑣𝑎𝑙]σ₁)

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

Impl of deref

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑙, σ₁)
-----------------------------------------------------------
(value-of (deref-exp 𝑒𝑥𝑝) ρ σ₀) = (σ₁(𝑙), σ₁)

(define deref
  (lambda (ref)
    (list-ref the-store ref)))

Impl of setref

      (value-of 𝑒𝑥𝑝₁ ρ σ₀) = (𝑙, σ₁)
      (value-of 𝑒𝑥𝑝₂ ρ σ₁) = (𝑣𝑎𝑙, σ₂)
-----------------------------------------------------------
(value-of (setref-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) ρ σ₀) = (𝑣𝑎𝑙, [𝑙=𝑣𝑎𝑙]σ₂)                                                          

  (define setref!                                                                                                
    (lambda (ref val)
      (set! the-store
        (letrec
          ((setref-inner
             ;; returns a list like store1, except that position ref1
             ;; contains val. 
             (lambda (store1 ref1)
               (cond
                 ((null? store1)
                  (report-invalid-reference ref the-store))
                 ((zero? ref1)
                  (cons val (cdr store1)))
                 (else
                   (cons
                     (car store1)
                     (setref-inner
                       (cdr store1) (- ref1 1))))))))
          (setref-inner the-store ref)))))

Different Syntax

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

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

Explicit vs Implicit 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)

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

Store-Manipulating Operation

[Concrete Syntax]
Expression ::= ...
            | set Identifier = Expression

[Abstract Syntax]
Expression ::= ...
            |  assign-exp (var exp)

Spec of assign-exp

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑣𝑎𝑙, σ₁)
-----------------------------------------------------------
(value-of (assign-exp 𝑣𝑎𝑟 𝑒𝑥𝑝) ρ σ₀) = (𝑣𝑎𝑙, [__=𝑣𝑎𝑙]σ₁)

      (value-of 𝑒𝑥𝑝₁ ρ σ₀) = (𝑙, σ₁)
      (value-of 𝑒𝑥𝑝₂ ρ σ₁) = (𝑣𝑎𝑙, σ₂)
-----------------------------------------------------------
(value-of (setref-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂) ρ σ₀) = (𝑣𝑎𝑙, [𝑙=𝑣𝑎𝑙]σ₂)

Spec of assign-exp

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑣𝑎𝑙, σ₁)
-----------------------------------------------------------
(value-of (assign-exp 𝑣𝑎𝑟 𝑒𝑥𝑝) ρ σ₀) = (𝑣𝑎𝑙, [ρ(𝑣𝑎𝑟)=𝑣𝑎𝑙]σ₁)

Spec of assign-exp

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑣𝑎𝑙, σ₁)
-----------------------------------------------------------
(value-of (assign-exp 𝑣𝑎𝑟 𝑒𝑥𝑝) ρ σ₀) = (𝑣𝑎𝑙, [ρ(𝑣𝑎𝑟)=𝑣𝑎𝑙]σ₁)

set counter = counter + 1

Environment: Var → Val         Store: Loc → Val               

|  Var    | Val |              | Loc | Val |
|---------|-----|              |-----|-----|
| counter | l   |              |  l  |  2  |

L-Value

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑣𝑎𝑙, σ₁)
-----------------------------------------------------------
(value-of (assign-exp 𝑣𝑎𝑟 𝑒𝑥𝑝) ρ σ₀) = (𝑣𝑎𝑙, [ρ(𝑣𝑎𝑟)=𝑣𝑎𝑙]σ₁)

set counter = counter + 1

Environment: Var → Val         Store: Loc → Val               

|  Var    | Val |              | Loc | Val |
|---------|-----|              |-----|-----|
| counter | l   |              |  l  |  2  |

R-Value

(value-of (var-exp 𝑣𝑎𝑟) ρ σ) = (σ(ρ(𝑣𝑎𝑟)), σ)

set counter = counter + 1

Environment: Var → Val         Store: Loc → Val               

|  Var    | Val |              | Loc | Val |
|---------|-----|              |-----|-----|
| counter | l   |              |  l  |  2  |

Explicit vs Implicit Reference

• What values can expressions have?

  (* 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)

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

Explicit vs Implicit Reference

• What values can expressions and variables have?

  (* 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)

• ExpVal = Int + Bool + Proc + Ref(ExpVal)
• DenVal = ExpVal

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

Explicit vs Implicit Reference

• What values can expressions and variables have?

  (* 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)

• ExpVal = Int + Bool + Proc + Ref(ExpVal)
• DenVal = ExpVal

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

• ExpVal = Int + Bool + Proc
• DenVal = Ref(ExpVal)

Spec of apply-procedure

• Without Store

(apply-procedure (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ) 𝑣𝑎𝑙) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑣𝑎𝑙]ρ)

Spec of apply-procedure

• Implicit Reference
  • ExpVal = Int + Bool + Proc
  • DenVal = Ref(ExpVal)

(apply-procedure (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ) 𝑣𝑎𝑙 σ) = (value-of 𝑏𝑜𝑑𝑦 __ __)

Spec of apply-procedure

• Implicit Reference
  • ExpVal = Int + Bool + Proc
  • DenVal = Ref(ExpVal)

(apply-procedure (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ) 𝑣𝑎𝑙 σ) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ [𝑙=𝑣𝑎𝑙]σ)

• 𝑙 ∉ dom(σ)

Spec of let

• Without Store

       (value-of 𝑒𝑥𝑝 ρ) = 𝑣𝑎𝑙                              
---------------------------------------------
(value-of (let-exp 𝑣𝑎𝑟 𝑒𝑥𝑝 𝑏𝑜𝑑𝑦) ρ)
= (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟 = 𝑣𝑎𝑙]ρ) 

Spec of let

• Implicit Reference

       (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑣𝑎𝑙, σ₁)
---------------------------------------------
(value-of (let-exp 𝑣𝑎𝑟 𝑒𝑥𝑝 𝑏𝑜𝑑𝑦) ρ σ₀)
= (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ [𝑙=𝑣𝑎𝑙]σ₁)

• 𝑙 ∉ dom(σ₁)

Impl of Implicit Reference

; Storeless and Explicit Reference
(define value-of
  (lambda (exp env)
    (cases expression exp
      ...
      (var-exp (var) (apply-env env var))
      ...)))

↓

; Implicit Reference
(define value-of
  (lambda (exp env)
    (cases expression exp
      ...
      (var-exp (var) ___________________)
      ...)))

Impl of Implicit Reference

; Storeless and Explicit Reference
(define value-of
  (lambda (exp env)
    (cases expression exp
      ...
      (var-exp (var) (apply-env env var))
      ...)))

↓

; Implicit Reference
(define value-of
  (lambda (exp env)
    (cases expression exp
      ...
      (var-exp (var) (deref (apply-env env var)))
      ...)))

Impl of Implicit Reference

      (value-of 𝑒𝑥𝑝₁ ρ σ₀) = (𝑣𝑎𝑙, σ₁)
-----------------------------------------------------------
(value-of (assign-exp 𝑣𝑎𝑟 𝑒𝑥𝑝₁) ρ σ₀) = (𝑣𝑎𝑙, [ρ(𝑣𝑎𝑟)=𝑣𝑎𝑙]σ₁)

(define value-of
  (lambda (exp env)
    (cases expression exp
      ...
      (assign-exp (var exp1)
        (let ((val (value-of exp1 env)))
          (setref!
            (apply-env env var)
            val)
          val))
      ...)))

Impl of Implicit Reference

(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 Implicit Reference

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

↓

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

Impl of Implicit Reference

(let-exp (var exp1 body)       
          (let ((val1 (value-of exp1 env)))
            (value-of body
              (extend-env var val1 env))))

↓

(let-exp (var exp1 body)       
          (let ((val1 (value-of exp1 env)))
            (value-of body
              (extend-env var (newref val1) env))))