5.2 Kerneli语言 基调Σ的第4个类别state init state update state x loc x val -state lookup state x loc -val 代数公理 lookup (update s I v)1 (lookup) if Eg?II then y else (lookup s l) update s l (lookup s I)s (update) update (update s l u)I y if Eg?IP (update)2 then update s l v else update (update s l'v)l u5.2 Kernel语言 基调的第4个类别state init : state update : state  loc  val → state lookup : state  loc → val 代数公理 lookup (update s l v) l = (lookup) if Eq? l l then v else (lookup s l) update s l (lookup s l) = s (update)1 update (update s l u) l v = if Eq? l l (update)2 then update s l v else update (update s l v) l u