CSE271: Principles of Programming Languages

Recursive Procedures

Jooyong Yi (UNIST)

Recursion

(value-of
  << let double = proc (x) if zero?(x) then 0 else -((double -(x,1)), -2)
     in (double 6) >>
  ρ₀)  

ρ₀ = []

Recursion

(value-of
  << let double = proc (x) if zero?(x) then 0 else -((double -(x,1)), -2)
     in (double 6) >>
  ρ₀)
=  
(value-of
  << (double 6) >>
  ρ₁)  

ρ₀ = []
ρ₁ = [double=(proc-val (procedure x <<if zero?(x) then 0 else -((double -(x,1)), -2)>> ρ₀))]ρ₀

(value-of (proc-exp 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦) ρ)  = (proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ))

Recursion

(value-of
  << (double 6) >>
  ρ₁)
=  
(value-of
  (call-exp double 6)
  ρ₁)  

ρ₀ = []
ρ₁ = [double=(proc-val (procedure x <<if zero?(x) then 0 else -((double -(x,1)), -2)>> ρ₀))]ρ₀

Recursion

(value-of
  (call-exp double 6)
  ρ₁)  
=
(value-of
  << if zero?(x) then 0 else -((double -(x,1)), -2) >>
  [x=6]ρ₀)  

ρ₀ = []
ρ₁ = [double=(proc-val (procedure x <<if zero?(x) then 0 else -((double -(x,1)), -2)>> ρ₀))]ρ₀

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

Recursion

(value-of
  << if zero?(x) then 0 else -((double -(x,1)), -2) >>
  [x=6]ρ₀)  
=
(value-of
  <<-((double -(x,1)), -2)>>  
  [x=6]ρ₀)

ρ₀ = []
ρ₁ = [double=(proc-val (procedure x <<if zero?(x) then 0 else -((double -(x,1)), -2)>> ρ₀))]ρ₀

Root Cause of the Problem?

(value-of
  << let double = proc (x) if zero?(x) then 0 else -((double -(x,1)), -2)                           
     in (double 6) >>
  ρ₀)
=  
(value-of
  << (double 6) >>
  ρ₁)
=  
(value-of
  (call-exp double 6)
  ρ₁)  
=
(value-of
  << if zero?(x) then 0 else -((double -(x,1)), -2) >>
  [x=6]ρ₀)  
=
(value-of
  <<-((double -(x,1)), -2)>>  
  [x=6]ρ₀)

ρ₀ = []
ρ₁ = [double=(proc-val (procedure x <<if zero?(x) then 0 else -((double -(x,1)), -2)>> ρ₀))]ρ₀

What We Want

(value-of
  << let double = proc (x) if zero?(x) then 0 else -((double -(x,1)), -2)                           
     in (double 6) >>
  ρ₀)
=  
(value-of
  << (double 6) >>
  ρ₁)
=  
(value-of
  (call-exp double 6)
  ρ₁)  
=
(value-of
  << if zero?(x) then 0 else -((double -(x,1)), -2) >>
  [x=6]ρ₁)  
=
(value-of
  <<-((double -(x,1)), -2)>>  
  [x=6]ρ₁)

ρ₀ = []
ρ₁ = [double=(proc-val (procedure x <<if zero?(x) then 0 else -((double -(x,1)), -2)>> ρ₁))]ρ₀

Any Problem?

(value-of
  << let double = proc (x) if zero?(x) then 0 else -((double -(x,1)), -2)                           
     in (double 6) >>
  ρ₀)
=  
(value-of
  << (double 6) >>
  ρ₁)
=  
(value-of
  (call-exp double 6)
  ρ₁)  
=
(value-of
  << if zero?(x) then 0 else -((double -(x,1)), -2) >>
  [x=6]ρ₁)  
=
(value-of
  <<-((double -(x,1)), -2)>>  
  [x=6]ρ₁)

ρ₀ = []
ρ₁ = [double=(proc-val (procedure x <<if zero?(x) then 0 else -((double -(x,1)), -2)>> ρ₁))]ρ₀

Hint for Fix

• When do we need the value of double?

(value-of
  << let double = proc (x) if zero?(x) then 0 else -((double -(x,1)), -2)                           
     in (double 6) >> ρ₀)
=  
(value-of
  << (double 6) >> ρ₁)
=  
(value-of
  (call-exp double 6) ρ₁)  
=
(value-of
  << if zero?(x) then 0 else -((double -(x,1)), -2) >> [x=6]ρ₁)  
=
(value-of
  <<-((double -(x,1)), -2)>> [x=6]ρ₁)

ρ₀ = []
ρ₁ = [double=(proc-val (procedure x <<if zero?(x) then 0 else -((double -(x,1)), -2)>> ρ₁))]ρ₀

