5.3操作语义 ·-→eam公理 (x,S〉-→eal7(c) -〈c,S）-→eval CA →ea推理规则 (M,s〉-→emly1…〈Mn〉-之erat V&(Vp,w小y fM1.M3S〉-→eval V 〈k,S〉-→ealI lookupA(s,D)=v (contx,S〉→eval V5.3 操作语义 • →eval公理 – x, s →eval  (x) – c, s →eval c A • →eval推理规则 f A(v1 ,…, vk )=v lookupA(s, l)=v M1 , s →eval v1 … Mk , s →eval vk f M1… Mk , s →eval v x, s →eval l cont x, s →eval v