previous up next
Go backward to Programs Are Functions
Go up to Top
Go forward to Program Denotation
RISC-Linz logo

Programs are Functions

||
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

Author: Wolfgang Schreiner
Last Modification: October 14, 1997

previous up next