let f = proc (x,y) -(x,y) in (f (4, 3))
value-of
(value-of (proc-exp (args 𝑣𝑎𝑟₁ 𝑣𝑎𝑟₂ ... 𝑣𝑎𝑟ₙ) 𝑏𝑜𝑑𝑦) ρ) = (proc-val (procedure (𝑣𝑎𝑟₁ 𝑣𝑎𝑟₂ ... 𝑣𝑎𝑟ₙ) 𝑏𝑜𝑑𝑦 ρ))
(value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁) = (proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)) (value-of 𝑟𝑎𝑛𝑑₁ ρ₁) = 𝑣𝑎𝑙₁ (value-of 𝑟𝑎𝑛𝑑₂ ρ₁) = 𝑣𝑎𝑙₂ ... (value-of 𝑟𝑎𝑛𝑑ₙ ρ₁) = 𝑣𝑎𝑙ₙ ---------------------------------------------------------------------------------------------- (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑₁ 𝑟𝑎𝑛𝑑₂ ... 𝑟𝑎𝑛𝑑ₙ) ρ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟₁=𝑣𝑎𝑙₁,...,𝑣𝑎𝑟ₙ=𝑣𝑎𝑙ₙ]ρ₂)
↓
let f = proc (x) proc (y) -(x,y) in ((f 4) 3)
(value-of <<let f = proc (x) proc (y) -(x,y) in ((f 4) 3)>> ρ₁) = (value-of <<((f 4) 3)>> [f=(proc-val (procedure x <<proc (y) -(x,y)>> ρ₁))]ρ₁)
(value-of (proc-exp 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦) ρ) = (proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ))
(value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁) = (proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)) (value-of 𝑟𝑎𝑛𝑑 ρ₁) = 𝑣𝑎𝑙 ---------------------------------------------------------------- (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑣𝑎𝑙]ρ₂)
(value-of <<(f 4)>> [f=(proc-val (procedure x <<proc (y) -(x,y)>> ρ₁))]ρ₁) = (value-of <<proc (y) -(x,y)>> [x=4]ρ₁) = (proc-val (procedure y <<-(x,y)>> [x=4]ρ₁))
(value-of <<((f 4) 3)>> [f=(proc-val (procedure x <<proc (y) -(x,y)>> ρ₁))]ρ₁) = (value-of <<-(x,y)>> [y=3][x=4]ρ₁) = 1
(value-of <<(f 4)>> [f=(proc-val (procedure x <<proc (y) -(x,y)>> ρ₁))]ρ₁) = (proc-val (procedure y <<-(x,y)>> [x=4]ρ₁))
v.s.