Let's Fix

(value-of
  << letrec double = proc (x) if zero?(x) then 0 else -((double -(x,1)), -2)                           
     in (double 6) >> ρ₀)
=  
(value-of
  << (double 6) >> ρ₁)
=  
(value-of
  (call-exp double 6) ρ₁)  
=
(value-of
  << if zero?(x) then 0 else -((double -(x,1)), -2) >> [x=6]ρ₁)  

ρ₀ = []
ρ₁ = (extend-env-rec double x <<if zero?(x) ... >> ρ₀)

(apply-env ρ₁ double) = (proc-val (procedure x <<if zero?(x) ... >> ρ₁))

Let's Fix

(value-of
  << let y = 1
     in letrec double = proc (x) if zero?(x) then 0 else -((double -(x,y)), -2)                           
        in (double 6) >> ρ₀)
= ... = 
(value-of
  << (double 6) >> ρ₂)
=  
(value-of
  (call-exp double 6) ρ₂)  
=
(value-of
  << if zero?(x) then 0 else -((double -(x,y)), -2) >> [x=6]ρ₂)  

ρ₁ = (extend-env y 1 ρ₀)
ρ₂ = (extend-env-rec double x <<if zero?(x) ... >> ρ₁)

(apply-env ρ₂ double) = (proc-val (procedure x <<if zero?(x) ... >> ρ₂))
(apply-env ρ₂ y) = ?

Let's Fix

(value-of
  << let y = 1
     in letrec double = proc (x) if zero?(x) then 0 else -((double -(x,y)), -2)                           
        in (double 6) >> ρ₀)
= ... = 
(value-of
  << (double 6) >> ρ₂)
=  
(value-of
  (call-exp double 6) ρ₂)  
=
(value-of
  << if zero?(x) then 0 else -((double -(x,y)), -2) >> [x=6]ρ₂)  

ρ₁ = (extend-env y 1 ρ₀)
ρ₂ = (extend-env-rec double x <<if zero?(x) ... >> ρ₁)

(apply-env ρ₂ double) = (proc-val (procedure x <<if zero?(x) ... >> ρ₂))
(apply-env ρ₂ y) = (apply-env ρ₁ y) = 1

Spec of letrec expression

(value-of
  (letrec-exp proc-name bound-var proc-body letrec-body) 
  ρ)
=
(value-of
  letrec-body
  (extend-env-rec proc-name bound-var proc-body ρ))

Spec of apply-env

  ρ₁ = (extend-env-rec proc-name bound-var proc-body ρ₀)
----------------------------------------------------------------------------------- search-proc-name = proc-name
  (apply-env ρ₁ search-proc-name) = (proc-val (procedure bound-var proc-body ρ₁))

Spec of apply-env

  ρ₁ = (extend-env-rec proc-name bound-var proc-body ρ₀)
----------------------------------------------------------------------------------- search-proc-name = proc-name
  (apply-env ρ₁ search-proc-name) = (proc-val (procedure bound-var proc-body ρ₁))


  ρ₁ = (extend-env-rec proc-name bound-var proc-body ρ₀)
--------------------------------------------------------------------- search-proc-name ≠ proc-name
  (apply-env ρ₁ search-proc-name) = (apply-env ρ₀ search-proc-name)

Spec and Impl of apply-env

  ρ₁ = (extend-env var val ρ₀)
---------------------------------------------------------------- search-var = var
  (apply-env ρ₁ search-var) = val


  ρ₁ = (extend-env var val ρ₀)
---------------------------------------------------------------- search-var ≠ var
  (apply-env ρ₁ search-var) = (apply-env ρ₀ search-var)  

(define apply-env
  (lambda (env search-var)
     (cases environment env        
        ...
        (extend-env (var val saved-env)
          (if (eqv? search-var var)
              val
              (apply-env saved-env search-var)))
        ...)))

Spec and Impl of apply-env

  ρ₁ = (extend-env-rec proc-name bound-var proc-body ρ₀)
----------------------------------------------------------------------------------- search-proc-name = proc-name
  (apply-env ρ₁ search-proc-name) = (proc-val (procedure bound-var proc-body ρ₁))


  ρ₁ = (extend-env-rec proc-name bound-var proc-body ρ₀)
--------------------------------------------------------------------- search-proc-name ≠ proc-name
  (apply-env ρ₁ search-proc-name) = (apply-env ρ₀ search-proc-name)

(define apply-env
  (lambda (env search-var)
     (cases environment env        
        ...
        (extend-env-rec (proc-name bound-var proc-body saved-env)
          (if (eqv? search-var proc-name)
              (proc-val (procedure bound-var proc-body env))
              (apply-env saved-env search-var)))
        ...)))