Go backward to Programs Are Functions Go up to Top Go forward to Program Denotation |
||
lambdan.let s1 = ( [ [[A]] |-> n] newstore) s2 = [ [[Z]] |-> one ]s1 s3 = (n equals zero) -> _|_ [] s2 s' = [ [[Z]] |-> three ]s3 in access [[Z]] s'
||
lambdan.let s1 = ( [ [[A]] |-> n] newstore) s2 = [ [[Z]] |-> one ]s1 s3 = (n equals zero) -> _|_ [] s2 s' =(n equals zero) -> _|_ [] [ [[Z]] |-> three ]s3 in access [[Z]] s'
||
lambdan.let s1 = ( [ [[A]] |-> n] newstore) s2 = [ [[Z]] |-> one ]s1 in (n equals zero) -> _|_ [] access [[Z]] [ [[Z]] |-> three ]s2
||
lambdan.(n equals zero) -> _|_ [] three