Go backward to Function Domains Go up to Top Go forward to Lifted Domains

Function Domains

Dynamic arrays with curried operations

Domain Array = Nat -> A

where A is a domain with an error element

Operations

newarray: Array
    newarray = lambda n.error
access: Nat -> Array -> A
    access = lambda n.lambda r.r(n)
update: Nat -> A -> Array -> Array
    access = lambda n.lambda v.lambda r.[n |-> v]r

Functions take one argument at a time!

access(k) = lambda r.r(k)
access(k)(r) -> r(k)
(access k r) -> r(k)